Harmonic polynomials and the Fischer decomposition

For finitely many variables X₁, …, Xₙ, the Laplacian of a polynomial is Δ p = ∑ᵢ ∂²p/∂Xᵢ² and r² = ∑ᵢ Xᵢ² is the polynomial giving the squared Euclidean norm. A polynomial is harmonic when its Laplacian vanishes. This file develops the finite algebra of harmonic homogeneous polynomials that underlies spherical harmonics: over ℝ, a harmonic homogeneous polynomial of degree d in n variables restricts to an eigenfunction of the Laplacian of the unit sphere S^(n-1), with eigenvalue d(d + n - 2). That restriction is not treated here.

Writing P_d for the homogeneous polynomials of degree d and H_d ⊆ P_d for the harmonic ones, the Laplacian maps P_d to P_(d-2), and for q ∈ P_e the product rule and Euler's identity give

Δ (r² q) = r² Δ q + (2n + 4e) q,

and hence, for h ∈ H_l, Δ (r^(2(k+1)) h) = 2(k+1)(2l + n + 2k) r^(2k) h. Over a field of characteristic zero and with at least one variable, the operator q ↦ Δ (r² q) is bijective on P_e, which yields the Fischer decomposition

P_(e+2) = H_(e+2) ⊕ r² P_e,

and the dimension formula dim H_(e+2) = dim P_(e+2) - dim P_e. Since every polynomial of degree at most one is harmonic, H_d = P_d for d ≤ 1. Iterating the decomposition writes every homogeneous polynomial as a sum of harmonic ones multiplied by powers of r².

The Laplacian is defined as a linear map on polynomials rather than through the analytic notation class Laplacian, so that this file stays purely algebraic.

Main definitions

• MvPolynomial.laplacian: the Laplacian ∑ᵢ ∂²/∂Xᵢ² on polynomials in finitely many variables.
• MvPolynomial.normSq: the polynomial r² = ∑ᵢ Xᵢ².
• MvPolynomial.harmonicSubmodule σ R d: the harmonic homogeneous polynomials of degree d.

Main results

• MvPolynomial.laplacian_mul: the product rule Δ (p q) = Δ p q + 2 ∑ᵢ ∂ᵢp ∂ᵢq + p Δ q.
• MvPolynomial.IsHomogeneous.laplacian: the Laplacian lowers the degree by two.
• MvPolynomial.laplacian_normSq_mul: Δ (r² q) = r² Δ q + (2n + 4e) q for q ∈ P_e.
• MvPolynomial.laplacian_normSq_pow_mul: Δ (r^(2(k+1)) h) = 2(k+1)(2l + n + 2k) r^(2k) h for h ∈ H_l.
• MvPolynomial.eq_zero_of_laplacian_normSq_mul_eq_zero and MvPolynomial.exists_laplacian_normSq_mul_eq: q ↦ Δ (r² q) is bijective on P_e.
• MvPolynomial.harmonicSubmodule_sup_map_mulLeft_normSq and MvPolynomial.disjoint_ker_laplacian_map_mulLeft_normSq: the Fischer decomposition P_(e+2) = H_(e+2) ⊕ r² P_e.
• MvPolynomial.homogeneousSubmodule_eq_iSup_map_mulLeft_normSq_pow: iterating, every homogeneous polynomial of degree d is a sum ∑_{k ≤ d/2} r^(2k) h_k with h_k ∈ H_(d-2k).
• MvPolynomial.finrank_harmonicSubmodule_add_finrank, MvPolynomial.finrank_harmonicSubmodule_add_two and MvPolynomial.finrank_harmonicSubmodule_of_le_one: the dimension of H_d, in terms of the multichoose numbers dim P_d = n.multichoose d.

References

• S. Axler, P. Bourdon and W. Ramey, Harmonic Function Theory, 2nd ed., Springer GTM 137 (2001), Chapter 5 (harmonic polynomials and the decomposition of homogeneous polynomials).
• E. M. Stein and G. Weiss, Introduction to Fourier Analysis on Euclidean Spaces, Princeton University Press (1971), Chapter IV, Section 2 (spherical harmonics).

noncomputable def MvPolynomial.laplacian {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] : MvPolynomial σ R →ₗ[R] MvPolynomial σ R

The Laplacian Δ p = ∑ᵢ ∂²p/∂Xᵢ² of a polynomial in finitely many variables.

theorem MvPolynomial.laplacian_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] (p : MvPolynomial σ R) : laplacian p = ∑ i : σ, (pderiv i) ((pderiv i) p)

@[simp]

theorem MvPolynomial.laplacian_C {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] (a : R) : laplacian (C a) = 0

