Commit 2023-06-04 09:37 c9bd9b5d

View on Github →

feat: port Analysis.Calculus.ContDiff (#4532)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/ContDiff.lean

added theorem ContDiff.add

added theorem ContDiff.clm_apply

added theorem ContDiff.clm_comp

added theorem ContDiff.comp

added theorem ContDiff.comp_contDiffAt

added theorem ContDiff.comp_contDiffOn

added theorem ContDiff.comp_contDiffWithinAt

added theorem ContDiff.comp_contDiff_on₂

added theorem ContDiff.comp_contDiff_on₃

added theorem ContDiff.comp_continuousLinearMap

added theorem ContDiff.comp₂

added theorem ContDiff.comp₃

added theorem ContDiff.const_smul

added theorem ContDiff.contDiff_fderiv_apply

added theorem ContDiff.continuousLinearMap_comp

added theorem ContDiff.continuous_deriv

added theorem ContDiff.div

added theorem ContDiff.div_const

added theorem ContDiff.fderiv_apply

added theorem ContDiff.fderiv_right

added theorem ContDiff.fst'

added theorem ContDiff.fst

added theorem ContDiff.hasStrictDerivAt

added theorem ContDiff.hasStrictFDerivAt

added theorem ContDiff.inv

added theorem ContDiff.iterate_deriv'

added theorem ContDiff.iterate_deriv

added theorem ContDiff.mul

added theorem ContDiff.neg

added theorem ContDiff.pow

added theorem ContDiff.prod

added theorem ContDiff.prod_map

added theorem ContDiff.restrict_scalars

added theorem ContDiff.smul

added theorem ContDiff.smulRight

added theorem ContDiff.snd'

added theorem ContDiff.snd

added theorem ContDiff.sub

added theorem ContDiff.sum

added theorem ContDiffAt.add

added theorem ContDiffAt.comp_contDiffWithinAt

added theorem ContDiffAt.const_smul

added theorem ContDiffAt.continuousLinearMap_comp

added theorem ContDiffAt.exists_lipschitzOnWith

added theorem ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt

added theorem ContDiffAt.fderiv_right

added theorem ContDiffAt.fst''

added theorem ContDiffAt.fst'

added theorem ContDiffAt.fst

added theorem ContDiffAt.hasStrictDerivAt'

added theorem ContDiffAt.hasStrictDerivAt

added theorem ContDiffAt.hasStrictFDerivAt'

added theorem ContDiffAt.hasStrictFDerivAt

added theorem ContDiffAt.neg

added theorem ContDiffAt.prod

added theorem ContDiffAt.prod_map'

added theorem ContDiffAt.prod_map

added theorem ContDiffAt.restrict_scalars

added theorem ContDiffAt.smul

added theorem ContDiffAt.snd''

added theorem ContDiffAt.snd'

added theorem ContDiffAt.snd

added theorem ContDiffAt.sub

added theorem ContDiffAt.sum

added theorem ContDiffOn.add

added theorem ContDiffOn.clm_apply

added theorem ContDiffOn.clm_comp

added theorem ContDiffOn.comp'

added theorem ContDiffOn.comp

added theorem ContDiffOn.comp_continuousLinearMap

added theorem ContDiffOn.const_smul

added theorem ContDiffOn.continuousLinearMap_comp

added theorem ContDiffOn.continuousOn_derivWithin

added theorem ContDiffOn.continuousOn_deriv_of_open

added theorem ContDiffOn.continuousOn_fderivWithin_apply

added theorem ContDiffOn.deriv_of_open

added theorem ContDiffOn.div

added theorem ContDiffOn.div_const

added theorem ContDiffOn.fst

added theorem ContDiffOn.inv

added theorem ContDiffOn.mul

added theorem ContDiffOn.neg

added theorem ContDiffOn.pow

added theorem ContDiffOn.prod

added theorem ContDiffOn.prod_map

added theorem ContDiffOn.restrict_scalars

added theorem ContDiffOn.smul

added theorem ContDiffOn.snd

added theorem ContDiffOn.sub

added theorem ContDiffOn.sum

added theorem ContDiffWithinAt.add

added theorem ContDiffWithinAt.comp'

added theorem ContDiffWithinAt.comp

added theorem ContDiffWithinAt.comp_continuousLinearMap

added theorem ContDiffWithinAt.comp_of_mem

added theorem ContDiffWithinAt.const_smul

added theorem ContDiffWithinAt.continuousLinearMap_comp

added theorem ContDiffWithinAt.div

added theorem ContDiffWithinAt.div_const

added theorem ContDiffWithinAt.exists_lipschitzOnWith

added theorem ContDiffWithinAt.fderivWithin''

added theorem ContDiffWithinAt.fderivWithin'

added theorem ContDiffWithinAt.fderivWithin_apply

added theorem ContDiffWithinAt.fderivWithin_right

added theorem ContDiffWithinAt.hasFDerivWithinAt_nhds

added theorem ContDiffWithinAt.inv

added theorem ContDiffWithinAt.mul

added theorem ContDiffWithinAt.neg

added theorem ContDiffWithinAt.pow

added theorem ContDiffWithinAt.prod

added theorem ContDiffWithinAt.prod_map'

added theorem ContDiffWithinAt.prod_map

added theorem ContDiffWithinAt.restrict_scalars

added theorem ContDiffWithinAt.smul

added theorem ContDiffWithinAt.sub

added theorem ContDiffWithinAt.sum

added theorem Continuous.fderiv

added theorem ContinuousLinearEquiv.comp_contDiffAt_iff

added theorem ContinuousLinearEquiv.comp_contDiffOn_iff

added theorem ContinuousLinearEquiv.comp_contDiffWithinAt_iff

added theorem ContinuousLinearEquiv.comp_contDiff_iff

added theorem ContinuousLinearEquiv.contDiff

added theorem ContinuousLinearEquiv.contDiffAt_comp_iff

added theorem ContinuousLinearEquiv.contDiffOn_comp_iff

added theorem ContinuousLinearEquiv.contDiffWithinAt_comp_iff

added theorem ContinuousLinearEquiv.contDiff_comp_iff

added theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_left

added theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_right

added theorem ContinuousLinearMap.contDiff

added theorem ContinuousLinearMap.iteratedFDerivWithin_comp_left

added theorem ContinuousLinearMap.iteratedFDerivWithin_comp_right

added theorem ContinuousLinearMap.iteratedFDeriv_comp_left

added theorem ContinuousLinearMap.iteratedFDeriv_comp_right

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 HasFTaylorSeriesUpToOn.add

added theorem HasFTaylorSeriesUpToOn.compContinuousLinearMap

added theorem HasFTaylorSeriesUpToOn.continuousLinearMap_comp

added theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith

added theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt

added theorem HasFTaylorSeriesUpToOn.hasStrictFDerivAt

added theorem HasFTaylorSeriesUpToOn.prod

added theorem HasFTaylorSeriesUpToOn.restrictScalars

added theorem Homeomorph.contDiff_symm

added theorem Homeomorph.contDiff_symm_deriv

added theorem IsBoundedBilinearMap.contDiff

added theorem IsBoundedLinearMap.contDiff

added theorem LinearIsometry.contDiff

added theorem LinearIsometry.norm_iteratedFDerivWithin_comp_left

added theorem LinearIsometry.norm_iteratedFDeriv_comp_left

added theorem LinearIsometryEquiv.contDiff

added theorem LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left

added theorem LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right

added theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_left

added theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_right

added theorem LocalHomeomorph.contDiffAt_symm

added theorem LocalHomeomorph.contDiffAt_symm_deriv

added theorem contDiffAt_const

added theorem contDiffAt_fst

added theorem contDiffAt_id

added theorem contDiffAt_inv

added theorem contDiffAt_map_inverse

added theorem contDiffAt_of_subsingleton

added theorem contDiffAt_pi

added theorem contDiffAt_prod'

added theorem contDiffAt_prod

added theorem contDiffAt_ring_inverse

added theorem contDiffAt_snd

added theorem contDiffOn_clm_apply

added theorem contDiffOn_const

added theorem contDiffOn_fderivWithin_apply

added theorem contDiffOn_fst

added theorem contDiffOn_id

added theorem contDiffOn_inv

added theorem contDiffOn_of_subsingleton

added theorem contDiffOn_pi

added theorem contDiffOn_prod'

added theorem contDiffOn_prod

added theorem contDiffOn_snd

added theorem contDiffOn_succ_iff_derivWithin

added theorem contDiffOn_succ_iff_deriv_of_open

added theorem contDiffOn_succ_iff_fderiv_apply

added theorem contDiffOn_succ_of_fderiv_apply

added theorem contDiffOn_top_iff_derivWithin

added theorem contDiffOn_top_iff_deriv_of_open

added theorem contDiffWithinAt_const

added theorem contDiffWithinAt_fst

added theorem contDiffWithinAt_id

added theorem contDiffWithinAt_of_subsingleton

added theorem contDiffWithinAt_pi

added theorem contDiffWithinAt_prod'

added theorem contDiffWithinAt_prod

added theorem contDiffWithinAt_snd

added theorem contDiff_add

added theorem contDiff_apply

added theorem contDiff_apply_apply

added theorem contDiff_clm_apply_iff

added theorem contDiff_const

added theorem contDiff_const_smul

added theorem contDiff_fst

added theorem contDiff_id

added theorem contDiff_mul

added theorem contDiff_neg

added theorem contDiff_of_subsingleton

added theorem contDiff_one_iff_deriv

added theorem contDiff_pi

added theorem contDiff_prod'

added theorem contDiff_prod

added theorem contDiff_prodAssoc

added theorem contDiff_prodAssoc_symm

added theorem contDiff_prod_mk_left

added theorem contDiff_prod_mk_right

added theorem contDiff_smul

added theorem contDiff_snd

added theorem contDiff_succ_iff_deriv

added theorem contDiff_succ_iff_fderiv_apply

added theorem contDiff_top_iff_deriv

added theorem contDiff_zero_fun

added theorem hasFTaylorSeriesUpToOn_pi'

added theorem hasFTaylorSeriesUpToOn_pi

added theorem iteratedFDerivWithin_add_apply'

added theorem iteratedFDerivWithin_add_apply

added theorem iteratedFDerivWithin_const_smul_apply

added theorem iteratedFDerivWithin_neg_apply

added theorem iteratedFDeriv_add_apply'

added theorem iteratedFDeriv_add_apply

added theorem iteratedFDeriv_const_of_ne

added theorem iteratedFDeriv_const_smul_apply

added theorem iteratedFDeriv_neg_apply

added theorem iteratedFDeriv_succ_const

added theorem iteratedFDeriv_zero_fun

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