laplacian_add — Mathlib

English

Let h1, h2 be real-valued C^2 functions at a point x. Then the Laplacian at x is additive: Δ(h1 + h2)(x) = Δ(h1)(x) + Δ(h2)(x).

Русский

Пусть h1, h2 — функции, для которых существует лаплациан в точке x; тогда в точке x лаплациан суммируется: Δ(h1 + h2)(x) = Δ(h1)(x) + Δ(h2)(x).

LaTeX

$$$ \Delta (f_1 + f_2)(x) = \Delta f_1(x) + \Delta f_2(x). $$$

Lean4

/-- The Laplacian commutes with addition. -/
theorem _root_.ContDiffAt.laplacian_add (h₁ : ContDiffAt ℝ 2 f₁ x) (h₂ : ContDiffAt ℝ 2 f₂ x) :
    Δ (f₁ + f₂) x = Δ f₁ x + Δ f₂ x := by
  simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, ← Finset.sum_add_distrib, iteratedFDeriv_add_apply h₁ h₂]

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