English
Composition on the right with a linear map preserves ContDiffWithinAt: f ∘ g has ContDiffWithinAt given f does.
Русский
Композиция справа линейного отображения сохраняет ContDiffWithinAt: если f обладает свойством, то f ∘ g тоже имеет его.
LaTeX
$$$\forall g:\, G \to_L[\mathbb{K}] E,\; ContDiffWithinAt 𝕜 n f s (g x) \Rightarrow ContDiffWithinAt 𝕜 n (f\circ g) s x$$$
Lean4
/-- Composition by continuous linear maps on the right preserves `C^n` functions at a point on
a domain. -/
theorem comp_continuousLinearMap {x : G} (g : G →L[𝕜] E) (hf : ContDiffWithinAt 𝕜 n f s (g x)) :
ContDiffWithinAt 𝕜 n (f ∘ g) (g ⁻¹' s) x := by
match n with
| ω =>
obtain ⟨u, hu, p, hp, h'p⟩ := hf
refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g, ?_⟩
· refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)
· intro i
change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.compContinuousLinearMapL (fun _ ↦ g) (p (g x) i)) (⇑g ⁻¹' u)
apply AnalyticOn.comp _ _ (Set.mapsTo_univ _ _)
· exact ContinuousLinearMap.analyticOn _ _
· exact (h'p i).comp (g.analyticOn _) (mapsTo_preimage _ _)
| (n : ℕ∞) =>
intro m hm
rcases hf m hm with ⟨u, hu, p, hp⟩
refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g⟩
refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)
