Prove2Me

Tail bound ∫∣x∣≥R∣x∣−(d+1) dx≤Cd/R\int_{|x|\ge R}|x|^{-(d+1)}\,dx\le C_d/R in Rd\mathbb R^d

Proved
DbarRegularity.lintegral_inv_norm_pow_succ_le

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

harmonic-analysismeasure-theoryreal-analysis

Let d≥0d\ge 0. There is a constant CC, depending only on dd, such that for every R>0R>0

∫{x∈Rd: ∣x∣≥R}dx∣x∣d+1  ≤  CR.\int_{\{x\in\mathbb R^d:\ |x|\ge R\}}\frac{dx}{|x|^{d+1}}\;\le\;\frac{C}{R}.

This is the scale-invariant decay of the tail of ∣x∣−(d+1)|x|^{-(d+1)}, the integrability exponent one above the dimension; it is the basic size estimate for kernels whose gradient decays like ∣x∣−(d+1)|x|^{-(d+1)}.

Formalization Note. Rd\mathbb R^d is EuclideanSpace ℝ (Fin d) with Lebesgue measure volume. The integrand is written as ENNReal.ofReal ((‖x‖ ^ (d + 1))⁻¹) and the integral is the lower Lebesgue integral ∫⁻ over the set {x | R ≤ ‖x‖}; the bound is ENNReal.ofReal (C / R) with a real constant C chosen before R.

Preamble
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
import Mathlib.Analysis.SpecialFunctions.JapaneseBracket
import Mathlib.Analysis.InnerProductSpace.PiL2
Formal statement
namespace DbarRegularity

open MeasureTheory Set
open scoped ENNReal

/-- In `ℝ^d`, the tail integral of `|x|^{-(d+1)}` over `{|x| ≥ R}` is bounded by `C / R`, with a
constant `C` depending only on `d`. -/
theorem lintegral_inv_norm_pow_succ_le (d : ℕ) :
    ∃ C : ℝ, ∀ R : ℝ, 0 < R →
      ∫⁻ x in {x : EuclideanSpace ℝ (Fin d) | R ≤ ‖x‖}, ENNReal.ofReal ((‖x‖ ^ (d + 1))⁻¹)
        ≤ ENNReal.ofReal (C / R) := by sorry

end DbarRegularity
Source
E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton University Press (1970), Chapter II, § 2.2, p. 29

View graph