English
If n is not infinity, ContDiffWithinAt 𝕜 n f s x is equivalent to the existence of a neighborhood u and a formal Taylor series p with HasFTaylorSeriesUpToOn n f p u, together with an ω-analytic condition if n equals ω.
Русский
Если n не равен бесконечности, ContDiffWithinAt 𝕜 n f s x эквивалентно существованию окрестности u и формальной серии Тейлора p c HasFTaylorSeriesUpToOn n f p u, вместе с аналитическим условием для случая n = ω.
LaTeX
$$$ ContDiffWithinAt 𝕜 n f s x \\iff \\exists u \\in 𝓝[insert x s] x, \\; \\exists p : E \\to \\text{FormalMultilinearSeries } 𝕜 E F,\\ HasFTaylorSeriesUpToOn n f p u \\land (n = ω \\to \\forall i, AnalyticOn 𝕜 (\\lambda z, p z i) u)$$
Lean4
/-- When `n` is either a natural number or `ω`, one can characterize the property of being `C^n`
as the existence of a neighborhood on which there is a Taylor series up to order `n`,
requiring in addition that its terms are analytic in the `ω` case. -/
theorem contDiffWithinAt_iff_of_ne_infty (hn : n ≠ ∞) :
ContDiffWithinAt 𝕜 n f s x ↔
∃ u ∈ 𝓝[insert x s] x,
∃ p : E → FormalMultilinearSeries 𝕜 E F,
HasFTaylorSeriesUpToOn n f p u ∧ (n = ω → ∀ i, AnalyticOn 𝕜 (fun x ↦ p x i) u) :=
by
match n with
| ω => simp [ContDiffWithinAt]
| ∞ => simp at hn
| (n : ℕ) => simp [contDiffWithinAt_nat]
