Samplinglib mathematical lesson

Normalize the signed Gaussian expectation

Read this first

Mathematical statement

At the selected tilt, factor the actual Gaussian expectation into a scalar coefficient and one absolutely integrable Haar kernel.

\[H_\gamma(\ell)=\beta_{n,\kappa}\,\mathbb E_\mu q,\qquad q\in L^1(\mu).\]

Lean statement · selected_gaussian_normalization

The unchanged preproof signature has only source n>=3 and kappa>=4. Actual Gaussian/Haar objects and normalized kernel are literal; positivity and L1 are proved internally.

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 selected_gaussian_normalization {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) :
    let s : ℝ := Real.sqrt κ
    let r : ℝ := (1 - 1 / (n : ℝ)) * ((s - 1) / (s + 1))
    let ℓ : ℝ := (4 * (n : ℝ) * s + (s - 1) ^ 2) /
      (8 * (n : ℝ) * ((n : ℝ) - 1))
    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 q : Matrix.orthogonalGroup (Fin n) ℝ → ℝ := fun O =>
      ((s + 1) * U O - (s - 1)) /
        (1 + r ^ 2 - 2 * r * U O) ^ ((n : ℝ) / 2)
    let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
      fun O => ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
        (singleBlockPrecision κ O)⁻¹
    Integrable q (orthogonalHaar n) ∧
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det *
          (∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-ℓ * ‖x‖ ^ 2) ∂γ O)
        ∂orthogonalHaar n) =
        (((-1 : ℝ) ^ (n - 1) * (s - 1) ^ (n - 1)) / (s + 1) ^ n) *
          (1 - 1 / (n : ℝ)) ^ ((n : ℝ) / 2) * (∫ O, q O ∂orthogonalHaar n)

Exact module and namespace context

This supplies the real-power normalization before Eq24; the actual sphere law and Poisson integral remain open.

Full assumptions and notation

All objects and hypotheses

Exactly natural \(n\ge3\) and real \(\kappa\ge4\), including \(\kappa=4\). All divisions involving \(n\) are real after coercion; \(n/2\) is a real exponent, including odd dimensions.
\(\mu\) is the unchanged normalized Haar probability on full \(O(n)\), with both determinant signs. \(U=O_{11}\) is its actual matrix coordinate; \(\gamma_O\) is the canonical Gaussian with covariance \(A_O^{-1}\).
\(r,\ell\) are the literal selected parameters. Their positivity, the actual-coordinate denominator positivity and absolute integrability of \(q\) are conclusions, never caller assumptions.

Notation and interpretation

\(s,r,\ell\): Literal source choices, with real dimension arithmetic.
\[s=\sqrt\kappa,\qquad r=\left(1-\frac1n\right)\frac{s-1}{s+1},\qquad\ell=\frac{4ns+(s-1)^2}{8n(n-1)}.\]
\(H_\gamma,q,\beta\): Actual signed Gaussian expectation, normalized scalar kernel and selected coefficient. The Haar expectation of q is not evaluated here.
\[\begin{aligned}H_\gamma(\ell)&=\mathbb E_\mu\!\left[\det(O)\int e^{-\ell\|x\|_2^2}\,d\gamma_O\right],\\q(O)&=\frac{(s+1)U-(s-1)}{(1+r^2-2rU)^{n/2}},\\\beta_{n,\kappa}&=\frac{(-1)^{n-1}(s-1)^{n-1}}{(s+1)^n}\left(1-\frac1n\right)^{n/2}.\end{aligned}\]
\(A_O,\gamma_O\): The literal source precision and actual canonical Gaussian. Fin n index zero denotes the source first coordinate.
\[A_O=\frac{\kappa+1}{2}I-\frac{\kappa-1}{4}(O+O^\top),\qquad\gamma_O=\mathcal N(0,A_O^{-1}).\]

Mathematical proof

Open a step to read its argument and formula.

1. Use the actual selected parameters

Apply the identical compiled selection theorem. It supplies the positive tilt, the radius interval and the literal affine matching. These conditions are not copied into the public hypotheses.

\[0<r<1,\quad\ell>0,\qquad D_\ell(U)=\kappa+1+4\ell-(\kappa-1)U=C(1+r^2-2rU),\quad C=\frac{n(s+1)^2}{2(n-1)}>0.\]

