English
Let s be a domain with unique differentiability. Then f is ContDiffOn 𝕜 n on s if and only if, for every m, m ≤ n implies the m-th iterated derivative within s is continuous on s, and for every m, m < n implies the m-th iterated derivative within s is differentiable on s.
Русский
Пусть s — область, на которой существуют уникальные производные. Тогда f∈ContDiffOn 𝕜 n на s эквивалентно тому, что для каждого m≤n функция iteratedFDerivWithin 𝕜 m f s непрерывна на s, а для каждого m<n она дифференцируема на s.
LaTeX
$$$\\text{UniqueDiffOn } 𝕜\, s \\;\\Rightarrow\\; \\ContDiffOn 𝕜 n f s \\iff \\Big(\\forall m : \\mathbb{N},\\ m \\le n \\to \\operatorname{ContinuousOn}(\\lambda x. \\operatorname{iteratedFDerivWithin} 𝕜 m f s x)\\, s\\Big) \\land \\Big(\\forall m : \\mathbb{N},\\ m < n \\to \\operatorname{DifferentiableOn} 𝕜 (\\lambda x. \\operatorname{iteratedFDerivWithin} 𝕜 m f s x) \\; s\\Big)$$
Lean4
theorem contDiffOn_iff_continuousOn_differentiableOn {n : ℕ∞} (hs : UniqueDiffOn 𝕜 s) :
ContDiffOn 𝕜 n f s ↔
(∀ m : ℕ, m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
∀ m : ℕ, m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s :=
⟨fun h =>
⟨fun _m hm => h.continuousOn_iteratedFDerivWithin (mod_cast hm) hs, fun _m hm =>
h.differentiableOn_iteratedFDerivWithin (mod_cast hm) hs⟩,
fun h => contDiffOn_of_continuousOn_differentiableOn h.1 h.2⟩
