English
A function is C^(n+1) at x iff there exists a derivative f' with HasFDerivAt and f' is C^n at x.
Русский
Функция является C^(n+1) в точке x тогда и только тогда, когда существует предел производной f' с HasFDerivAt и f' является C^n в точке x.
LaTeX
$$$ContDiffAt\ 𝕜\ (n+1)\ f\ x\iff \exists f' : E \to E \toL[𝕜] F,\ (\exists u \in 𝓝 x, \forall y \in u, HasFDerivAt\ f\ (f'\ y)\ y) \land ContDiffAt\ 𝕜\ n\ f'\ x$$$
Lean4
/-- A function is `C^(n + 1)` at a point iff locally, it has a derivative which is `C^n`. -/
theorem contDiffAt_succ_iff_hasFDerivAt {n : ℕ} :
ContDiffAt 𝕜 (n + 1) f x ↔
∃ f' : E → E →L[𝕜] F, (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 n f' x :=
by
rw [← contDiffWithinAt_univ, contDiffWithinAt_succ_iff_hasFDerivWithinAt (by simp)]
simp only [nhdsWithin_univ, mem_univ, insert_eq_of_mem]
constructor
· rintro ⟨u, H, -, f', h_fderiv, h_cont_diff⟩
rcases mem_nhds_iff.mp H with ⟨t, htu, ht, hxt⟩
refine ⟨f', ⟨t, ?_⟩, h_cont_diff.contDiffAt H⟩
refine ⟨mem_nhds_iff.mpr ⟨t, Subset.rfl, ht, hxt⟩, ?_⟩
intro y hyt
refine (h_fderiv y (htu hyt)).hasFDerivAt ?_
exact mem_nhds_iff.mpr ⟨t, htu, ht, hyt⟩
· rintro ⟨f', ⟨u, H, h_fderiv⟩, h_cont_diff⟩
refine ⟨u, H, by simp, f', fun x hxu ↦ ?_, h_cont_diff.contDiffWithinAt⟩
exact (h_fderiv x hxu).hasFDerivWithinAt
