Commit 2026-01-05 16:12 2ae0b921

View on Github →

feat(MeasureTheory/Integral): add versions of exists_eq_interval_average and first mean value theorem for integrals (#30344) Add the First mean value theorem for (unordered) interval integrals on ℝ.

exists_eq_const_mul_interval_integral_of_continuous_on_of_ae_nonneg
exists_eq_const_mul_interval_integral_of_continuous_on_of_nonneg

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

added theorem ContinuousOn.integrableOn_of_subset_isCompact

Modified Mathlib/MeasureTheory/Integral/Average.lean

added theorem MeasureTheory.exists_eq_setAverage

Modified Mathlib/MeasureTheory/Integral/IntervalAverage.lean

added theorem exists_eq_interval_average_of_measure

added theorem exists_eq_interval_average_of_noAtoms

Created Mathlib/MeasureTheory/Integral/IntervalIntegral/MeanValue.lean

added theorem exists_eq_const_mul_intervalIntegral_of_ae_nonneg

added theorem exists_eq_const_mul_intervalIntegral_of_nonneg

Created Mathlib/MeasureTheory/Integral/MeanValue.lean

added theorem exists_eq_const_mul_setIntegral_of_ae_nonneg

added theorem exists_eq_const_mul_setIntegral_of_nonneg

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

added theorem Real.volume_uIoc

added theorem Real.volume_uIoo

Modified Mathlib/Order/Interval/Set/UnorderedInterval.lean

added theorem Set.nonempty_uIoc

Modified Mathlib/Topology/Order/IntermediateValue.lean

added theorem isConnected_uIoc

added theorem isConnected_uIoo

added theorem isPreconnected_uIoc

added theorem isPreconnected_uIoo