The Japanese bracket integral on a Euclidean space of even dimension

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Analysis.SpecialFunctions.JapaneseBracket).

JapaneseBracketIntegral.lean computes ∫_{ℂⁿ} (1 + ∑ⱼ |wⱼ|²)^{-(n+1)} dw = πⁿ / n! against the product Lebesgue measure on Fin n → ℂ, with the norm written as a coordinate sum. This module carries the value to the spaces where the norm is the norm:

• ★ Complex.lintegral_euclideanSpace_pow_inv_one_add_norm_sq — the same integral on EuclideanSpace ℂ (Fin n), ∫ (1 + ‖x‖²)^{-(n+1)} dx = πⁿ / n!, against the volume of its real inner-product structure (Complex.measurePreserving_ofLp, EuclideanSpace.norm_sq_eq);
• ★★ lintegral_pow_inv_one_add_norm_sq — on every real inner-product space of dimension 2n, ∫ (1 + ‖x‖²)^{-(n+1)} dx = πⁿ / n!: any two such spaces are isometric through their orthonormal bases, and a linear isometry preserves the volume (LinearIsometryEquiv.measurePreserving).

Only the exponent n + 1 in dimension 2n is computed — the one the Fubini–Study mass needs — not the general (1 + ‖x‖²)^{-r/2} of Mathlib's integrability statement.

theorem measurable_pow_inv_one_add_norm_sq {F : Type u_1} [NormedAddCommGroup F] [MeasurableSpace F] [OpensMeasurableSpace F] (m : ℕ) : Measurable fun (x : F) => ENNReal.ofReal ((1 + ‖x‖ ^ 2)⁻¹ ^ m)

The integrand, as a function of the squared norm; continuous, hence measurable.

theorem Complex.lintegral_euclideanSpace_pow_inv_one_add_norm_sq (n : ℕ) : ∫⁻ (x : EuclideanSpace ℂ (Fin n)), ENNReal.ofReal ((1 + ‖x‖ ^ 2)⁻¹ ^ (n + 1)) = ENNReal.ofReal (Real.pi ^ n / ↑n.factorial)

★ ∫_{ℂⁿ} (1 + ‖x‖²)^{-(n+1)} dx = πⁿ / n! on EuclideanSpace ℂ (Fin n), against the volume of its real inner-product structure: ofLp is volume preserving and carries ‖x‖² to the coordinate sum ∑ⱼ ‖xⱼ‖².

theorem lintegral_pow_inv_one_add_norm_sq {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {n : ℕ} (h : Module.finrank ℝ F = 2 * n) : ∫⁻ (x : F), ENNReal.ofReal ((1 + ‖x‖ ^ 2)⁻¹ ^ (n + 1)) = ENNReal.ofReal (Real.pi ^ n / ↑n.factorial)

★★ The Japanese bracket integral on a real inner-product space of dimension 2n: ∫ (1 + ‖x‖²)^{-(n+1)} dx = πⁿ / n!. Any two such spaces are isometric through orthonormal bases indexed by Fin (2n) (OrthonormalBasis.repr), and a linear isometry preserves the volume.