Commit 2024-07-22 14:24 409fa733

View on Github →

feat: continuity of primitives for parametric integrals (#11185) From the sphere eversion project and generalised by sgouezel. This is used in the sphere eversion project to show that averaging of loops is continuous (which will be PRed to mathlib at a later point). Co-authored by: @fpvandoorn (who write this code originally, I believe)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

added theorem tendsto_measure_Icc

added theorem tendsto_measure_Icc_nhdsWithin_right'

added theorem tendsto_measure_Icc_nhdsWithin_right

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

modified theorem intervalIntegral.continuousAt_parametric_primitive_of_dominated

added theorem intervalIntegral.continuous_parametric_intervalIntegral_of_continuous'

added theorem intervalIntegral.continuous_parametric_intervalIntegral_of_continuous

added theorem intervalIntegral.continuous_parametric_primitive_of_continuous

Modified Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean

added theorem Real.singleton_eq_inter_Icc

Modified Mathlib/Topology/Order/LeftRight.lean

added theorem nhdsWithin_right_sup_nhds_singleton