Commit 2023-06-08 18:26 21a16103

View on Github →

feat: port MeasureTheory.Measure.Lebesgue.Integral (#4734)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean

added theorem Real.integrable_of_summable_norm_Icc

added theorem integral_comp_neg_Iic

added theorem integral_comp_neg_Ioi

added theorem volume_regionBetween_eq_integral'

added theorem volume_regionBetween_eq_integral