English
Let f1, f2 be real-valued functions defined on a set s, differentiable within s around x, with UniqueDiffOn(s) and x ∈ s. Then Δ[s](f1 + f2) equals Δ[s]f1 + Δ[s]f2 in a neighborhood of x restricted to s.
Русский
Пусть f1, f2 определены на s и достаточно гладкие внутри s near x; тогда в окрестности x внутри s выполняется сумма лаплацианов: Δ[s](f1 + f2) = Δ[s]f1 + Δ[s]f2.
LaTeX
$$$ (\Delta[s](f_1 + f_2)) = (\Delta[s]f_1) + (\Delta[s]f_2) \quad \text{в } \mathcal{N}_s(x). $$$
Lean4
/-- The Laplacian commutes with addition. -/
theorem _root_.ContDiffAt.laplacianWithin_add_nhdsWithin (h₁ : ContDiffWithinAt ℝ 2 f₁ s x)
(h₂ : ContDiffWithinAt ℝ 2 f₂ s x) (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) :
Δ[s](f₁ + f₂) =ᶠ[𝓝[s] x] (Δ[s]f₁) + Δ[s]f₂ :=
by
nth_rw 1 [← s.insert_eq_of_mem hx]
filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp), eventually_mem_nhdsWithin] with y h₁y h₂y h₃y
rw [s.insert_eq_of_mem hx] at h₃y
simp [h₁y.laplacianWithin_add h₂y hs h₃y]
