Commit 2023-09-15 05:52 ee0f4af6

View on Github →

feat: the line derivative is measurable (#7055) Last prerequisite for Rademacher theorem in #7003. Along the way, we weaken the second-countability assumptions for strong measurability of the derivative and the right derivative.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

modified theorem aestronglyMeasurable_derivWithin_Ici

modified theorem aestronglyMeasurable_derivWithin_Ioi

modified theorem stronglyMeasurable_derivWithin_Ici

modified theorem stronglyMeasurable_derivWithin_Ioi

Created Mathlib/Analysis/Calculus/LineDeriv/Measurable.lean

added theorem aemeasurable_lineDeriv

added theorem aemeasurable_lineDeriv_uncurry

added theorem aestronglyMeasurable_lineDeriv

added theorem aestronglyMeasurable_lineDeriv_uncurry

added theorem measurableSet_lineDifferentiableAt

added theorem measurableSet_lineDifferentiableAt_uncurry

added theorem measurable_lineDeriv

added theorem measurable_lineDeriv_uncurry

added theorem stronglyMeasurable_lineDeriv

added theorem stronglyMeasurable_lineDeriv_uncurry