Corresponding Lean step

hsel and hden call SelectedTilt.selected_tilt exactly; all n, square-root and coefficient domains are derived internally.

2. Keep the actual coordinate in its range

Orthogonality gives the coordinate bound. The normalized denominator is uniformly positive, so the quotient is continuous on compact full O(n) and absolutely integrable under its Haar probability. This step is essential before the real-power rule.

\[|U|\le1,\qquad 1+r^2-2rU=(1-r)^2+2r(1-U)\ge(1-r)^2>0,\qquad q\in L^1(\mu).\]

Corresponding Lean step

hbpos uses canonical entry_norm_bound_of_unitary and the compiled radius bounds. hqcont uses Continuous.rpow_const and Continuous.div; hqL directly calls Continuous.integrable_of_hasCompactSupport with the existing Haar probability, without cloning a generic compact-integration lemma.

3. Scale the positive real power

Write p=n/2 and a=1-1/n. Both factors in the matched denominator are positive. The positive-base multiplication law therefore applies even when n is odd.

\[[C(1+r^2-2rU)]^p=C^p(1+r^2-2rU)^p,\qquad p=n/2,\quad a=1-1/n>0.\]

Corresponding Lean step

The pointwise final integral congruence uses hden, hC, hbpos and canonical Real.mul_rpow. The actual coordinate range is a consumed proof dependency, not positivity for an arbitrary real u.

4. Simplify the entire prefactor

Normalize the coefficient together with the original factor of two. Converting the squared base to the natural n-th power uses real exponent multiplication, not integer rounding.

\[2C=\frac{(s+1)^2}{a},\qquad 2^p C^p=\frac{(s+1)^n}{a^p},\qquad\beta_{n,\kappa}=\frac{(-1)^{n-1}(s-1)^{n-1}}{(s+1)^n}a^p.\]

Corresponding Lean step

htwoC, hpow2, hscale and hpref directly reuse Real.rpow_natCast_mul, Real.rpow_natCast, Real.mul_rpow and Real.div_rpow. Nonzero denominators are established before field normalization.

5. Join the actual Gaussian transform

Use the existing actual Gaussian expectation identity at the proved positive tilt, rewrite its denominator and move the constant outside the same full-Haar integral. The normalized expectation is left unevaluated.

\[H_\gamma(\ell)=\frac{(-1)^{n-1}(s-1)^{n-1}}{2^p}(C^p)^{-1}\mathbb E_\mu q=\beta_{n,\kappa}\mathbb E_\mu q.\]

Corresponding Lean step

hg calls GaussianExpectation.actual_gaussian_transform hn hκ hℓ.le. The final calc uses integral_congr_ae and integral_const_mul, then hpref. The focused test consumes this exact equality in the actual determinant-conditioned Gaussian mixture expectation gap. It does not supply the sphere/Poisson evaluation.

Lean verification

Lean proof · selected_gaussian_normalization

Positive-base real-power normalization joins the identical selected-parameter and actual Gaussian transform parents.

Download module (.lean)

