Samplinglib mathematical lesson

Evaluate the finite radialized Gaussian test average

AutoSamplingTheory.ExampleCases.GaussianComplexity.RadialIntegral.radialized_test_integral · theorem · Teaching coverage

Read this first

Mathematical statement

Let n≥3, kappa≥4 and lambda≥0, and draw O from the existing normalized Haar probability on the full real O(n). Put U=O_11, p=n/2 as a real number, a(O)=kappa+1+4lambda-(kappa-1)U, A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O^T), F(O)=det(O)sqrt(det A_O), N(O)=(sqrt(kappa)+1)U-(sqrt(kappa)-1), and J(O)=integral over real Euclidean n-space of exp(-a(O)||x||^2/4) against canonical volume. Every inner spatial integrand is absolutely integrable; F(O)J(O) and N(O)/a(O)^p are absolutely integrable under this Haar probability. Their finite expectations satisfy E[FJ]/(2pi)^p = [(-1)^(n-1)(sqrt(kappa)-1)^(n-1)/2^p] E[N/a^p]. This evaluates the explicit radialized iterated integral and does not identify it with the original mixture test H(lambda).

\[\frac{\mathbb E[F(O)J(O)]}{(2\pi)^p}=\frac{(-1)^{n-1}(\sqrt\kappa-1)^{n-1}}{2^p}\,\mathbb E\!\left[\frac{(\sqrt\kappa+1)U-(\sqrt\kappa-1)}{a(O)^p}\right],\qquad p=\frac n2\]

Lean statement · radialized_test_integral

The local lets spell out first index, actual matrix entry, denominator and real exponent; all L1 assertions are outputs.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem radialized_test_integral {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) {ℓ : ℝ} (hℓ : 0 ≤ ℓ) :
    let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
    let U : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
      fun O => (O : Matrix (Fin n) (Fin n) ℝ) j0 j0
    let a : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
      fun O => κ + 1 + 4 * ℓ - (κ - 1) * U O
    let p : ℝ := (n : ℝ) / 2
    (∀ O : Matrix.orthogonalGroup (Fin n) ℝ,
      Integrable (fun x : EuclideanSpace ℝ (Fin n) => Real.exp (-a O * ‖x‖ ^ 2 / 4)) volume) ∧
    Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        (∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-a O * ‖x‖ ^ 2 / 4))) (orthogonalHaar n) ∧
    Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      ((Real.sqrt κ + 1) * U O - (Real.sqrt κ - 1)) / (a O) ^ p) (orthogonalHaar n) ∧
    (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        (∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-a O * ‖x‖ ^ 2 / 4)) ∂orthogonalHaar n) /
      (2 * Real.pi) ^ p =
      ((-1 : ℝ) ^ (n - 1) * (Real.sqrt κ - 1) ^ (n - 1) / (2 : ℝ) ^ p) *
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          ((Real.sqrt κ + 1) * U O - (Real.sqrt κ - 1)) / (a O) ^ p ∂orthogonalHaar n)

Exact module and namespace context

Proof roadmap

1Keep the denominator strictly positive
Orthogonality bounds the first diagonal entry by one in absolute value. Since kappa-1 is nonnegative, a(O)≥2+4lambda≥2. Thus every real power and denominator in the displayed actual integrands has a strictly positive base. This is derived from the stated assumptions.
2Evaluate a genuine finite spatial Gaussian integral
For each fixed O, apply the existing Euclidean Gaussian formula with positive rate a(O)/4. Its integrability theorem is used as well as its value. Dimension is exactly n, and the exponent is n/2 in R. Hence this step cannot obtain the displayed value from a default integral of a divergent function.
3Prove the outer expectations are finite
The functions U, a, det(O), det(A_O) and sqrt(det(A_O)) are continuous on the actual compact group O(n). The positive denominators preserve continuity. Thus F/a^p and N/a^p are integrable under the existing finite Haar probability. The formula for J transfers integrability to FJ. The implementation uses finite compact bounds where explicit sharp domination constants are unnecessary.
4Extract the exact Gaussian normalization
Use the pointwise finite Gaussian formula inside the already defined iterated integral. Real-power multiplication and quotient rules give (4pi)^p/(2pi)^p=2^p. Moving this constant through the Haar integral is ordinary one-integral linearity; no exchange of two integrals is asserted.
5Apply the actual general L1 cancellation theorem
Choose a globally continuous scalar extension h(u)=1/max(kappa+1+4lambda-(kappa-1)u,1)^p. On every actual U, the denominator is at least two, so h(U)=1/a(O)^p exactly. This extension makes the real-line Borel condition explicit without changing the actual weight. Compactness gives its actual Haar L1 property. The existing LemmaB6 therefore applies with all its genuine hypotheses discharged.
6Retain the half-dimensional power and sign
Since p=n/2 is real division, 2p=n and 2^n=2^p 2^p. Multiplying the Gaussian factor by the exact B6 coefficient gives 2^p/2^n=1/2^p. The parity factor (-1)^(n-1) and power (sqrt(kappa)-1)^(n-1) are unchanged.