theorem MvPolynomial.laplacian_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] (p q : MvPolynomial σ R) : laplacian (p * q) = laplacian p * q + 2 * ∑ i : σ, (pderiv i) p * (pderiv i) q + p * laplacian q

The product rule for the Laplacian: Δ (p q) = Δ p q + 2 ∑ᵢ ∂ᵢp ∂ᵢq + p Δ q.

theorem MvPolynomial.IsHomogeneous.laplacian {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] {p : MvPolynomial σ R} {n : ℕ} (hp : p.IsHomogeneous n) : (laplacian p).IsHomogeneous (n - 2)

The Laplacian lowers the degree of a homogeneous polynomial by two.

theorem MvPolynomial.IsHomogeneous.laplacian_eq_zero_of_le_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] {p : MvPolynomial σ R} {n : ℕ} (hp : p.IsHomogeneous n) (hn : n ≤ 1) : laplacian p = 0

A homogeneous polynomial of degree at most one is harmonic.

@[simp]

theorem MvPolynomial.laplacian_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] (j : σ) : laplacian (X j) = 0

noncomputable def MvPolynomial.normSq (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] : MvPolynomial σ R

The polynomial r² = ∑ᵢ Xᵢ² giving the squared Euclidean norm.

theorem MvPolynomial.normSq_def (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] : normSq σ R = ∑ i : σ, X i ^ 2

@[simp]

theorem MvPolynomial.eval_normSq (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (x : σ → R) : (eval x) (normSq σ R) = ∑ i : σ, x i ^ 2

theorem MvPolynomial.isHomogeneous_normSq (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] : (normSq σ R).IsHomogeneous 2

theorem MvPolynomial.normSq_ne_zero (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] [Nontrivial R] [Nonempty σ] : normSq σ R ≠ 0

normSq is a nonzero polynomial as soon as there is a variable.

@[simp]

theorem MvPolynomial.pderiv_normSq {σ : Type u_1} (R : Type u_2) [CommSemiring R] [Fintype σ] (i : σ) : (pderiv i) (normSq σ R) = 2 * X i

@[simp]

theorem MvPolynomial.laplacian_normSq {σ : Type u_1} (R : Type u_2) [CommSemiring R] [Fintype σ] : laplacian (normSq σ R) = 2 * ↑(Fintype.card σ)

theorem MvPolynomial.laplacian_normSq_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] {q : MvPolynomial σ R} {e : ℕ} (hq : q.IsHomogeneous e) : laplacian (normSq σ R * q) = normSq σ R * laplacian q + (2 * Fintype.card σ + 4 * e) • q

The Laplacian of r² q: for q homogeneous of degree e in n variables, Δ (r² q) = r² Δ q + (2n + 4e) q.

theorem MvPolynomial.laplacian_normSq_pow_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] {h : MvPolynomial σ R} {l : ℕ} (hh : h.IsHomogeneous l) (hΔ : laplacian h = 0) (k : ℕ) : laplacian (normSq σ R ^ (k + 1) * h) = (2 * (k + 1) * (2 * l + Fintype.card σ + 2 * k)) • (normSq σ R ^ k * h)

The Laplacian of r^(2(k+1)) h: for h harmonic and homogeneous of degree l in n variables, Δ (r^(2(k+1)) h) = 2(k+1)(2l + n + 2k) r^(2k) h.

noncomputable def MvPolynomial.harmonicSubmodule (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (d : ℕ) : Submodule R (MvPolynomial σ R)

The harmonic homogeneous polynomials of degree d: the homogeneous polynomials of degree d whose Laplacian vanishes.

@[simp]

theorem MvPolynomial.mem_harmonicSubmodule_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] {d : ℕ} {p : MvPolynomial σ R} : p ∈ harmonicSubmodule σ R d ↔ p.IsHomogeneous d ∧ laplacian p = 0

theorem MvPolynomial.harmonicSubmodule_le_homogeneousSubmodule {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] (d : ℕ) : harmonicSubmodule σ R d ≤ homogeneousSubmodule σ R d

theorem MvPolynomial.harmonicSubmodule_eq_of_le_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] {d : ℕ} (hd : d ≤ 1) : harmonicSubmodule σ R d = homogeneousSubmodule σ R d

In degree at most one every homogeneous polynomial is harmonic.

theorem MvPolynomial.finrank_harmonicSubmodule_of_le_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] [StrongRankCondition R] {d : ℕ} (hd : d ≤ 1) : Module.finrank R ↥(harmonicSubmodule σ R d) = (Fintype.card σ).multichoose d

