English
Let f1, f2 be functions whose Laplacians are defined on a set s with a regular differentiability condition, and assume s has unique differentiability and x ∈ s. Then the Laplacian within s is additive: the Laplacian of f1 + f2 at x equals the sum of the Laplacians of f1 and f2 at x.
Русский
Пусть f1, f2 — функции, для которых внутри множества s определён Laplacian, при условии, что f₁ и f₂ достаточно гладкие в пределах s, и что s имеет уникальную дифференцируемость; пусть x ∈ s. Тогда лаплациан внутри s суммируется: Δ[s](f₁ + f₂) на x равно Δ[s]f₁ на x плюс Δ[s]f₂ на x.
LaTeX
$$$ x \in s \implies \Delta[s](f_1 + f_2)(x) = (\Delta[s]f_1)(x) + (\Delta[s]f_2)(x) $$$
Lean4
/-- The Laplacian commutes with addition. -/
theorem _root_.ContDiffWithinAt.laplacianWithin_add (h₁ : ContDiffWithinAt ℝ 2 f₁ s x)
(h₂ : ContDiffWithinAt ℝ 2 f₂ s x) (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) :
(Δ[s](f₁ + f₂)) x = (Δ[s]f₁) x + (Δ[s]f₂) x := by
simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx, ← Finset.sum_add_distrib,
iteratedFDerivWithin_add_apply h₁ h₂ hs hx]
