laplacianWithin_smul — Mathlib

English

If f is differentiable within s at x and v ∈ ℝ is a scalar, then the Laplacian within s commutes with scalar multiplication: Δ[s](v · f) at x equals v times Δ[s]f at x.

Русский

Если f гладкая внутри s в точке x и v — скаляр, тогда лаплациан внутри s commute с умножением на скаляр: Δ[s](v f)(x) = v Δ[s]f(x).

LaTeX

$$$ (\Delta[s](v \cdot f)) x = v \cdot (\Delta[s]f) x. $$$

Lean4

/-- The Laplacian commutes with scalar multiplication. -/
theorem laplacianWithin_smul (v : ℝ) (hf : ContDiffWithinAt ℝ 2 f s x) (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) :
    (Δ[s](v • f)) x = v • (Δ[s]f) x := by
  simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx,
    iteratedFDerivWithin_const_smul_apply hf hs hx, Finset.smul_sum]

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