The dimension of the harmonic polynomials of degree d ≤ 1 in n variables is n.multichoose d, the dimension of all homogeneous polynomials of degree d.

instance MvPolynomial.instFiniteDimensionalSubtypeMemSubmoduleHarmonicSubmodule {σ : Type u_1} {K : Type u_3} [Field K] [Fintype σ] (d : ℕ) : FiniteDimensional K ↥(harmonicSubmodule σ K d)

theorem MvPolynomial.eq_zero_of_laplacian_normSq_mul_eq_zero {σ : Type u_1} {K : Type u_3} [Field K] [Fintype σ] [CharZero K] [Nonempty σ] {q : MvPolynomial σ K} {e : ℕ} (hq : q.IsHomogeneous e) (h : laplacian (normSq σ K * q) = 0) : q = 0

Injectivity of q ↦ Δ (r² q): over a field of characteristic zero and with at least one variable, if q is homogeneous and Δ (r² q) = 0, then q = 0.

theorem MvPolynomial.exists_laplacian_normSq_mul_eq {σ : Type u_1} {K : Type u_3} [Field K] [Fintype σ] [CharZero K] [Nonempty σ] {p : MvPolynomial σ K} {e : ℕ} (hp : p.IsHomogeneous e) : ∃ (q : MvPolynomial σ K), q.IsHomogeneous e ∧ laplacian (normSq σ K * q) = p

Surjectivity of q ↦ Δ (r² q): over a field of characteristic zero and with at least one variable, every homogeneous polynomial p of degree e is Δ (r² q) for a homogeneous polynomial q of degree e.

theorem MvPolynomial.disjoint_ker_laplacian_map_mulLeft_normSq {σ : Type u_1} {K : Type u_3} [Field K] [Fintype σ] [CharZero K] [Nonempty σ] (e : ℕ) : Disjoint laplacian.ker (Submodule.map (LinearMap.mulLeft K (normSq σ K)) (homogeneousSubmodule σ K e))

The Fischer decomposition, disjointness: a harmonic polynomial divisible by r² with homogeneous quotient is zero.

theorem MvPolynomial.harmonicSubmodule_sup_map_mulLeft_normSq {σ : Type u_1} {K : Type u_3} [Field K] [Fintype σ] [CharZero K] [Nonempty σ] (e : ℕ) : harmonicSubmodule σ K (e + 2) ⊔ Submodule.map (LinearMap.mulLeft K (normSq σ K)) (homogeneousSubmodule σ K e) = homogeneousSubmodule σ K (e + 2)

The Fischer decomposition: every homogeneous polynomial of degree e + 2 is the sum of a harmonic one and r² times a homogeneous polynomial of degree e. The sum is direct by MvPolynomial.disjoint_ker_laplacian_map_mulLeft_normSq.

theorem MvPolynomial.homogeneousSubmodule_eq_iSup_map_mulLeft_normSq_pow {σ : Type u_1} {K : Type u_3} [Field K] [Fintype σ] [CharZero K] [Nonempty σ] (d : ℕ) : homogeneousSubmodule σ K d = ⨆ (k : ℕ), ⨆ (_ : k ≤ d / 2), Submodule.map (LinearMap.mulLeft K (normSq σ K ^ k)) (harmonicSubmodule σ K (d - 2 * k))

The harmonic decomposition: every homogeneous polynomial of degree d is a sum ∑_{k ≤ d/2} r^(2k) h_k with each h_k harmonic and homogeneous of degree d - 2k.

theorem MvPolynomial.finrank_harmonicSubmodule_add_finrank {σ : Type u_1} {K : Type u_3} [Field K] [Fintype σ] [CharZero K] [Nonempty σ] (e : ℕ) : Module.finrank K ↥(harmonicSubmodule σ K (e + 2)) + Module.finrank K ↥(homogeneousSubmodule σ K e) = Module.finrank K ↥(homogeneousSubmodule σ K (e + 2))

The dimension of the harmonic polynomials: dim H_(e+2) + dim P_e = dim P_(e+2).

theorem MvPolynomial.finrank_harmonicSubmodule_add_two {σ : Type u_1} {K : Type u_3} [Field K] [Fintype σ] [CharZero K] [Nonempty σ] (e : ℕ) : Module.finrank K ↥(harmonicSubmodule σ K (e + 2)) = (Fintype.card σ).multichoose (e + 2) - (Fintype.card σ).multichoose e

The dimension of the harmonic polynomials of degree e + 2 in n variables is n.multichoose (e + 2) - n.multichoose e, that is C(n + e + 1, e + 2) - C(n + e - 1, e).