The integral of the Japanese bracket power (1 + ‖w‖²)^{-(n+1)} over ℂⁿ

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Analysis.SpecialFunctions.JapaneseBracket, which at the pin proves only the integrability of (1 + ‖x‖²)^{-r/2} for r > dim, never a value).

The analytic half of the Fubini–Study mass computation: the total mass of the Fubini–Study volume is 4ⁿ n! times this integral, and its value is πⁿ / n!.

• bracketAnti a k — the antiderivative -(a + r²)^{-(k+1)} / (2(k+1)) of r (a + r²)^{-(k+2)}, with hasDerivAt_bracketAnti, continuous_bracketAnti, tendsto_bracketAnti (to 0 at ∞);
• ★ integral_Ioi_mul_pow_inv_add_sq — the radial integral ∫₀^∞ r (a + r²)^{-(k+2)} dr = a^{-(k+1)} / (2(k+1)), by the fundamental theorem of calculus on [0, ∞) (integral_Ioi_of_hasDerivAt_of_tendsto), with integrableOn_Ioi_mul_pow_inv_add_sq;
• ★ lintegral_complex_pow_inv_add_norm_sq — the planar integral ∫_ℂ (a + |z|²)^{-(k+2)} dz = π a^{-(k+1)} / (k+1), by polar coordinates (Complex.lintegral_comp_polarCoord_symm) and Tonelli;
• ★★ lintegral_pi_pow_inv_one_add_sum_norm_sq — ∫_{ℂⁿ} (1 + ∑ⱼ |wⱼ|²)^{-(n+1)} dw = πⁿ / n!, by induction on n: split off one coordinate (measurePreserving_piFinSuccAbove), integrate it out with the planar integral at a = 1 + ‖w'‖², and recognise π/(n+1) times the case n.

Honest scope

⚠️ Lebesgue integrals (lintegral) of ENNReal.ofReal, against volume on Fin n → ℂ (the product of the Lebesgue measures on ℂ = ℝ²); the norm is written as the coordinate sum ∑ⱼ ‖wⱼ‖², so no EuclideanSpace appears. Only the exponent n + 1 on ℂⁿ is computed — the one the top power needs — not the general (1 + ‖x‖²)^{-r/2}.

Provenance and references. The top-power plan (M7); Mathlib/Analysis/SpecialFunctions/PolarCoord.lean; Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean; Mathlib/MeasureTheory/Constructions/Pi.lean (measurePreserving_piFinSuccAbove); the completed-work ledger.

The radial integral

noncomputable def MeasureTheory.bracketAnti (a : ℝ) (k : ℕ) (r : ℝ) : ℝ

The antiderivative -(a + r²)^{-(k+1)} / (2(k+1)) of r (a + r²)^{-(k+2)}.

Equations

• MeasureTheory.bracketAnti a k r = -((a + r ^ 2)⁻¹ ^ (k + 1) / (2 * (↑k + 1)))

theorem MeasureTheory.hasDerivAt_bracketAnti (a : ℝ) (ha : 0 < a) (k : ℕ) (r : ℝ) : HasDerivAt (bracketAnti a k) (r * (a + r ^ 2)⁻¹ ^ (k + 1 + 1)) r

theorem MeasureTheory.continuous_bracketAnti (a : ℝ) (ha : 0 < a) (k : ℕ) : Continuous (bracketAnti a k)

theorem MeasureTheory.tendsto_bracketAnti (a : ℝ) (k : ℕ) : Filter.Tendsto (bracketAnti a k) Filter.atTop (nhds 0)

theorem MeasureTheory.integrableOn_Ioi_mul_pow_inv_add_sq (a : ℝ) (ha : 0 < a) (k : ℕ) : IntegrableOn (fun (r : ℝ) => r * (a + r ^ 2)⁻¹ ^ (k + 1 + 1)) (Set.Ioi 0) volume

theorem MeasureTheory.integral_Ioi_mul_pow_inv_add_sq (a : ℝ) (ha : 0 < a) (k : ℕ) : ∫ (r : ℝ) in Set.Ioi 0, r * (a + r ^ 2)⁻¹ ^ (k + 1 + 1) = a⁻¹ ^ (k + 1) / (2 * (↑k + 1))

★ The radial integral ∫₀^∞ r (a + r²)^{-(k+2)} dr = a^{-(k+1)} / (2 (k+1)).

The planar integral

theorem MeasureTheory.lintegral_complex_pow_inv_add_norm_sq (a : ℝ) (ha : 0 < a) (k : ℕ) : ∫⁻ (z : ℂ), ENNReal.ofReal ((a + ‖z‖ ^ 2)⁻¹ ^ (k + 1 + 1)) = ENNReal.ofReal (Real.pi * a⁻¹ ^ (k + 1) / (↑k + 1))

★ The planar integral ∫_ℂ (a + |z|²)^{-(k+2)} dz = π a^{-(k+1)} / (k+1), by polar coordinates.

The integral over ℂⁿ

theorem MeasureTheory.lintegral_pi_pow_inv_one_add_sum_norm_sq (n : ℕ) : ∫⁻ (w : Fin n → ℂ), ENNReal.ofReal ((1 + ∑ j : Fin n, ‖w j‖ ^ 2)⁻¹ ^ (n + 1)) = ENNReal.ofReal (Real.pi ^ n / ↑n.factorial)

★★ ∫_{ℂⁿ} (1 + ‖w‖²)^{-(n+1)} dw = πⁿ / n!, with ‖w‖² = ∑ⱼ ‖wⱼ‖²: by induction on n, splitting off one coordinate (measurePreserving_piFinSuccAbove) and integrating it out.