laplacian_CLM_comp_left — Mathlib

English

Let l be a continuous linear map and f be ContDiffWithinAt Real 2 on s at x. Then Δ[s](l ∘ f) =ᶠ[𝓝[s] x] l ∘ Δ[s]f, i.e., the equality holds eventually in nhds within s.

Русский

Пусть l непрерывно линейно отображает F→G и f удовлетворяет ContDiffWithinAt Real 2 на s в x. Тогда Δ[s](l ∘ f) =ᶠ 𝓝[s]x l ∘ Δ[s]f.

LaTeX

$$$ Δ[s](l \circ f) =^{}_{𝓝[s]x} l \circ (Δ[s]f). $$$

Lean4

/-- The Laplacian commutes with left composition by continuous linear maps. -/
theorem _root_.ContDiffAt.laplacian_CLM_comp_left {l : F →L[ℝ] G} (h : ContDiffAt ℝ 2 f x) :
    Δ (l ∘ f) x = (l ∘ (Δ f)) x := by
  simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, l.iteratedFDeriv_comp_left h]

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