Commit 2023-05-29 18:40 1196ccc5

View on Github →

feat: port Analysis.Calculus.FDerivMeasurable (#4468)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/FDerivMeasurable.lean

added theorem ContinuousLinearMap.measurable_apply₂

added def FDerivMeasurableAux.A

added def FDerivMeasurableAux.B

added def FDerivMeasurableAux.D

added theorem FDerivMeasurableAux.a_mono

added theorem FDerivMeasurableAux.d_subset_differentiable_set

added theorem FDerivMeasurableAux.differentiable_set_eq_d

added theorem FDerivMeasurableAux.differentiable_set_subset_d

added theorem FDerivMeasurableAux.isOpen_a

added theorem FDerivMeasurableAux.isOpen_b

added theorem FDerivMeasurableAux.le_of_mem_a

added theorem FDerivMeasurableAux.mem_a_of_differentiable

added theorem FDerivMeasurableAux.norm_sub_le_of_mem_a

added def RightDerivMeasurableAux.A

added def RightDerivMeasurableAux.B

added def RightDerivMeasurableAux.D

added theorem RightDerivMeasurableAux.a_mem_nhdsWithin_Ioi

added theorem RightDerivMeasurableAux.a_mono

added theorem RightDerivMeasurableAux.b_mem_nhdsWithin_Ioi

added theorem RightDerivMeasurableAux.d_subset_differentiable_set

added theorem RightDerivMeasurableAux.differentiable_set_eq_d

added theorem RightDerivMeasurableAux.differentiable_set_subset_d

added theorem RightDerivMeasurableAux.le_of_mem_a

added theorem RightDerivMeasurableAux.measurableSet_b

added theorem RightDerivMeasurableAux.mem_a_of_differentiable

added theorem RightDerivMeasurableAux.norm_sub_le_of_mem_a

added theorem aemeasurable_deriv

added theorem aemeasurable_derivWithin_Ici

added theorem aemeasurable_derivWithin_Ioi

added theorem aestronglyMeasurable_deriv

added theorem aestronglyMeasurable_derivWithin_Ici

added theorem aestronglyMeasurable_derivWithin_Ioi

added theorem measurableSet_of_differentiableAt

added theorem measurableSet_of_differentiableAt_of_isComplete

added theorem measurableSet_of_differentiableWithinAt_Ici

added theorem measurableSet_of_differentiableWithinAt_Ici_of_isComplete

added theorem measurableSet_of_differentiableWithinAt_Ioi

added theorem measurable_deriv

added theorem measurable_derivWithin_Ici

added theorem measurable_derivWithin_Ioi

added theorem measurable_fderiv

added theorem measurable_fderiv_apply_const

added theorem stronglyMeasurable_deriv

added theorem stronglyMeasurable_derivWithin_Ici

added theorem stronglyMeasurable_derivWithin_Ioi