laplacianWithin_CLM_comp_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The Laplacian commutes with left composition by continuous linear maps. -/
theorem _root_.ContDiffWithinAt.laplacianWithin_CLM_comp_left {l : F →L[ℝ] G} (h : ContDiffWithinAt ℝ 2 f s x)
    (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) : (Δ[s](l ∘ f)) x = (l ∘ (Δ[s]f)) x := by
  simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx, l.iteratedFDerivWithin_comp_left h hs hx]

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