Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
  2. prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
Changeset 63941:f353674c2528 by hoelzl:
move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Complex_Analysis_Basics.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Set_Integral.thy (diff)
Changeset 63940:0d82c4c94014 by hoelzl:
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)