laplacianWithin_CLM_comp_left_nhds

English

Let l be a continuous linear map (F →L G). Then the Laplacian commutes with left composition: Δ (l ∘ f) x = l (Δ f) x for all x.

Русский

Пусть l — непрерывное линейное отображение F→G. Тогда лаплациан слева коммутирует: Δ(l ∘ f)(x) = l(Δ f)(x).

LaTeX

$$$ \Delta(l \circ f)(x) = l(\Delta f)(x). $$$

Lean4

/-- The Laplacian commutes with left composition by continuous linear maps. -/
theorem _root_.ContDiffWithinAt.laplacianWithin_CLM_comp_left_nhds {l : F →L[ℝ] G} (h : ContDiffWithinAt ℝ 2 f s x)
    (hs : UniqueDiffOn ℝ s) : Δ[s](l ∘ f) =ᶠ[𝓝[s] x] l ∘ Δ[s]f := by
  filter_upwards [(h.eventually (by simp)).filter_mono (nhdsWithin_mono _ (Set.subset_insert ..)),
    eventually_mem_nhdsWithin] with a h₁a using h₁a.laplacianWithin_CLM_comp_left hs

Похожие утверждения