`BookProof.ChapterSolidHarmonic.laplacian_angular_mul_sum` {A : E → ℝ} {x e : E} (he : ‖e‖ = 1) {μ : ℕ} (n : ℕ) (h3 : Module.finrank ℝ E = 3) (hA : ContDiffAt ℝ 2 A x) (hharm : (Δ

Proved

BookProof.ChapterSolidHarmonic.laplacian_angular_mul_sum

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSolidHarmonic.

BookProof.ChapterSolidHarmonic.laplacian_angular_mul_sum {A : E → ℝ} {x e : E} (he : ‖e‖ = 1) {μ : ℕ} (n : ℕ) (h3 : Module.finrank ℝ E = 3) (hA : ContDiffAt ℝ 2 A x) (hharm : (Δ A) x = 0) (heuler : fderiv ℝ A x x = μ * A x) (haxis : fderiv ℝ A x e = 0) (g : ℕ → ℝ) (hrec : ∀ j : ℕ, ((j : ℝ) + 2) * ((j : ℝ) + 1) * g (j + 2) = -(((n : ℝ) - j) * ((n : ℝ) + j + 2 * μ + 1)) * g j) : (Δ fun y : E => ∑ m ∈ Finset.range (n / 2 + 1), g (n - 2 * m) * (A y * ((⟪e, y⟫_ℝ) ^ (n - 2 * m) * (‖y‖ ^ 2) ^ m))) x = 0

Formalization note: Lean 4 identifier BookProof.ChapterSolidHarmonic.laplacian_angular_mul_sum.

Preamble

-- Generated from ChapterSolidHarmonic.lean — theorem BookProof.ChapterSolidHarmonic.laplacian_angular_mul_sum
import Definitions.Def_ChapterRadialLaplacian
import Definitions.Def_ChapterLaplacianProduct
import Definitions.Def_ChapterSolidHarmonicTools
import Definitions.Def_ChapterLegendrePolynomial
import Mathlib
import Definitions.Def_ChapterSolidHarmonic
open BookProof.ChapterSolidHarmonic



open Laplacian InnerProductSpace Polynomial
open BookProof.ChapterRadialLaplacian BookProof.ChapterLaplacianProduct
open BookProof.ChapterSolidHarmonicTools BookProof.ChapterLegendrePolynomial
open scoped RealInnerProductSpace

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]

Formal statement

theorem BookProof.ChapterSolidHarmonic.laplacian_angular_mul_sum {A : E → ℝ} {x e : E} (he : ‖e‖ = 1) {μ : ℕ} (n : ℕ)
    (h3 : Module.finrank ℝ E = 3)
    (hA : ContDiffAt ℝ 2 A x) (hharm : (Δ A) x = 0)
    (heuler : fderiv ℝ A x x = μ * A x) (haxis : fderiv ℝ A x e = 0)
    (g : ℕ → ℝ)
    (hrec : ∀ j : ℕ, ((j : ℝ) + 2) * ((j : ℝ) + 1) * g (j + 2)
      = -(((n : ℝ) - j) * ((n : ℝ) + j + 2 * μ + 1)) * g j) :
    (Δ fun y : E => ∑ m ∈ Finset.range (n / 2 + 1),
        g (n - 2 * m) * (A y * ((⟪e, y⟫_ℝ) ^ (n - 2 * m) * (‖y‖ ^ 2) ^ m))) x = 0 := by sorry

View graph