Commit 2023-11-11 17:12 5ac3430b

View on Github →

chore: split Mathlib.Analysis.Calculus.ContDiff.Basic (#8344)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

deleted theorem ContDiff.hasStrictDerivAt

deleted theorem ContDiff.hasStrictFDerivAt

deleted theorem ContDiff.lipschitzWith_of_hasCompactSupport

deleted theorem ContDiff.locallyLipschitz

deleted theorem ContDiffAt.exists_lipschitzOnWith

deleted theorem ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt

deleted theorem ContDiffAt.hasStrictDerivAt'

deleted theorem ContDiffAt.hasStrictDerivAt

deleted theorem ContDiffAt.hasStrictFDerivAt'

deleted theorem ContDiffAt.hasStrictFDerivAt

deleted theorem ContDiffWithinAt.exists_lipschitzOnWith

deleted theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear

deleted theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux

deleted theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one

deleted theorem ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear

deleted theorem ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one

deleted theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith

deleted theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt

deleted theorem HasFTaylorSeriesUpToOn.hasStrictFDerivAt

deleted theorem contDiffOn_clm_apply

deleted theorem contDiffOn_succ_iff_fderiv_apply

deleted theorem contDiffOn_succ_of_fderiv_apply

deleted theorem contDiff_clm_apply_iff

deleted theorem contDiff_succ_iff_fderiv_apply

deleted theorem norm_iteratedFDerivWithin_clm_apply

deleted theorem norm_iteratedFDerivWithin_clm_apply_const

deleted theorem norm_iteratedFDerivWithin_comp_le

deleted theorem norm_iteratedFDerivWithin_comp_le_aux

deleted theorem norm_iteratedFDerivWithin_mul_le

deleted theorem norm_iteratedFDerivWithin_smul_le

deleted theorem norm_iteratedFDeriv_clm_apply

deleted theorem norm_iteratedFDeriv_clm_apply_const

deleted theorem norm_iteratedFDeriv_comp_le

deleted theorem norm_iteratedFDeriv_mul_le

deleted theorem norm_iteratedFDeriv_smul_le

Created Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

added theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear

added theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux

added theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one

added theorem ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear

added theorem ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one

added theorem norm_iteratedFDerivWithin_clm_apply

added theorem norm_iteratedFDerivWithin_clm_apply_const

added theorem norm_iteratedFDerivWithin_comp_le

added theorem norm_iteratedFDerivWithin_comp_le_aux

added theorem norm_iteratedFDerivWithin_mul_le

added theorem norm_iteratedFDerivWithin_smul_le

added theorem norm_iteratedFDeriv_clm_apply

added theorem norm_iteratedFDeriv_clm_apply_const

added theorem norm_iteratedFDeriv_comp_le

added theorem norm_iteratedFDeriv_mul_le

added theorem norm_iteratedFDeriv_smul_le

Created Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean

added theorem contDiffOn_clm_apply

added theorem contDiffOn_succ_iff_fderiv_apply

added theorem contDiffOn_succ_of_fderiv_apply

added theorem contDiff_clm_apply_iff

added theorem contDiff_succ_iff_fderiv_apply

Created Mathlib/Analysis/Calculus/ContDiff/IsROrC.lean

added theorem ContDiff.hasStrictDerivAt

added theorem ContDiff.hasStrictFDerivAt

added theorem ContDiff.lipschitzWith_of_hasCompactSupport

added theorem ContDiff.locallyLipschitz

added theorem ContDiffAt.exists_lipschitzOnWith

added theorem ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt

added theorem ContDiffAt.hasStrictDerivAt'

added theorem ContDiffAt.hasStrictDerivAt

added theorem ContDiffAt.hasStrictFDerivAt'

added theorem ContDiffAt.hasStrictFDerivAt

added theorem ContDiffWithinAt.exists_lipschitzOnWith

added theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith

added theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt

added theorem HasFTaylorSeriesUpToOn.hasStrictFDerivAt

Modified Mathlib/Analysis/Calculus/Inverse.lean

Modified Mathlib/Analysis/Calculus/Series.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean