English
If f is differentiable on s, analytic wherever n=ω, and ContDiffOn ω (fderivWithin f s) on s, then ContDiffOn (n+1) f s.
Русский
Если функция дифференцируема на s, аналитична там, где n=ω, и ContDiffOn ω (fderivWithin f s) на s, тогда f ∈ ContDiffOn (n+1) f s.
LaTeX
$$$\\text{DifferentiableOn } 𝕜 f s \\wedge (n = ω \\rightarrow AnalyticOn 𝕜 f s) \\wedge \\ContDiffOn 𝕜 ω (fderivWithin 𝕜 f s) s \\Rightarrow \\ContDiffOn 𝕜 (n+1) f s$$
Lean4
theorem contDiffOn_succ_of_fderivWithin (hf : DifferentiableOn 𝕜 f s) (h' : n = ω → AnalyticOn 𝕜 f s)
(h : ContDiffOn 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) : ContDiffOn 𝕜 (n + 1) f s :=
by
rcases eq_or_ne n ∞ with rfl | hn
· rw [ENat.coe_top_add_one, contDiffOn_infty]
intro m x hx
apply ContDiffWithinAt.of_le _ (show (m : WithTop ℕ∞) ≤ m + 1 from le_self_add)
rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt (by simp), insert_eq_of_mem hx]
exact
⟨s, self_mem_nhdsWithin, (by simp), fderivWithin 𝕜 f s, fun y hy => (hf y hy).hasFDerivWithinAt,
(h x hx).of_le (mod_cast le_top)⟩
· intro x hx
rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt hn, insert_eq_of_mem hx]
exact ⟨s, self_mem_nhdsWithin, h', fderivWithin 𝕜 f s, fun y hy => (hf y hy).hasFDerivWithinAt, h x hx⟩
