laplacian_smul_nhds — Mathlib

English

Let v ∈ ℝ and f be ContDiffWithinAt Real 2 f x; then Δ(v·f) equals v times Δf in a neighborhood of x (nhds).

Русский

Пусть v ∈ ℝ и f удовлетворяет ContDiffWithinAt Real 2 в окрестности x; тогда Δ(f) в окрестности x масштабируется скалярно: Δ(v·f) = v·Δf в nhds.

LaTeX

$$$ Δ(v \cdot f) =^{}_{\ nhds x} v \cdot (Δ f). $$$

Lean4

/-- The Laplacian commutes with scalar multiplication. -/
theorem laplacian_smul_nhds (v : ℝ) (h : ContDiffAt ℝ 2 f x) : Δ (v • f) =ᶠ[𝓝 x] v • (Δ f) :=
  by
  filter_upwards [h.eventually (by simp)] with a ha
  simp [laplacian_smul v ha]

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