Mathlib Changelog
v4
Changelog
About
Github
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