Full assumptions and notation

All objects and hypotheses

Natural n≥3 and real kappa≥4 are the AppendixB2 standing range. Real lambda≥0 includes zero; no positive-lambda-only restriction is introduced.
The law is the actual canonical normalized full orthogonal Haar probability, with its inherited matrix topology and Borel sigma-algebra. A_O is the existing literal equation4 precision.
The inner domain is EuclideanSpace R (Fin n) with Euclidean norm and canonical volume. The exponent n/2 is real division, including half-integer dimensions; only the sign/normalizer powers n-1 use natural exponents.
All three absolute-integrability assertions are conclusions. No Gaussian density law, assumed Fubini equality, denominator bound, normalized-mixture identity or Borel/L1 weight is supplied by the caller.

Mathematical proof

1. Keep the denominator strictly positive

Orthogonality bounds the first diagonal entry by one in absolute value. Since kappa-1 is nonnegative, a(O)≥2+4lambda≥2. Thus every real power and denominator in the displayed actual integrands has a strictly positive base. This is derived from the stated assumptions.

\[|U|\le1,\qquad a(O)\ge2+4\lambda\ge2>0\]

Corresponding Lean step

The main proof uses entry_norm_bound_of_unitary on the actual matrix, then ha_bound and ha_pos. No caller bound or regularity premise is added.

2. Evaluate a genuine finite spatial Gaussian integral

For each fixed O, apply the existing Euclidean Gaussian formula with positive rate a(O)/4. Its integrability theorem is used as well as its value. Dimension is exactly n, and the exponent is n/2 in R. Hence this step cannot obtain the displayed value from a default integral of a divergent function.

\[J(O)=\int_{\mathbb R^n}e^{-a(O)\|x\|^2/4}\,dx=\left(\frac{4\pi}{a(O)}\right)^p,\qquad e^{-a(O)\|x\|^2/4}\in L^1(dx)\]

Corresponding Lean step

Private gaussian_integral genuinely calls GaussianFourier.integrable_cexp_neg_mul_sq_norm_add and takes its real part, then GaussianFourier.integral_rexp_neg_mul_sq_norm. Canonical finrank_euclideanSpace identifies dimension n. This is reuse of Mathlib, not a new public generic Gaussian wrapper.

3. Prove the outer expectations are finite

The functions U, a, det(O), det(A_O) and sqrt(det(A_O)) are continuous on the actual compact group O(n). The positive denominators preserve continuity. Thus F/a^p and N/a^p are integrable under the existing finite Haar probability. The formula for J transfers integrability to FJ. The implementation uses finite compact bounds where explicit sharp domination constants are unnecessary.

\[\frac{F}{a^p},\ \frac{N}{a^p}\in L^1(\mu_n),\qquad FJ=(4\pi)^p\frac{F}{a^p}\in L^1(\mu_n)\]

Corresponding Lean step

Private integrable_continuous_haar consumes orthogonalHaar_spec and Continuous.integrable_of_hasCompactSupport on compact O(n). The main proof establishes continuity of the literal precision and positive real-power denominators. This does not perform Fubini on the original experiment.

4. Extract the exact Gaussian normalization

Use the pointwise finite Gaussian formula inside the already defined iterated integral. Real-power multiplication and quotient rules give (4pi)^p/(2pi)^p=2^p. Moving this constant through the Haar integral is ordinary one-integral linearity; no exchange of two integrals is asserted.

