The integral and the moments of the Japanese bracket

Mathlib proves that x ↦ (1 + ‖x‖ ^ 2) ^ (-r / 2) is integrable on a finite-dimensional real normed space V of dimension d as soon as d < r (integrable_rpow_neg_one_add_norm_sq). When V is moreover a real inner product space, this file computes the integral against its canonical Lebesgue measure volume:

∫ x : V, (1 + ‖x‖ ^ 2) ^ (-r / 2) = π ^ (d / 2) Γ((r - d) / 2) / Γ(r / 2).

Integrating in polar coordinates and substituting u = ‖x‖ ^ 2 turns the integral into Euler's second beta integral ∫₀^∞ u ^ (a - 1) (1 + u) ^ (-(a + b)) du = Β(a, b) with a = d / 2 and b = (r - d) / 2 (TauCeti.integral_rpow_mul_one_add_rpow, in the radial form TauCeti.integral_rpow_mul_one_add_sq_rpow). For r = d + 1 this is the normalization of the multivariate Cauchy distribution and of the Poisson kernel of a half-space.

More generally, for every additive Haar measure μ and every real p ≥ 0 with d + p < r, the radial moment ∫ x, ‖x‖ ^ p (1 + ‖x‖ ^ 2) ^ (-r / 2) ∂μ is the beta integral d μ(B(0, 1)) Β((d + p) / 2, (r - d - p) / 2) / 2. The condition d + p < r records the decay needed at infinity, and p ≥ 0 excludes a singularity at the origin. The value of the integral above is the case p = 0. These formulas are useful for rescaled Euclidean profiles, including the moments of the Yamabe bubbles.

At the endpoint p + d = r the radial moment diverges logarithmically when d > 0. For the rescaled profile y ↦ 2 t / (t² + ‖y - b‖²) raised to a natural power m with p + d = 2 m, the file computes the moment truncated to a ball B(b, R) exactly, as an explicit logarithm minus a partial logarithmic series, and bounds its distance to the logarithm by a harmonic number.

Main declarations

• TauCeti.one_add_norm_sq_rpow_mul_norm_le: one power of ‖x‖ costs one order of the Japanese bracket, ⟨x⟩ ^ m ‖x‖ ≤ ⟨x⟩ ^ (m + 1).
• TauCeti.integrable_rpow_neg_sq_add_norm_sq: the rescaled bracket x ↦ (c ^ 2 + ‖x‖ ^ 2) ^ (-r / 2), c ≠ 0, is integrable for every additive Haar measure.
• TauCeti.integrable_one_add_norm_sq_rpow_neg_succ_div_two: on ℝⁿ the weight x ↦ (1 + ‖x‖ ^ 2) ^ (-(n + 1) / 2) is integrable.
• TauCeti.integrable_norm_rpow_mul_rpow_neg_one_add_norm_sq, TauCeti.integral_norm_rpow_mul_rpow_neg_one_add_norm_sq: integrability and value of the radial moments of the Japanese bracket, for every additive Haar measure.
• TauCeti.sub_two_mul_integral_radial: an identity between two radial moments of the rescaled bracket.
• TauCeti.integral_pow_mul_div_add_sq_pow: the radial integral of the truncated logarithmic moments.
• TauCeti.setIntegral_ball_norm_sub_rpow_mul_div_add_norm_sub_sq_pow, TauCeti.abs_setIntegral_ball_norm_sub_rpow_mul_div_add_norm_sub_sq_pow_sub_mul_log_le: the truncated logarithmic moments of the powers of the rescaled profile, exactly and up to a bounded error.
• TauCeti.integral_rpow_neg_one_add_norm_sq: the value of the integral on a real inner product space, for its canonical Lebesgue measure.

theorem TauCeti.one_add_norm_sq_rpow_mul_norm_le {E : Type u_1} [NormedAddCommGroup E] (x : E) (m : ℝ) : (1 + ‖x‖ ^ 2) ^ (m / 2) * ‖x‖ ≤ (1 + ‖x‖ ^ 2) ^ ((m + 1) / 2)

One power of ‖x‖ costs one order of the Japanese bracket ⟨x⟩ = (1 + ‖x‖ ^ 2) ^ (1 / 2): ⟨x⟩ ^ m ‖x‖ ≤ ⟨x⟩ ^ (m + 1) for every real m.

theorem TauCeti.integrable_rpow_neg_sq_add_norm_sq {V : Type u_1} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] {c r : ℝ} (hc : c ≠ 0) (hr : ↑(Module.finrank ℝ V) < r) : MeasureTheory.Integrable (fun (x : V) => (c ^ 2 + ‖x‖ ^ 2) ^ (-r / 2)) μ

