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