theorem selected_gaussian_normalization {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) :
    let s : ℝ := Real.sqrt κ
    let r : ℝ := (1 - 1 / (n : ℝ)) * ((s - 1) / (s + 1))
    let ℓ : ℝ := (4 * (n : ℝ) * s + (s - 1) ^ 2) /
      (8 * (n : ℝ) * ((n : ℝ) - 1))
    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 q : Matrix.orthogonalGroup (Fin n) ℝ → ℝ := fun O =>
      ((s + 1) * U O - (s - 1)) /
        (1 + r ^ 2 - 2 * r * U O) ^ ((n : ℝ) / 2)
    let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
      fun O => ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
        (singleBlockPrecision κ O)⁻¹
    Integrable q (orthogonalHaar n) ∧
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det *
          (∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-ℓ * ‖x‖ ^ 2) ∂γ O)
        ∂orthogonalHaar n) =
        (((-1 : ℝ) ^ (n - 1) * (s - 1) ^ (n - 1)) / (s + 1) ^ n) *
          (1 - 1 / (n : ℝ)) ^ ((n : ℝ) / 2) * (∫ O, q O ∂orthogonalHaar n) := by
  classical
  let s : ℝ := Real.sqrt κ
  let r : ℝ := (1 - 1 / (n : ℝ)) * ((s - 1) / (s + 1))
  let ℓ : ℝ := (4 * (n : ℝ) * s + (s - 1) ^ 2) /
    (8 * (n : ℝ) * ((n : ℝ) - 1))
  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 q : Matrix.orthogonalGroup (Fin n) ℝ → ℝ := fun O =>
    ((s + 1) * U O - (s - 1)) /
      (1 + r ^ 2 - 2 * r * U O) ^ ((n : ℝ) / 2)
  let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
    fun O => ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
      (singleBlockPrecision κ O)⁻¹
  change Integrable q (orthogonalHaar n) ∧ _
  have hsel := SelectedTilt.selected_tilt hn hκ
  change 0 < r ∧ r < 1 ∧ 0 < ℓ ∧ _ at hsel
  obtain ⟨hr, hr1, hℓ, _hell, _hcoeff, hmatch⟩ := hsel
  have hn3 : (3 : ℝ) ≤ n := by exact_mod_cast hn
  have hn0 : (0 : ℝ) < n := by linarith
  have hn1 : (0 : ℝ) < (n : ℝ) - 1 := by linarith
  have hs : 0 ≤ s := Real.sqrt_nonneg κ
  have hp : 0 < s + 1 := by linarith
  let a : ℝ := 1 - 1 / (n : ℝ)
  let p : ℝ := (n : ℝ) / 2
  let C : ℝ := (n : ℝ) * (s + 1) ^ 2 / (2 * ((n : ℝ) - 1))
  let b : Matrix.orthogonalGroup (Fin n) ℝ → ℝ := fun O =>
    1 + r ^ 2 - 2 * r * U O
  have ha : 0 < a := by
    have hdiv : (1 : ℝ) / n < 1 := (div_lt_one hn0).2 (by linarith)
    dsimp [a]
    linarith
  have hC : 0 < C := by dsimp [C]; positivity
  have htwoC : 2 * C = (s + 1) ^ 2 / a := by
    dsimp [C, a]
    field_simp [hn0.ne', hn1.ne']
  have hbpos (O : Matrix.orthogonalGroup (Fin n) ℝ) : 0 < b O := by
    have huabs : |U O| ≤ 1 := by
      simpa only [U, Real.norm_eq_abs] using
        entry_norm_bound_of_unitary O.property j0 j0
    have hu : U O ≤ 1 := (abs_le.mp huabs).2
    have hsq : 0 < (1 - r) ^ 2 := sq_pos_of_pos (sub_pos.mpr hr1)
    have hprod : 0 ≤ r * (1 - U O) := mul_nonneg hr.le (sub_nonneg.mpr hu)
    dsimp [b]
    nlinarith
  have hU : Continuous U := continuous_subtype_val.matrix_elem j0 j0
  have hbcont : Continuous b := by dsimp [b]; fun_prop
  have hqcont : Continuous q := by
    change Continuous (fun O => ((s + 1) * U O - (s - 1)) / (b O) ^ p)
    exact ((continuous_const.mul hU).sub continuous_const).div
      (hbcont.rpow_const (fun O => Or.inl (hbpos O).ne'))
      (fun O => (Real.rpow_pos_of_pos (hbpos O) p).ne')
  let := (orthogonalHaar_spec n).1
  have hqL : Integrable q (orthogonalHaar n) :=
    hqcont.integrable_of_hasCompactSupport (isClosed_tsupport q).isCompact
  have hpow2 : ((s + 1) ^ 2) ^ p = (s + 1) ^ n := by
    calc
      ((s + 1) ^ 2) ^ p = (s + 1) ^ ((2 : ℝ) * p) :=
        (Real.rpow_natCast_mul hp.le 2 p).symm
      _ = (s + 1) ^ (n : ℝ) := by congr 1; dsimp [p]; ring
      _ = (s + 1) ^ n := Real.rpow_natCast _ _
  have hscale : (2 : ℝ) ^ p * C ^ p = (s + 1) ^ n / a ^ p := by
    rw [← Real.mul_rpow (by norm_num : (0 : ℝ) ≤ 2) hC.le, htwoC,
      Real.div_rpow (sq_nonneg _) ha.le, hpow2]
  have hpref :
      (((-1 : ℝ) ^ (n - 1) * (s - 1) ^ (n - 1)) / (2 : ℝ) ^ p) * (C ^ p)⁻¹ =
        (((-1 : ℝ) ^ (n - 1) * (s - 1) ^ (n - 1)) / (s + 1) ^ n) * a ^ p := by
    calc
      _ = ((-1 : ℝ) ^ (n - 1) * (s - 1) ^ (n - 1)) /
          ((2 : ℝ) ^ p * C ^ p) := by
        simp only [div_eq_mul_inv, _root_.mul_inv_rev]
        ring
      _ = ((-1 : ℝ) ^ (n - 1) * (s - 1) ^ (n - 1)) /
          ((s + 1) ^ n / a ^ p) := by rw [hscale]
      _ = _ := by
        field_simp [(Real.rpow_pos_of_pos ha p).ne', pow_ne_zero n hp.ne']
  have hden (O : Matrix.orthogonalGroup (Fin n) ℝ) :
      κ + 1 + 4 * ℓ - (κ - 1) * U O = C * b O :=
    (hmatch (U O)).1.trans (hmatch (U O)).2
  have hg := GaussianExpectation.actual_gaussian_transform hn hκ hℓ.le
  refine ⟨hqL, ?_⟩
  calc
    _ = (((-1 : ℝ) ^ (n - 1) * (s - 1) ^ (n - 1)) / (2 : ℝ) ^ p) *
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          ((s + 1) * U O - (s - 1)) /
            (κ + 1 + 4 * ℓ - (κ - 1) * U O) ^ p ∂orthogonalHaar n) := hg.2.2
    _ = (((-1 : ℝ) ^ (n - 1) * (s - 1) ^ (n - 1)) / (2 : ℝ) ^ p) *
        ((C ^ p)⁻¹ * (∫ O, q O ∂orthogonalHaar n)) := by
      congr 1
      rw [← integral_const_mul]
      apply integral_congr_ae
      exact Filter.Eventually.of_forall fun O => by
        change ((s + 1) * U O - (s - 1)) /
          (κ + 1 + 4 * ℓ - (κ - 1) * U O) ^ p = (C ^ p)⁻¹ * q O
        rw [hden O, Real.mul_rpow hC.le (hbpos O).le]
        change ((s + 1) * U O - (s - 1)) / (C ^ p * (b O) ^ p) =
          (C ^ p)⁻¹ * (((s + 1) * U O - (s - 1)) / (b O) ^ p)
        simp only [div_eq_mul_inv, _root_.mul_inv_rev]
        ring
    _ = _ := by rw [← mul_assoc, hpref]

end AutoSamplingTheory.ExampleCases.GaussianComplexity.PoissonNormalization

Exact module and namespace context

Scope and omitted-condition boundaries

Normalized actual signed Gaussian expectation and absolute Haar integrability of its normalized scalar kernel. No sphere pushforward, either Poisson integral evaluation, Eq24 evaluated H, actual positive TV first ratio, amplification, oracle/query/cost, hidden-eigenbasis or main bounds. The source-omitted real-power scaling and normalized kernel L1 are supplied internally, not hypotheses.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

entry_norm_bound_of_unitary
Continuous.matrix_elem
Continuous.rpow_const
Continuous.div
Continuous.integrable_of_hasCompactSupport
Real.rpow_natCast_mul
Real.rpow_natCast
Real.mul_rpow
Real.div_rpow
Real.rpow_pos_of_pos
integral_const_mul
integral_congr_ae

Mathematical sources

Zhou–Suzuki, Eq. (21)–(24): normalization bridge — Normalized actual signed Gaussian expectation and absolute Haar integrability of its normalized scalar kernel. No sphere pushforward, either Poisson integral evaluation, Eq24 evaluated H, actual positive TV first ratio, amplification, oracle/query/cost, hidden-eigenbasis or main bounds. The source-omitted real-power scaling and normalized kernel L1 are supplied internally, not hypotheses.

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