Commit 2024-11-25 11:42 85ded514

View on Github →

feat: extend ContDiff to take a smoothness exponent in WithTop ℕ∞ (#19442) This is mathematically not meaningful at all, since the definition of C^∞ and C^ω functions is the same in this PR. However, this opens the way to replacing the definition of C^ω with analytic in #17152. So, the current PR is just an intermediate step towards #17152, but making sure that the final diff will be smaller than the current +1280 lines changes. There is no mathematical content in the current PR: it's mostly adapting the library to provide an element of WithTop ℕ∞ when it was expecting an element of ℕ∞ before. In the locale ContDiff, we introduce two notations ω for ⊤ : WithTop ℕ∞ and ∞ for (⊤ : ℕ∞) : WithTop ℕ∞. A lot of the changes are to open the locale and use ∞ at suitable places.

Estimated changes

modified theorem ContDiff.div
modified theorem ContDiff.fderiv_apply
modified theorem ContDiff.fderiv_right
modified theorem ContDiff.inv
modified theorem ContDiffAt.fderiv_right
modified theorem ContDiffOn.div
modified theorem ContDiffOn.inv
modified theorem ContDiffWithinAt.div
modified theorem ContDiffWithinAt.inv
modified theorem Continuous.fderiv
modified theorem contDiff_single
modified theorem contDiff_update
modified theorem contDiff_zero_fun
modified theorem norm_iteratedFDeriv_comp_le
modified theorem norm_iteratedFDeriv_mul_le
modified theorem norm_iteratedFDeriv_smul_le
modified def ContDiff
modified def ContDiffAt
modified def ContDiffOn
modified def ContDiffWithinAt
modified theorem contDiffOn_all_iff_nat
modified theorem contDiff_all_iff_nat
modified theorem contDiff_iff_forall_nat_le
modified theorem contDiffOn_clm_apply
modified theorem contDiff_clm_apply_iff
modified theorem AnalyticAt.contDiffAt
modified theorem AnalyticOnNhd.contDiff
modified theorem CPolynomialAt.contDiffAt
modified theorem CPolynomialOn.contDiffOn
modified theorem ContDiffAt.to_localInverse
modified theorem ContDiff.real_of_complex
modified theorem ContDiffAt.real_of_complex
modified theorem Complex.contDiff_exp
modified theorem Real.contDiff_exp
modified theorem Real.contDiffAt_log
modified theorem Real.contDiffOn_log
modified theorem Real.contDiffAt_rpow_of_ne
modified theorem Complex.contDiffAt_tan
modified theorem Real.contDiffAt_arccos
modified theorem Real.contDiffAt_arccos_iff
modified theorem Real.contDiffAt_arcsin
modified theorem Real.contDiffAt_arcsin_iff
modified theorem Real.contDiffOn_arccos
modified theorem Real.contDiffOn_arcsin
modified theorem contDiff_stereoInvFunAux
modified theorem contMDiff_circleExp