Normalize the signed Gaussian expectation

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling. This is the source-implicit positive real-power normalization joining Eq21 and Eq23, before the Poisson value is substituted in Eq24. Kernel absolute integrability and coefficient algebra are explicit here.

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

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

Source correspondence and review

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
B7 natural n>=3 and real kappa>=4; literal source Gaussian and full O(n) Haar.	Exactly the same hypotheses, objects and selected parameters. Actual U coordinate positivity and q L1 derived internally.	same	No integrability, selected-parameter bounds, positive denominator or Poisson identity added as a premise.
Eq23 is substituted into Eq21 before the Poisson value gives Eq24; positive real-power normalization and absolute kernel L1 are omitted.	Makes that unevaluated intermediate normalization and its L1 conclusion explicit.	source-implicit	These are necessary bookkeeping/analytic bridges. Full Eq24 evaluation remains an independent open consumer.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

conclusion: Relative to the raw paper, absolute L1 of the normalized kernel and the positive real-power intermediate coefficient are now explicit. The packet original already honestly includes this source-implicit bridge. This is an elaboration, not an extra assumption or an evaluated Eq24 theorem. — Pinned Eq21-23, transition p5.7 and Eq24; production hqL,hpow2,hscale,hpref and final calc; publication scope explicitly discloses source omission.
objects: Source O_11 and reconstruction O_00 name the same first coordinate under one-based source notation versus Fin n indexing. — Production j0=<0,...>; source A2.SS2.p2.1; current lesson A_O,gamma_O notation explicitly explains the index convention.
domains: The source uses positive-base half powers and meaningful expectations implicitly. Lean derives the actual coordinate bound, positive denominator, L1 and real-power rules from the original hypotheses; it does not add a free-u positivity assumption. — Production hbpos,hqcont,hqL and Real.mul_rpow invocation; current graph COORDINATE_RANGE -> REAL_POWER_SCALING; source Eq22-23 and actual O(n) context.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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.

Normalize the signed Gaussian expectation

Actual selected Gaussian normalization

Read the formalized proofs

Normalize the signed Gaussian expectation

Mathematical statement

All objects and hypotheses

Notation and interpretation

Mathematical proof

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?