Commit 2024-11-29 21:45 67afcb68

View on Github →

feat: update the ContDiff definition to integrate analytic functions in the hierarchy (#17152) We modify the definition of ContDiff so that the smoothness exponent belongs to WithTop (ℕ∞), where top smoothness (denoted with ω in the ContDiff scope) means analyticity (together with analyticity of all the iterated derivatives). This will make it possible to write theorems like: consider a function which is C^2 over the reals or complexes, or analytic over a general field. Then... Many theorems in calculus hold under these assumptions (and it's the way things are written in Bourbaki), so having this possibility is a necessary improvement unless one wants to duplicate everything. The PR is mostly not changing the API: theorems that were proved for C^n functions with n ∈ ℕ or n = ∞ are now proved for n ∈ ℕ or n = ∞ or n = ω (unless they are not true for analytic functions, but it turns out in most cases things are fine). Of course, results have to be added in the files ContDiff.Def and ContDiff.Basic to deal with analytic functions. I know that the PR is huge and hard to review. I have tried to separate all the other results in other PRs, but once one changes the basic definition one has to fix everything downstream to get mathlib compiling, so I can not make it shorter...

Estimated changes

deleted theorem AnalyticAt.contDiffAt
deleted theorem AnalyticOnNhd.contDiff
modified theorem ContDiff.continuous_deriv
modified theorem ContDiff.div
modified theorem ContDiffOn.div
modified theorem ContDiffWithinAt.div
modified theorem ContDiffWithinAt.inv
modified theorem IsBoundedLinearMap.contDiff
modified theorem contDiffAt_ring_inverse
modified theorem contDiff_const
modified theorem contDiff_one_iff_deriv
modified theorem contDiff_succ_iff_deriv
deleted theorem contDiff_top_iff_deriv
modified theorem contDiff_zero_fun
added theorem AnalyticAt.contDiffAt
added theorem AnalyticOn.contDiff
added theorem AnalyticOn.contDiffOn
added theorem AnalyticOnNhd.contDiff
added theorem ContDiff.analyticOnNhd
modified theorem ContDiff.of_succ
modified theorem ContDiff.one_of_succ
added theorem ContDiffAt.analyticAt
added theorem ContDiffOn.analyticOn
modified theorem ContDiffOn.of_succ
modified theorem ContDiffOn.one_of_succ
modified theorem ContDiffWithinAt.contDiffOn
added theorem contDiffAt_infty
deleted theorem contDiffAt_top
added theorem contDiffOn_infty
deleted theorem contDiffOn_top
added theorem contDiffWithinAt_infty
deleted theorem contDiffWithinAt_top
modified theorem contDiff_all_iff_nat
modified theorem contDiff_iff_ftaylorSeries
added theorem contDiff_infty
modified theorem contDiff_one_iff_fderiv
modified theorem contDiff_succ_iff_fderiv
deleted theorem contDiff_top
deleted theorem contDiff_top_iff_fderiv
modified theorem contDiffAt_piLp
modified theorem contDiffOn_piLp
modified theorem contDiffWithinAt_piLp
modified theorem contDiff_piLp
modified theorem contDiffAt_euclidean
modified theorem contDiffOn_euclidean
modified theorem contDiffWithinAt_euclidean
modified theorem contDiff_euclidean
modified theorem Complex.contDiffAt_log
modified theorem Real.contDiffAt_log
modified theorem Real.contDiffAt_sqrt
modified theorem Real.contDiffAt_tan
modified theorem Real.contDiff_arctan
modified theorem ContDiffOn.div'