English
The Cartesian product of C^n functions at a point is C^n: if hf : ContDiffWithinAt 𝕜 n f s x and hg : ContDiffWithinAt 𝕜 n g s x, then ContDiffWithinAt 𝕜 n (fun x => (f x, g x)) s x.
Русский
Доказательство: произведение двух функций в точке сохраняет гладкость; если f и g — C^n внутри s в x, то их пара — C^n внутри s в x.
LaTeX
$$$ \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n} f\,s\,x \land \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n} g\,s\,x \Rightarrow \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n} (\lambda y. (f y, g y))\,s\,x$$$
Lean4
/-- The composition of `C^n` functions at points in domains is `C^n`. -/
theorem comp {s : Set E} {t : Set F} {g : F → G} {f : E → F} (x : E) (hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x) (st : MapsTo f s t) : ContDiffWithinAt 𝕜 n (g ∘ f) s x := by
match n with
| ω =>
have h'f : ContDiffWithinAt 𝕜 ω f s x := hf
obtain ⟨u, hu, p, hp, h'p⟩ := h'f
obtain ⟨v, hv, q, hq, h'q⟩ := hg
let w := insert x s ∩ (u ∩ f ⁻¹' v)
have wv : w ⊆ f ⁻¹' v := fun y hy => hy.2.2
have wu : w ⊆ u := fun y hy => hy.2.1
refine ⟨w, ?_, fun y ↦ (q (f y)).taylorComp (p y), hq.comp (hp.mono wu) wv, ?_⟩
· apply inter_mem self_mem_nhdsWithin (inter_mem hu ?_)
apply (continuousWithinAt_insert_self.2 hf.continuousWithinAt).preimage_mem_nhdsWithin'
apply nhdsWithin_mono _ _ hv
simp only [image_insert_eq]
apply insert_subset_insert
exact image_subset_iff.mpr st
· have : AnalyticOn 𝕜 f w :=
by
have : AnalyticOn 𝕜 (fun y ↦ (continuousMultilinearCurryFin0 𝕜 E F).symm (f y)) w :=
((h'p 0).mono wu).congr fun y hy ↦ (hp.zero_eq' (wu hy)).symm
have :
AnalyticOn 𝕜
(fun y ↦ (continuousMultilinearCurryFin0 𝕜 E F) ((continuousMultilinearCurryFin0 𝕜 E F).symm (f y))) w :=
AnalyticOnNhd.comp_analyticOn (LinearIsometryEquiv.analyticOnNhd _ _) this (mapsTo_univ _ _)
simpa using this
exact analyticOn_taylorComp h'q (fun n ↦ (h'p n).mono wu) this wv
| (n : ℕ∞) =>
intro m hm
rcases hf m hm with ⟨u, hu, p, hp⟩
rcases hg m hm with ⟨v, hv, q, hq⟩
let w := insert x s ∩ (u ∩ f ⁻¹' v)
have wv : w ⊆ f ⁻¹' v := fun y hy => hy.2.2
have wu : w ⊆ u := fun y hy => hy.2.1
refine ⟨w, ?_, fun y ↦ (q (f y)).taylorComp (p y), hq.comp (hp.mono wu) wv⟩
apply inter_mem self_mem_nhdsWithin (inter_mem hu ?_)
apply (continuousWithinAt_insert_self.2 hf.continuousWithinAt).preimage_mem_nhdsWithin'
apply nhdsWithin_mono _ _ hv
simp only [image_insert_eq]
apply insert_subset_insert
exact image_subset_iff.mpr st