The rescaled Japanese bracket x ↦ (c ^ 2 + ‖x‖ ^ 2) ^ (-r / 2) with c ≠ 0 is integrable on a finite-dimensional real normed space of dimension d < r, for every additive Haar measure. For c = 1 this is Mathlib's integrable_rpow_neg_one_add_norm_sq.

theorem TauCeti.integrable_norm_rpow_mul_rpow_neg_one_add_norm_sq {V : Type u_1} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] {p r : ℝ} (hp : 0 ≤ p) (hr : ↑(Module.finrank ℝ V) + p < r) : MeasureTheory.Integrable (fun (x : V) => ‖x‖ ^ p * (1 + ‖x‖ ^ 2) ^ (-r / 2)) μ

The radial moment x ↦ ‖x‖ ^ p (1 + ‖x‖ ^ 2) ^ (-r / 2) of order p ≥ 0 of the Japanese bracket is integrable for every additive Haar measure when its decay exponent exceeds dim V + p.

theorem TauCeti.integrable_one_add_norm_sq_rpow_neg_succ_div_two {n : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} [μ.IsAddHaarMeasure] : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin n)) => (1 + ‖x‖ ^ 2) ^ (-(↑n + 1) / 2)) μ

On ℝⁿ the Japanese bracket weight ⟨x⟩ ^ (-(n + 1)) is integrable for every additive Haar measure, its decay exponent exceeding the dimension by one.

theorem TauCeti.integral_norm_rpow_mul_rpow_neg_one_add_norm_sq {V : Type u_1} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [Nontrivial V] (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] {p r : ℝ} (hp : 0 ≤ p) (hr : ↑(Module.finrank ℝ V) + p < r) : ∫ (x : V), ‖x‖ ^ p * (1 + ‖x‖ ^ 2) ^ (-r / 2) ∂μ = ↑(Module.finrank ℝ V) * μ.real (Metric.ball 0 1) * (ProbabilityTheory.beta ((↑(Module.finrank ℝ V) + p) / 2) ((r - ↑(Module.finrank ℝ V) - p) / 2) / 2)

The radial moments of the Japanese bracket. On a nontrivial finite-dimensional real normed space V of dimension d, for an additive Haar measure μ and 0 ≤ p with d + p < r, ∫ ‖x‖ ^ p (1 + ‖x‖ ^ 2) ^ (-r / 2) ∂μ = d μ(B(0, 1)) Β((d + p) / 2, (r - d - p) / 2) / 2. For Lebesgue measure on an inner product space the factor d μ(B(0, 1)) is the area of the unit sphere of V.

theorem TauCeti.sub_two_mul_integral_radial {n : ℕ} (hn : 2 < n) {t : ℝ} (ht : 0 < t) (h₁ : MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ (n - 1) * (2 * t / (t ^ 2 + r ^ 2)) ^ n) (Set.Ioi 0) MeasureTheory.volume) (h₂ : MeasureTheory.IntegrableOn (fun (r : ℝ) => r ^ (n - 1) * (r ^ 2 * (2 * t / (t ^ 2 + r ^ 2)) ^ n)) (Set.Ioi 0) MeasureTheory.volume) : (↑n - 2) * ∫ (r : ℝ) in Set.Ioi 0, r ^ (n - 1) * (r ^ 2 * (2 * t / (t ^ 2 + r ^ 2)) ^ n) = ↑n * t ^ 2 * ∫ (r : ℝ) in Set.Ioi 0, r ^ (n - 1) * (2 * t / (t ^ 2 + r ^ 2)) ^ n

For n > 2, the two radial moments of the rescaled Japanese bracket satisfy (n - 2) ∫₀^∞ r ^ (n - 1) r² ψ(r) = n t² ∫₀^∞ r ^ (n - 1) ψ(r), where ψ(r) = (2 t / (t² + r²)) ^ n. This follows by integrating the derivative of r ↦ r ^ n (t² + r²) ψ(r), which vanishes at 0 and at infinity.

Truncated moments at the logarithmic endpoint

For p + d = 2 m, the moment ∫ ‖x‖ ^ p (2 t / (t² + ‖x‖²)) ^ m of the m-th power of the rescaled bracket profile diverges logarithmically when d > 0, and the moments truncated to a ball are computed instead. In polar coordinates about the centre, the integrand is r ^ (2 m - 1) (2 t / (t² + r²)) ^ m. With w = r² / (t² + r²), its antiderivative is (2 t) ^ m / 2 (log (t² + r²) - ∑_{k < m - 1} w ^ (k + 1) / (k + 1)): the derivative of the partial logarithmic series is a geometric sum in w.

