English
If around every point x ∈ s there exists an open neighborhood u with x ∈ u such that ContDiffOn 𝕜 n f (s ∩ u), then ContDiffOn 𝕜 n f s.
Русский
Если вокруг каждой точки x ∈ s существует открытое множество u с x ∈ u и ContDiffOn 𝕜 n f (s ∩ u), то ContDiffOn 𝕜 n f s.
LaTeX
$$$(\\forall x \\in s, \\exists u,\\ IsOpen u \\land x \\in u \\land ContDiffOn\\ 𝕜\\ n\\ f\\ (s \\cap u)) \\rightarrow ContDiffOn\\ 𝕜\\ n\\ f\\ s$$$
Lean4
/-- A function is `C^(n + 1)` on a domain iff locally, it has a derivative which is `C^n`. -/
theorem contDiffOn_succ_iff_hasFDerivWithinAt (hn : n ≠ ∞) :
ContDiffOn 𝕜 (n + 1) f s ↔
∀ x ∈ s,
∃ u ∈ 𝓝[insert x s] x,
(n = ω → AnalyticOn 𝕜 f u) ∧
∃ f' : E → E →L[𝕜] F, (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u :=
by
constructor
· intro h x hx
rcases (contDiffWithinAt_succ_iff_hasFDerivWithinAt hn).1 (h x hx) with ⟨u, hu, f_an, f', hf', Hf'⟩
rcases Hf'.contDiffOn le_rfl (by simp [hn]) with ⟨v, vu, v'u, hv⟩
rw [insert_eq_of_mem hx] at hu ⊢
have xu : x ∈ u := mem_of_mem_nhdsWithin hx hu
rw [insert_eq_of_mem xu] at vu v'u
exact ⟨v, nhdsWithin_le_of_mem hu vu, fun h ↦ (f_an h).mono v'u, f', fun y hy ↦ (hf' y (v'u hy)).mono v'u, hv⟩
· intro h x hx
rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt hn]
rcases h x hx with ⟨u, u_nhbd, f_an, f', hu, hf'⟩
have : x ∈ u := mem_of_mem_nhdsWithin (mem_insert _ _) u_nhbd
exact ⟨u, u_nhbd, f_an, f', hu, hf' x this⟩
