English
For n finite, ContDiffWithinAt (n+1) f s x is equivalent to the existence of a neighborhood u of x in insert x s with a derivative within s, together with a differentiability condition for f' and ContDiffWithinAt n f' within u.
Русский
Для конечного n, ContDiffWithinAt (n+1) f s x эквивалентно существованию окрестности u и производной внутри s.
LaTeX
$$$\text{ContDiffWithinAt}_{\mathbb{K}}(n+1,f;s;x) \iff \exists u \in \mathcal{N}[insert\ x\ s]x,\; u \subset insert\ x\ s \land \Big( \text{...} \Big)$$$
Lean4
/-- A function is `C^(n + 1)` on a domain iff locally, it has a derivative which is `C^n`
(and moreover the function is analytic when `n = ω`). -/
theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt (hn : n ≠ ∞) :
ContDiffWithinAt 𝕜 (n + 1) f s x ↔
∃ u ∈ 𝓝[insert x s] x,
(n = ω → AnalyticOn 𝕜 f u) ∧
∃ f' : E → E →L[𝕜] F, (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x :=
by
have h'n : n + 1 ≠ ∞ := by simpa using hn
constructor
· intro h
rcases (contDiffWithinAt_iff_of_ne_infty h'n).1 h with ⟨u, hu, p, Hp, H'p⟩
refine
⟨u, hu, ?_, fun y => (continuousMultilinearCurryFin1 𝕜 E F) (p y 1), fun y hy =>
Hp.hasFDerivWithinAt le_add_self hy, ?_⟩
· rintro rfl
exact Hp.analyticOn (H'p rfl 0)
apply (contDiffWithinAt_iff_of_ne_infty hn).2
refine ⟨u, ?_, fun y : E => (p y).shift, ?_⟩
· convert @self_mem_nhdsWithin _ _ x u
have : x ∈ insert x s := by simp
exact insert_eq_of_mem (mem_of_mem_nhdsWithin this hu)
· rw [hasFTaylorSeriesUpToOn_succ_iff_right] at Hp
refine ⟨Hp.2.2, ?_⟩
rintro rfl i
change AnalyticOn 𝕜 (fun x ↦ (continuousMultilinearCurryRightEquiv' 𝕜 i E F) (p x (i + 1))) u
apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn ?_ (Set.mapsTo_univ _ _)
exact H'p rfl _
· rintro ⟨u, hu, hf, f', f'_eq_deriv, Hf'⟩
rw [contDiffWithinAt_iff_of_ne_infty h'n]
rcases (contDiffWithinAt_iff_of_ne_infty hn).1 Hf' with ⟨v, hv, p', Hp', p'_an⟩
refine ⟨v ∩ u, ?_, fun x => (p' x).unshift (f x), ?_, ?_⟩
· apply Filter.inter_mem _ hu
apply nhdsWithin_le_of_mem hu
exact nhdsWithin_mono _ (subset_insert x u) hv
· rw [hasFTaylorSeriesUpToOn_succ_iff_right]
refine ⟨fun y _ => rfl, fun y hy => ?_, ?_⟩
· change
HasFDerivWithinAt (fun z => (continuousMultilinearCurryFin0 𝕜 E F).symm (f z))
(FormalMultilinearSeries.unshift (p' y) (f y) 1).curryLeft (v ∩ u) y
rw [← Function.comp_def _ f, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']
convert (f'_eq_deriv y hy.2).mono inter_subset_right
rw [← Hp'.zero_eq y hy.1]
ext z
change ((p' y 0) (init (@cons 0 (fun _ => E) z 0))) (@cons 0 (fun _ => E) z 0 (last 0)) = ((p' y 0) 0) z
congr
norm_num [eq_iff_true_of_subsingleton]
· convert (Hp'.mono inter_subset_left).congr fun x hx => Hp'.zero_eq x hx.1 using 1
· ext x y
change p' x 0 (init (@snoc 0 (fun _ : Fin 1 => E) 0 y)) y = p' x 0 0 y
rw [init_snoc]
· ext x k v y
change
p' x k (init (@snoc k (fun _ : Fin k.succ => E) v y)) (@snoc k (fun _ : Fin k.succ => E) v y (last k)) =
p' x k v y
rw [snoc_last, init_snoc]
· intro h i
simp only [WithTop.add_eq_top, WithTop.one_ne_top, or_false] at h
match i with
| 0 =>
simp only [FormalMultilinearSeries.unshift]
apply AnalyticOnNhd.comp_analyticOn _ ((hf h).mono inter_subset_right) (Set.mapsTo_univ _ _)
exact LinearIsometryEquiv.analyticOnNhd _ _
| i + 1 =>
simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one]
apply AnalyticOnNhd.comp_analyticOn _ ((p'_an h i).mono inter_subset_left) (Set.mapsTo_univ _ _)
exact LinearIsometryEquiv.analyticOnNhd _ _
