English
If f is analytic on s and fderivWithin is ContDiffOn ω on s, then f is ContDiffOn on s for all n.
Русский
Если f аналитична на s и fderivWithin 𝕜 f s имеет гладкость ω на s, тогда f ∈ ContDiffOn 𝕜 n f s для всех n.
LaTeX
$$$\\text{AnalyticOn } 𝕜 f s \\wedge \\ContDiffOn 𝕜 ω (fderivWithin 𝕜 f s) s \\Rightarrow \\ContDiffOn 𝕜 n f s\\quad (\\forall n)$$$
Lean4
theorem contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn (hs : UniqueDiffOn 𝕜 s) :
ContDiffOn 𝕜 (n + 1) f s ↔
(n = ω → AnalyticOn 𝕜 f s) ∧
∃ f' : E → E →L[𝕜] F, ContDiffOn 𝕜 n f' s ∧ ∀ x, x ∈ s → HasFDerivWithinAt f (f' x) s x :=
by
rw [contDiffOn_succ_iff_fderivWithin hs]
refine ⟨fun h => ⟨h.2.1, fderivWithin 𝕜 f s, h.2.2, fun x hx => (h.1 x hx).hasFDerivWithinAt⟩, fun ⟨f_an, h⟩ => ?_⟩
rcases h with ⟨f', h1, h2⟩
refine ⟨fun x hx => (h2 x hx).differentiableWithinAt, f_an, fun x hx => ?_⟩
exact (h1 x hx).congr_of_mem (fun y hy => (h2 y hy).fderivWithin (hs y hy)) hx
