Homogeneous kernels with spherical mean zero integrate to zero on annuli

Proved

DbarRegularity.setIntegral_annulus_div_norm_pow_eq_zero

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

harmonic-analysismeasure-theorysingular-integrals

Let $d\ge0$ and let $\Omega:\mathbb{R}^d\to\mathbb{C}$ be homogeneous of degree $0$ , i.e. $\Omega(tx)=\Omega(x)$ for all $x$ and all $t>0$ , with mean zero on the unit sphere: $\int_{S^{d-1}}\Omega\,d\sigma=0$ . Then for all $0<R_1$ and all $R_2$

\int_{R_1<|x|<R_2}\frac{\Omega(x)}{|x|^d}\,dx=0 .

Formalization Note. $\mathbb{R}^d$ is EuclideanSpace ℝ (Fin d) with volume; $\sigma$ is Mathlib's volume.toSphere on sphere 0 1. The integrals are Bochner integrals, so no measurability or integrability of $\Omega$ is assumed (a non-integrable integrand has Bochner integral $0$ ). $|x|^d$ is the real power ‖x‖ ^ d cast to ℂ.

Preamble

import Mathlib.MeasureTheory.Constructions.HaarToSphere
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
import Mathlib.MeasureTheory.Integral.Prod
import Mathlib.Analysis.InnerProductSpace.PiL2

Formal statement

namespace DbarRegularity

open MeasureTheory Set Metric
open scoped ENNReal

/-- If `Ω` on `ℝ^d` is homogeneous of degree `0` and has mean zero on the unit sphere, then
`Ω(x) / |x|^d` has integral zero over every annulus `{R₁ < |x| < R₂}`. -/
theorem setIntegral_annulus_div_norm_pow_eq_zero {d : ℕ} (Ω : EuclideanSpace ℝ (Fin d) → ℂ)
    (hhom : ∀ x, ∀ t : ℝ, 0 < t → Ω (t • x) = Ω x)
    (hmean : ∫ x : sphere (0 : EuclideanSpace ℝ (Fin d)) 1, Ω x ∂(volume.toSphere) = 0)
    (R₁ R₂ : ℝ) (hR₁ : 0 < R₁) :
    ∫ x in {x : EuclideanSpace ℝ (Fin d) | R₁ < ‖x‖ ∧ ‖x‖ < R₂},
      Ω x / ((‖x‖ ^ d : ℝ) : ℂ) = 0 := by sorry

end DbarRegularity

Source

E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), Chapter II, § 4.2, Theorem 3, p. 39

View graph