English
On a domain with UniqueDiffOn, ContDiffOn (n+1) f s is equivalent to differentiability of f on s, plus analyticity when n=ω, and ContDiffOn n of fderivWithin f s on s.
Русский
На области с уникальными дифференциалами ContDiffOn (n+1) f s эквивалентно дифференцируемости f на s, аналитичности при n=ω и ContDiffOn n по fderivWithin f s на s.
LaTeX
$$$\\text{UniqueDiffOn } 𝕜 s \\Rightarrow \\ContDiffOn 𝕜 (n+1) f s \\iff (\\text{DifferentiableOn } 𝕜 f s) \\land (\\big(n = ω \\Rightarrow AnalyticOn 𝕜 f s\\big)) \\land \\ContDiffOn 𝕜 n (fderivWithin 𝕜 f s) s$$
Lean4
theorem contDiffOn_of_analyticOn_of_fderivWithin (hf : AnalyticOn 𝕜 f s)
(h : ContDiffOn 𝕜 ω (fun y ↦ fderivWithin 𝕜 f s y) s) : ContDiffOn 𝕜 n f s :=
by
suffices ContDiffOn 𝕜 (ω + 1) f s from this.of_le le_top
exact contDiffOn_succ_of_fderivWithin hf.differentiableOn (fun _ ↦ hf) h
