English
If for each m ≤ n, the iterated derivatives iteratedFDerivWithin 𝕜 m f s are continuous on s, and for m < n they are differentiable on s, then f is ContDiffOn 𝕜 n f s.
Русский
Если для каждого m ≤ n соответствующие итеративные производные непрерывны на s, а для m < n они дифференцируемы на s, то f ∈ ContDiffOn 𝕜 n f s.
LaTeX
$$$(\\forall m, m ≤ n → ContinuousOn (iteratedFDerivWithin 𝕜 m f s) s) ∧ (\\forall m, m < n → DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s) → ContDiffOn 𝕜 n f s$$$
Lean4
theorem contDiffOn_of_continuousOn_differentiableOn {n : ℕ∞}
(Hcont : ∀ m : ℕ, m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s)
(Hdiff : ∀ m : ℕ, m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s) : ContDiffOn 𝕜 n f s :=
by
intro x hx m hm
rw [insert_eq_of_mem hx]
refine ⟨s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_⟩
constructor
· intro y _
simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply, iteratedFDerivWithin_zero_apply]
· intro k hk y hy
convert (Hdiff k (lt_of_lt_of_le (mod_cast hk) (mod_cast hm)) y hy).hasFDerivWithinAt
· intro k hk
exact Hcont k (le_trans (mod_cast hk) (mod_cast hm))