theorem TauCeti.integral_pow_mul_div_add_sq_pow {t : ℝ} (ht : t ≠ 0) (m : ℕ) (R : ℝ) : ∫ (r : ℝ) in 0..R, r ^ (2 * m + 1) * (2 * t / (t ^ 2 + r ^ 2)) ^ (m + 1) = 2 ^ m * t ^ (m + 1) * (Real.log (1 + (R / t) ^ 2) - ∑ k ∈ Finset.range m, (R ^ 2 / (t ^ 2 + R ^ 2)) ^ (k + 1) / (↑k + 1))

The radial integral of the truncated profile moments: ∫_0^R r ^ (2 m + 1) (2 t / (t² + r²)) ^ (m + 1) dr = 2 ^ m t ^ (m + 1) (log (1 + (R / t)²) - ∑_{k < m} w ^ (k + 1) / (k + 1)), with w = R² / (t² + R²).

theorem TauCeti.setIntegral_ball_norm_sub_rpow_mul_div_add_norm_sub_sq_pow {V : Type u_1} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] {m : ℕ} (hm : m ≠ 0) {p : ℝ} (hp : p + ↑(Module.finrank ℝ V) = 2 * ↑m) {t : ℝ} (ht : t ≠ 0) {R : ℝ} (hR : 0 ≤ R) (b : V) : ∫ (x : V) in Metric.ball b R, ‖x - b‖ ^ p * (2 * t / (t ^ 2 + ‖x - b‖ ^ 2)) ^ m ∂μ = ↑(Module.finrank ℝ V) * μ.real (Metric.ball 0 1) * (2 ^ (m - 1) * t ^ m * (Real.log (1 + (R / t) ^ 2) - ∑ k ∈ Finset.range (m - 1), (R ^ 2 / (t ^ 2 + R ^ 2)) ^ (k + 1) / (↑k + 1)))

Truncated moments at the logarithmic endpoint. For an additive Haar measure on a space of dimension n, a natural number m ≠ 0 and an order p with p + n = 2 m, the moment of order p of the m-th power of the bubble profile y ↦ 2 t / (t² + ‖y - b‖²) over the ball B(b, R) is n |B(0, 1)| 2 ^ (m - 1) t ^ m (log (1 + (R / t)²) - ∑_{k < m - 1} w ^ (k + 1) / (k + 1)), with w = R² / (t² + R²). When V is nontrivial, the integral over the whole space diverges logarithmically.

theorem TauCeti.abs_setIntegral_ball_norm_sub_rpow_mul_div_add_norm_sub_sq_pow_sub_mul_log_le {V : Type u_1} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] {m : ℕ} (hm : m ≠ 0) {p : ℝ} (hp : p + ↑(Module.finrank ℝ V) = 2 * ↑m) {t : ℝ} (ht : 0 < t) {R : ℝ} (hR : 0 ≤ R) (b : V) : |∫ (x : V) in Metric.ball b R, ‖x - b‖ ^ p * (2 * t / (t ^ 2 + ‖x - b‖ ^ 2)) ^ m ∂μ - ↑(Module.finrank ℝ V) * μ.real (Metric.ball 0 1) * (2 ^ (m - 1) * t ^ m * Real.log (1 + (R / t) ^ 2))| ≤ ↑(Module.finrank ℝ V) * μ.real (Metric.ball 0 1) * (2 ^ (m - 1) * t ^ m * ↑(harmonic (m - 1)))

Truncated moments at the logarithmic endpoint, with remainder bound. In the setting of TauCeti.setIntegral_ball_norm_sub_rpow_mul_div_add_norm_sub_sq_pow, the truncated moment differs from n |B(0, 1)| 2 ^ (m - 1) t ^ m log (1 + (R / t)²) by at most n |B(0, 1)| 2 ^ (m - 1) t ^ m H_{m - 1}, where H_j is the j-th harmonic number.

theorem TauCeti.integral_rpow_neg_one_add_norm_sq {V : Type u_1} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {r : ℝ} (hr : ↑(Module.finrank ℝ V) < r) : ∫ (x : V), (1 + ‖x‖ ^ 2) ^ (-r / 2) = Real.pi ^ (↑(Module.finrank ℝ V) / 2) * Real.Gamma ((r - ↑(Module.finrank ℝ V)) / 2) / Real.Gamma (r / 2)

The integral of the Japanese bracket. On a real inner product space V of dimension d < r, ∫ (1 + ‖x‖ ^ 2) ^ (-r / 2) = π ^ (d / 2) Γ((r - d) / 2) / Γ(r / 2).