laplacian_add_nhds — Mathlib

English

Let f1, f2 be functions with ContDiffAt Real 2 at x. Then the Laplacian at x is additive: Δ(f1 + f2)(x) = Δ f1(x) + Δ f2(x).

Русский

Пусть f1, f2 гладкие до второй производной в точке x; тогда в точке x выполняется линейность лаплациана: Δ(f1+f2)(x) = Δ f1(x) + Δ f2(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_nhds (h₁ : ContDiffAt ℝ 2 f₁ x) (h₂ : ContDiffAt ℝ 2 f₂ x) :
    Δ (f₁ + f₂) =ᶠ[𝓝 x] (Δ f₁) + (Δ f₂) :=
  by
  filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp)] with x h₁x h₂x
  exact h₁x.laplacian_add h₂x

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