English
For unique differentiable domains, a ContDiffOn (n+1) f s is equivalent to the existence of a family f' with ContDiffOn n and HasFDerivWithinAt f (f' x) on s.
Русский
На области с уникальной выпуклостью существует f' such that ContDiffOn n f' s и HasFDerivWithinAt f (f' x) на s для всех x∈s, если ContDiffOn (n+1) f s.
LaTeX
$$$\\text{UniqueDiffOn } 𝕜 s \\Rightarrow \\ContDiffOn 𝕜 (n+1) f s \\iff (\\nexists f' : E \\to E \\toL[𝕜] F, \\ ContDiffOn 𝕜 n f' s \\wedge \\forall x, x \\in s \\to HasFDerivWithinAt f (f' x) s x) \\ (\\text{and a differentiability/analyticity condition})$$$
Lean4
/-- A function is `C^(n + 1)` on a domain with unique derivatives if and only if it is
differentiable there, and its derivative (expressed with `fderivWithin`) is `C^n`. -/
theorem contDiffOn_succ_iff_fderivWithin (hs : UniqueDiffOn 𝕜 s) :
ContDiffOn 𝕜 (n + 1) f s ↔
DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f s) s :=
by
refine ⟨fun H => ?_, fun h => contDiffOn_succ_of_fderivWithin h.1 h.2.1 h.2.2⟩
refine ⟨H.differentiableOn le_add_self, ?_, fun x hx => ?_⟩
· rintro rfl
exact H.analyticOn
have A (m : ℕ) (hm : m ≤ n) : ContDiffWithinAt 𝕜 m (fun y => fderivWithin 𝕜 f s y) s x :=
by
rcases
(contDiffWithinAt_succ_iff_hasFDerivWithinAt (n := m) (ne_of_beq_false rfl)).1
(H.of_le (add_le_add_right hm 1) x hx) with
⟨u, hu, -, f', hff', hf'⟩
rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
rw [inter_comm, insert_eq_of_mem hx] at ho
have := hf'.mono ho
rw [contDiffWithinAt_inter' (mem_nhdsWithin_of_mem_nhds (IsOpen.mem_nhds o_open xo))] at this
apply this.congr_of_eventuallyEq_of_mem _ hx
have : o ∩ s ∈ 𝓝[s] x := mem_nhdsWithin.2 ⟨o, o_open, xo, Subset.refl _⟩
rw [inter_comm] at this
refine Filter.eventuallyEq_of_mem this fun y hy => ?_
have A : fderivWithin 𝕜 f (s ∩ o) y = f' y := ((hff' y (ho hy)).mono ho).fderivWithin (hs.inter o_open y hy)
rwa [fderivWithin_inter (o_open.mem_nhds hy.2)] at A
match n with
| ω => exact (H.analyticOn.fderivWithin hs).contDiffOn hs (n := ω) x hx
| ∞ => exact contDiffWithinAt_infty.2 (fun m ↦ A m (mod_cast le_top))
| (n : ℕ) => exact A n le_rfl