\[\frac{\mathbb E[FJ]}{(2\pi)^p}=\frac{(4\pi)^p}{(2\pi)^p}\mathbb E\!\left[\frac F{a^p}\right]=2^p\mathbb E\!\left[\frac F{a^p}\right]\]

Corresponding Lean step

hprod and hOuter_eq use the actual gaussian_integral value, Real.div_rpow and integral_const_mul. hnorm proves the pi factors cancel exactly.

5. Apply the actual general L1 cancellation theorem

Choose a globally continuous scalar extension h(u)=1/max(kappa+1+4lambda-(kappa-1)u,1)^p. On every actual U, the denominator is at least two, so h(U)=1/a(O)^p exactly. This extension makes the real-line Borel condition explicit without changing the actual weight. Compactness gives its actual Haar L1 property. The existing LemmaB6 therefore applies with all its genuine hypotheses discharged.

\[h(U)=a(O)^{-p},\qquad\mathbb E\!\left[\frac F{a^p}\right]=\frac{(-1)^{n-1}(\sqrt\kappa-1)^{n-1}}{2^n}\mathbb E\!\left[\frac N{a^p}\right]\]

Corresponding Lean step

The proof constructs the continuous positive-base max extension, proves hactual on every O and hL1 internally, and directly calls the identical compiled signed_sqrt_det_integral. The extension is a proof adapter outside the actual entry range, not a changed source weight or source repair.

6. Retain the half-dimensional power and sign

Since p=n/2 is real division, 2p=n and 2^n=2^p 2^p. Multiplying the Gaussian factor by the exact B6 coefficient gives 2^p/2^n=1/2^p. The parity factor (-1)^(n-1) and power (sqrt(kappa)-1)^(n-1) are unchanged.

\[2^p\,\frac{(-1)^{n-1}(\sqrt\kappa-1)^{n-1}}{2^n}=\frac{(-1)^{n-1}(\sqrt\kappa-1)^{n-1}}{2^p}\]

Corresponding Lean step

htwos uses Real.rpow_add and Real.rpow_natCast with p+p=n. The final field identity uses actual nonzero positive powers; no natural-number truncation of n/2 is allowed.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · radialized_test_integral

Two private providers establish genuine continuous Haar integrability and spatial Gaussian finiteness/evaluation. The public proof derives the positive denominator, all three L1 outputs, exact B6 use and normalization arithmetic.

Download module (.lean)

