The tail integral of a negative power of the distance

In a pseudometric measure space whose balls of radius r > R satisfy the growth bound μ (ball y r) ≤ A rⁿ (with A : ℝ≥0∞), the tail integral of x ↦ dist x y ^ (-s) obeys, for 0 ≤ s, n < s and R > 0, the extended-valued bound

∫_{dist x y > R} dist x y ^ (-s) dx ≤ A 2ⁿ R ^ (n - s) / (1 - 2 ^ (n - s))

(TauCeti.setLIntegral_ofReal_dist_rpow_neg_le). When A < ∞ the right-hand side is finite, so dist x y ^ (-s) is integrable on {x | R < dist x y}. The exponent n need not be an integer. For an additive Haar measure on a finite-dimensional real normed space the growth bound holds with n the dimension and A the measure of the unit ball (MeasureTheory.Measure.setLIntegral_ofReal_norm_rpow_neg_le).

The proof splits the region dist x y > R into the dyadic annuli 2ᵏ R ≤ dist x y < 2ᵏ⁺¹ R. On the k-th annulus dist x y ^ (-s) is at most (2ᵏ R) ^ (-s), and the annulus lies in a ball of measure at most A (2ᵏ⁺¹ R)ⁿ, so the annuli contribute a convergent geometric series with ratio 2 ^ (n - s).

Main declarations

• TauCeti.setLIntegral_ofReal_dist_rpow_neg_le: the tail bound for dist x y ^ (-s).
• MeasureTheory.Measure.setLIntegral_ofReal_norm_rpow_neg_le: the tail bound for ‖x‖ ^ (-s) under an additive Haar measure, for s above the dimension.

theorem TauCeti.setLIntegral_ofReal_dist_rpow_neg_le {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} {y : X} {A : ENNReal} {n s R : ℝ} (hμ : ∀ (r : ℝ), R < r → μ (Metric.ball y r) ≤ A * ENNReal.ofReal (r ^ n)) (hs : 0 ≤ s) (hns : n < s) (hR : 0 < R) : ∫⁻ (x : X) in {x : X | R < dist x y}, ENNReal.ofReal (dist x y ^ (-s)) ∂μ ≤ A * ENNReal.ofReal (2 ^ n / (1 - 2 ^ (n - s)) * R ^ (n - s))

The tail of a power of the distance. If the balls about y of radius r > R satisfy the growth bound μ (ball y r) ≤ A rⁿ, then for 0 ≤ s, n < s and R > 0,

∫_{dist x y > R} dist x y ^ (-s) dx ≤ A 2ⁿ R ^ (n - s) / (1 - 2 ^ (n - s)).

theorem MeasureTheory.Measure.setLIntegral_ofReal_norm_rpow_neg_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] {s : ℝ} (hs : ↑(Module.finrank ℝ E) < s) {R : ℝ} (hR : 0 < R) : ∫⁻ (x : E) in {x : E | R < ‖x‖}, ENNReal.ofReal (‖x‖ ^ (-s)) ∂μ ≤ μ (Metric.ball 0 1) * ENNReal.ofReal (2 ^ ↑(Module.finrank ℝ E) / (1 - 2 ^ (↑(Module.finrank ℝ E) - s)) * R ^ (↑(Module.finrank ℝ E) - s))

The tail of a negative power of the norm. For an additive Haar measure μ on a finite-dimensional real normed space of dimension n, n < s and R > 0,

∫_{‖x‖ > R} ‖x‖ ^ (-s) dx ≤ μ (B(0, 1)) 2ⁿ R ^ (n - s) / (1 - 2 ^ (n - s)).