English
If for every m, AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s, then ContDiffOn 𝕜 n f s.
Русский
Если для каждого m AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s, тогда ContDiffOn 𝕜 n f s.
LaTeX
$$$(\\forall m, AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s) → ContDiffOn 𝕜 n f s$$$
Lean4
theorem contDiffOn_of_analyticOn_iteratedFDerivWithin (h : ∀ m, AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s) :
ContDiffOn 𝕜 n f s := by
suffices ContDiffOn 𝕜 ω f s from this.of_le le_top
intro x hx
refine ⟨insert x s, self_mem_nhdsWithin, ftaylorSeriesWithin 𝕜 f s, ?_, ?_⟩
· rw [insert_eq_of_mem hx]
constructor
· intro y _
simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply, iteratedFDerivWithin_zero_apply]
· intro k _ y hy
exact ((h k).differentiableOn y hy).hasFDerivWithinAt
· intro k _
exact (h k).continuousOn
· intro i
rw [insert_eq_of_mem hx]
exact h i
