Second coordinate moments of unit-sphere surface measure

Proved

MeasureTheory.integral_sphere_coordinate_mul

by Mazecto · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

integration-by-partsnewtonian-potentialpde

For $n\ge1$ , surface measure on the unit sphere satisfies

\int_{S^{n-1}}\omega_i\omega_j\,dS(\omega)=\alpha_n\delta_{ij},

where $\alpha_n$ is the volume of the unit ball. Equivalently, the normalized second moment is $\delta_{ij}/n$ . This is the spherical symmetry computation in Hunter Corollary 2.27, p. 39. It also follows from the ball divergence theorem applied to the linear coordinate function $y\mapsto y_i$ in direction $e_j$ .

Preamble

import Definitions.Def_HunterPDE_Newtonian_FundamentalSolution
import Mathlib.MeasureTheory.Constructions.HaarToSphere
import Mathlib.MeasureTheory.Integral.Bochner.Basic
open MeasureTheory

Formal statement

theorem MeasureTheory.integral_sphere_coordinate_mul (n : ℕ) (hn : 0 < n) (i j : Fin n) :
    (∫ w : Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1,
      w.1 i * w.1 j ∂volume.toSphere) =
      HunterPDE.Newtonian.unitBallVolume n * (if i = j then 1 else 0) := by sorry

Source

Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/ch2.pdf, pp. 37–39, Theorem 2.26 Eqs. (2.25)–(2.28), Corollary 2.27 Eq. (2.29).

View graph