theorem radialized_test_integral {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) {ℓ : ℝ} (hℓ : 0 ≤ ℓ) :
    let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
    let U : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
      fun O => (O : Matrix (Fin n) (Fin n) ℝ) j0 j0
    let a : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
      fun O => κ + 1 + 4 * ℓ - (κ - 1) * U O
    let p : ℝ := (n : ℝ) / 2
    (∀ O : Matrix.orthogonalGroup (Fin n) ℝ,
      Integrable (fun x : EuclideanSpace ℝ (Fin n) => Real.exp (-a O * ‖x‖ ^ 2 / 4)) volume) ∧
    Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        (∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-a O * ‖x‖ ^ 2 / 4))) (orthogonalHaar n) ∧
    Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ =>
      ((Real.sqrt κ + 1) * U O - (Real.sqrt κ - 1)) / (a O) ^ p) (orthogonalHaar n) ∧
    (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        (∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-a O * ‖x‖ ^ 2 / 4)) ∂orthogonalHaar n) /
      (2 * Real.pi) ^ p =
      ((-1 : ℝ) ^ (n - 1) * (Real.sqrt κ - 1) ^ (n - 1) / (2 : ℝ) ^ p) *
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          ((Real.sqrt κ + 1) * U O - (Real.sqrt κ - 1)) / (a O) ^ p ∂orthogonalHaar n) := by
  classical
  let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
  let U : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
    fun O => (O : Matrix (Fin n) (Fin n) ℝ) j0 j0
  let a : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
    fun O => κ + 1 + 4 * ℓ - (κ - 1) * U O
  let p : ℝ := (n : ℝ) / 2
  let F : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
    fun O => (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det
  let N : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
    fun O => (Real.sqrt κ + 1) * U O - (Real.sqrt κ - 1)
  let J : Matrix.orthogonalGroup (Fin n) ℝ → ℝ :=
    fun O => ∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-a O * ‖x‖ ^ 2 / 4)
  let C : ℝ := (4 * Real.pi) ^ p
  let c : ℝ := (-1 : ℝ) ^ (n - 1) * (Real.sqrt κ - 1) ^ (n - 1)
  change (∀ O : Matrix.orthogonalGroup (Fin n) ℝ,
      Integrable (fun x : EuclideanSpace ℝ (Fin n) => Real.exp (-a O * ‖x‖ ^ 2 / 4)) volume) ∧
    Integrable (fun O => F O * J O) (orthogonalHaar n) ∧
    Integrable (fun O => N O / (a O) ^ p) (orthogonalHaar n) ∧
      (∫ O, F O * J O ∂orthogonalHaar n) / (2 * Real.pi) ^ p =
        (c / (2 : ℝ) ^ p) * (∫ O, N O / (a O) ^ p ∂orthogonalHaar n)
  have hUc : Continuous U := continuous_subtype_val.matrix_elem j0 j0
  have hac : Continuous a := by dsimp only [a]; fun_prop
  have ha_bound (O : Matrix.orthogonalGroup (Fin n) ℝ) : 2 + 4 * ℓ ≤ a O := by
    have hU : U O ≤ 1 := le_trans (le_abs_self _) (by
      simpa only [U, Real.norm_eq_abs] using entry_norm_bound_of_unitary O.property j0 j0)
    have hmul := mul_le_mul_of_nonneg_left hU (show 0 ≤ κ - 1 by linarith)
    dsimp only [a]
    nlinarith
  have ha_pos (O : Matrix.orthogonalGroup (Fin n) ℝ) : 0 < a O := by
    have := ha_bound O
    linarith
  have hpownz (O : Matrix.orthogonalGroup (Fin n) ℝ) : (a O) ^ p ≠ 0 :=
    (Real.rpow_pos_of_pos (ha_pos O) p).ne'
  have hpowc : Continuous (fun O => (a O) ^ p) :=
    hac.rpow_const (fun O => Or.inl (ha_pos O).ne')
  have hAc : Continuous (fun O : Matrix.orthogonalGroup (Fin n) ℝ => singleBlockPrecision κ O) := by
    unfold singleBlockPrecision
    exact continuous_const.sub
      ((continuous_subtype_val.add continuous_subtype_val.matrix_transpose).const_smul ((κ - 1) / 4))
  have hFc : Continuous F := continuous_subtype_val.matrix_det.mul
    (Real.continuous_sqrt.comp hAc.matrix_det)
  have hNc : Continuous N := (hUc.const_mul _).sub continuous_const
  have hWint : Integrable (fun O => F O / (a O) ^ p) (orthogonalHaar n) :=
    integrable_continuous_haar (hFc.div hpowc hpownz)
  have hNint : Integrable (fun O => N O / (a O) ^ p) (orthogonalHaar n) :=
    integrable_continuous_haar (hNc.div hpowc hpownz)
  have hJ (O : Matrix.orthogonalGroup (Fin n) ℝ) : J O = (4 * Real.pi / a O) ^ p :=
    (gaussian_integral (ha_pos O)).2
  have hprod (O : Matrix.orthogonalGroup (Fin n) ℝ) :
      F O * J O = C * (F O / (a O) ^ p) := by
    rw [hJ, Real.div_rpow (by positivity) (ha_pos O).le]
    dsimp only [C]
    ring
  have hOuter : Integrable (fun O => F O * J O) (orthogonalHaar n) :=
    (hWint.const_mul C).congr (Filter.Eventually.of_forall fun O => (hprod O).symm)
  refine ⟨fun O => (gaussian_integral (ha_pos O)).1, hOuter, hNint, ?_⟩
  let h : ℝ → ℝ := fun u => 1 / (max (κ + 1 + 4 * ℓ - (κ - 1) * u) 1) ^ p
  have hbase : Continuous (fun u : ℝ => max (κ + 1 + 4 * ℓ - (κ - 1) * u) 1) := by fun_prop
  have hbase_pos (u : ℝ) : 0 < max (κ + 1 + 4 * ℓ - (κ - 1) * u) 1 :=
    lt_of_lt_of_le zero_lt_one (le_max_right _ _)
  have hh : Continuous h := continuous_const.div
    (hbase.rpow_const (fun u => Or.inl (hbase_pos u).ne'))
    (fun u => (Real.rpow_pos_of_pos (hbase_pos u) p).ne')
  have hactual (O : Matrix.orthogonalGroup (Fin n) ℝ) : h (U O) = 1 / (a O) ^ p := by
    change 1 / (max (a O) 1) ^ p = 1 / (a O) ^ p
    rw [max_eq_left (by linarith [ha_bound O])]
  have hL1 : Integrable (fun O => h (U O)) (orthogonalHaar n) :=
    integrable_continuous_haar (hh.comp hUc)
  have hb := signed_sqrt_det_integral hn hκ h hh.measurable hL1
  change (∫ O, F O * h (U O) ∂orthogonalHaar n) =
    c / (2 : ℝ) ^ n * (∫ O, N O * h (U O) ∂orthogonalHaar n) at hb
  simp_rw [hactual, mul_one_div] at hb
  have hOuter_eq : (∫ O, F O * J O ∂orthogonalHaar n) =
      C * (∫ O, F O / (a O) ^ p ∂orthogonalHaar n) := by
    simp_rw [hprod]
    exact integral_const_mul _ _
  have hpi_ne : (2 * Real.pi) ^ p ≠ 0 :=
    (Real.rpow_pos_of_pos (by positivity : 0 < 2 * Real.pi) p).ne'
  have htwo_ne : (2 : ℝ) ^ p ≠ 0 := (Real.rpow_pos_of_pos (by norm_num : 0 < (2 : ℝ)) p).ne'
  have hnorm : C / (2 * Real.pi) ^ p = (2 : ℝ) ^ p := by
    dsimp only [C]
    rw [show 4 * Real.pi = (2 : ℝ) * (2 * Real.pi) by ring,
      Real.mul_rpow (by norm_num : 0 ≤ (2 : ℝ)) (by positivity)]
    exact mul_div_cancel_right₀ _ hpi_ne
  have htwos : (2 : ℝ) ^ n = (2 : ℝ) ^ p * (2 : ℝ) ^ p := by
    rw [← Real.rpow_natCast, ← Real.rpow_add (by norm_num : 0 < (2 : ℝ))]
    congr 1
    dsimp only [p]
    ring
  rw [hOuter_eq]
  calc
    C * (∫ O, F O / (a O) ^ p ∂orthogonalHaar n) / (2 * Real.pi) ^ p =
        (C / (2 * Real.pi) ^ p) * (∫ O, F O / (a O) ^ p ∂orthogonalHaar n) := by ring
    _ = (2 : ℝ) ^ p * (c / (2 : ℝ) ^ n *
        (∫ O, N O / (a O) ^ p ∂orthogonalHaar n)) := by rw [hnorm, hb]
    _ = c / (2 : ℝ) ^ p * (∫ O, N O / (a O) ^ p ∂orthogonalHaar n) := by
      rw [htwos]
      field_simp [htwo_ne]

end AutoSamplingTheory.ExampleCases.GaussianComplexity.RadialIntegral

Exact module and namespace context

Scope and omitted-condition boundaries

Only Ex60 Gaussian evaluation for its explicit radialized integral and the B6 specialization leading to the Eq21 right-hand side. Equality to original H(lambda), actual Gaussian probability laws and density normalization, conjugation/radialization of the original mixture, original Fubini/interchange, determinant-component half-mass, Haar-column sphere uniformity, Poisson identities, TV/radial/Hellinger separation, transcript/eigenbasis reductions and both main lower bounds remain separate obligations. The source-only sharp minor/path bounds inherited from B6 are not newly claimed; additional sharp domination constants in the source inventory are distinguishable from sufficient compact boundedness.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

GaussianFourier.integrable_cexp_neg_mul_sq_norm_add
GaussianFourier.integral_rexp_neg_mul_sq_norm
finrank_euclideanSpace
Continuous.integrable_of_hasCompactSupport
entry_norm_bound_of_unitary
Continuous.matrix_det
Real.continuous_sqrt
Continuous.rpow_const
Real.div_rpow
Real.mul_rpow
Real.rpow_add
Real.rpow_natCast
MeasureTheory.integral_const_mul

Mathematical sources

Explicit radialized integral and its analytic evaluation — Ex60 RHS radial integral through Eq21 RHS only; identification with original H(lambda) is excluded.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.