Average the actual signed Gaussian normalization factor

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling. ASTIS mathematical restatement with source coordinate1 represented by Fin n coordinate0.

Complete source statement (Samplinglib restatement)

Let n>=3, kappa>=4, and let O have the actual full orthogonal Haar probability law. Write U=O_11 and A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O^T). For every Borel h with E|h(U)| finite, E[det(O)sqrt(det A_O)h(U)] equals ((-1)^(n-1)(sqrt(kappa)-1)^(n-1)/2^n) E[((sqrt(kappa)+1)U-(sqrt(kappa)-1))h(U)].

(15)

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

Average the actual signed Gaussian normalization factor

AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantCancellation.signed_sqrt_det_integral · theorem · Teaching coverage

Read this first

Mathematical statement

Let n≥3, kappa≥4, and let O have the actual full orthogonal Haar probability law. Write U=O_11 and A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O^T). For every Borel h with E|h(U)| finite, E[det(O)sqrt(det A_O)h(U)] equals ((-1)^(n-1)(sqrt(kappa)-1)^(n-1)/2^n) E[((sqrt(kappa)+1)U-(sqrt(kappa)-1))h(U)].

\[\mathbb E\!\left[\det(O)\sqrt{\det A_O}\,h(U)\right]=\frac{(-1)^{n-1}(\sqrt\kappa-1)^{n-1}}{2^n}\,\mathbb E\!\left[\bigl((\sqrt\kappa+1)U-(\sqrt\kappa-1)\bigr)h(U)\right]\]

Lean statement · signed_sqrt_det_integral

Source coordinate1 becomes Fin n coordinate0 with its membership proof derived from n>=3. The actual Haar and literal precision definitions are reused unchanged.

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 signed_sqrt_det_integral {n : ℕ} (hn : 3 ≤ n) {κ : ℝ} (hκ : 4 ≤ κ)
    (h : ℝ → ℝ) (hh : Measurable h)
    (hL1 : Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ => h ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n))) (orthogonalHaar n)) :
    (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        h ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n)) ∂orthogonalHaar n) =
      ((-1 : ℝ) ^ (n - 1) * (Real.sqrt κ - 1) ^ (n - 1) / (2 : ℝ) ^ n) *
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          ((Real.sqrt κ + 1) * ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n)) - (Real.sqrt κ - 1)) *
            h ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n)) ∂orthogonalHaar n)

Exact module and namespace context

Proof roadmap

1Reuse the signed pointwise normalizer
Put a=sqrt(kappa)+1 and b=sqrt(kappa)-1. The already compiled equation18 gives det(O)sqrt(det A_O)=2^(-n)det(aO-bI). Its positive square-root branch was proved internally in the earlier packet.
2Expand the determinant by multilinearity
Choose, independently in each row of aO+bI, either the O row or the identity row. Group choices by S. Extract row scalars and use the canonical principal-submatrix determinant identity. This yields an exact finite expansion, with no stochastic approximation.
3Pass only finite sums through the integral
For each S, integrable_minor_weight supplies the real L1 obligation. Thus finite-sum linearity and constant extraction are legal for the actual law. Every term whose S contains a non-first coordinate vanishes by the preceding public cancellation theorem.
4Evaluate the two survivors
If S has no non-first index, then S is empty or consists of the first coordinate. Their determinants are 1 and U. Hence the sum is (-b)^n E[h(U)]+a(-b)^(n-1)E[Uh(U)]. The bound |U|≤1 proves U h(U) is L1 from the source hypothesis.
5Keep the parity and normalization exact
Use n=(n-1)+1 and (-b)^(n-1)=(-1)^(n-1)b^(n-1), then combine the two finite expectations by integral linearity. The exact coefficient is the one in equation15.

Full assumptions and notation

All objects and hypotheses

n≥3 and real kappa≥4, retaining AppendixB2 standing assumptions.
The same actual full orthogonal Haar probability and the same literal equation4 precision A_O are used. Square roots are nonnegative real square roots.
h:R→R is Borel measurable with actual E|h(O_11)| finite. Weighted-minor integrability, cancellation, determinant expansion and all linearity conditions are derived internally.

Mathematical proof

1. Reuse the signed pointwise normalizer

Put a=sqrt(kappa)+1 and b=sqrt(kappa)-1. The already compiled equation18 gives det(O)sqrt(det A_O)=2^(-n)det(aO-bI). Its positive square-root branch was proved internally in the earlier packet.

\[\det(O)\sqrt{\det A_O}=2^{-n}\det(aO-bI)\]

Corresponding Lean step

The public proof calls the existing singleBlockPrecision_signed_sqrt_det on the identical actual precision. No Gaussian density normalization is assumed. The earlier Lean proof uses a squared-norm kernel contradiction and continuity; the source quantitative path norm lower bound remains a separately visible source estimate.

2. Expand the determinant by multilinearity

Choose, independently in each row of aO+bI, either the O row or the identity row. Group choices by S. Extract row scalars and use the canonical principal-submatrix determinant identity. This yields an exact finite expansion, with no stochastic approximation.

\[\det(aO+bI)=\sum_{S\subseteq[n]}a^{|S|}b^{n-|S|}\det(O_{S,S})\]

Corresponding Lean step

det_affine_principalMinor uses detRowAlternating.map_add_univ/map_smul_univ and Matrix.det_piecewise_one_eq_submatrix_det. The previously retrieved polynomial coefficient theorem is not called; the actual dependency is row multilinearity plus the canonical submatrix identity.

3. Pass only finite sums through the integral

For each S, integrable_minor_weight supplies the real L1 obligation. Thus finite-sum linearity and constant extraction are legal for the actual law. Every term whose S contains a non-first coordinate vanishes by the preceding public cancellation theorem.

\[\mathbb E[\det(aO-bI)h(U)]=\sum_S a^{|S|}(-b)^{n-|S|}\mathbb E[\det(O_{S,S})h(U)]\]

Corresponding Lean step

The private affine_det_weighted_average genuinely consumes principalMinor_weighted_integral_eq_zero, checks each integral_finsetSum premise and reduces the finite sum using Finset.sum_subset.

4. Evaluate the two survivors

If S has no non-first index, then S is empty or consists of the first coordinate. Their determinants are 1 and U. Hence the sum is (-b)^n E[h(U)]+a(-b)^(n-1)E[Uh(U)]. The bound |U|≤1 proves U h(U) is L1 from the source hypothesis.

\[\mathbb E[\det(aO-bI)h(U)]=(-b)^n\mathbb E[h(U)]+a(-b)^{n-1}\mathbb E[Uh(U)]\]

Corresponding Lean step

Empty and singleton determinants use det_eq_one_of_card_eq_zero and det_eq_elem_of_card_eq_one. entry_norm_bound_of_unitary and Integrable.bdd_mul supply the actual weighted-coordinate integrability.

5. Keep the parity and normalization exact

Use n=(n-1)+1 and (-b)^(n-1)=(-1)^(n-1)b^(n-1), then combine the two finite expectations by integral linearity. The exact coefficient is the one in equation15.

\[2^{-n}(-b)^{n-1}\bigl(a\mathbb E[Uh(U)]-b\mathbb E[h(U)]\bigr)=\frac{(-1)^{n-1}b^{n-1}}{2^n}\mathbb E[(aU-b)h(U)]\]

Corresponding Lean step

The final proof uses integral_sub with actual L1 arguments and elementary ring identities. Concrete tests check the nonzero averages -1/8 for n3 and +1/16 for n4 at kappa4, so discarding the empty term or losing parity is detected.

Lean verification

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

Lean proof · signed_sqrt_det_integral

The exact module derives integrability, reflection algebra, law preservation, finite expansion and survivor evaluation internally. The Borel premise is retained from the source even where L1 already supplies the measurability needed by a bounded-multiplier step.

Download module (.lean)

theorem signed_sqrt_det_integral {n : ℕ} (hn : 3 ≤ n) {κ : ℝ} (hκ : 4 ≤ κ)
    (h : ℝ → ℝ) (hh : Measurable h)
    (hL1 : Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ => h ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n))) (orthogonalHaar n)) :
    (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        h ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n)) ∂orthogonalHaar n) =
      ((-1 : ℝ) ^ (n - 1) * (Real.sqrt κ - 1) ^ (n - 1) / (2 : ℝ) ^ n) *
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          ((Real.sqrt κ + 1) * ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n)) - (Real.sqrt κ - 1)) *
            h ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n)) ∂orthogonalHaar n) := by
  classical
  let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
  let U (O : Matrix.orthogonalGroup (Fin n) ℝ) : ℝ :=
    (O : Matrix (Fin n) (Fin n) ℝ) j0 j0
  let g : Matrix.orthogonalGroup (Fin n) ℝ → ℝ := fun O => h (U O)
  let a := Real.sqrt κ + 1
  let b := Real.sqrt κ - 1
  change (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        g O ∂orthogonalHaar n) =
    ((-1 : ℝ) ^ (n - 1) * b ^ (n - 1) / (2 : ℝ) ^ n) *
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ, (a * U O - b) * g O ∂orthogonalHaar n)
  have hnorm : ∀ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det =
        (1 / (2 : ℝ) ^ n) *
          (a • (O : Matrix (Fin n) (Fin n) ℝ) + (-b) • (1 : Matrix (Fin n) (Fin n) ℝ)).det := by
    intro O
    simpa only [a, b, neg_smul, sub_eq_add_neg] using singleBlockPrecision_signed_sqrt_det hn hκ O
  have hstep : (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        g O ∂orthogonalHaar n) =
      (1 / (2 : ℝ) ^ n) * (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (a • (O : Matrix (Fin n) (Fin n) ℝ) + (-b) • (1 : Matrix (Fin n) (Fin n) ℝ)).det *
          g O ∂orthogonalHaar n) := by
    calc
      _ = ∫ O : Matrix.orthogonalGroup (Fin n) ℝ, (1 / (2 : ℝ) ^ n) *
          ((a • (O : Matrix (Fin n) (Fin n) ℝ) + (-b) •
            (1 : Matrix (Fin n) (Fin n) ℝ)).det * g O) ∂orthogonalHaar n := by
        apply integral_congr_ae
        exact Filter.Eventually.of_forall fun O => by
          dsimp only
          rw [hnorm O]
          ring
      _ = _ := integral_const_mul _ _
  have havg := affine_det_weighted_average hn a (-b) h hh hL1
  change (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (a • (O : Matrix (Fin n) (Fin n) ℝ) + (-b) • (1 : Matrix (Fin n) (Fin n) ℝ)).det *
        g O ∂orthogonalHaar n) =
      (-b) ^ n * (∫ O, g O ∂orthogonalHaar n) +
        a * (-b) ^ (n - 1) * (∫ O, U O * g O ∂orthogonalHaar n) at havg
  have hUc : Continuous U := by
    dsimp only [U]
    exact (continuous_apply j0).comp ((continuous_apply j0).comp continuous_subtype_val)
  have hU : Integrable (fun O => U O * g O) (orthogonalHaar n) :=
    hL1.bdd_mul hUc.measurable.aestronglyMeasurable
      (show ∀ᵐ O : Matrix.orthogonalGroup (Fin n) ℝ ∂orthogonalHaar n, ‖U O‖ ≤ (1 : ℝ) from
        Filter.Eventually.of_forall fun O => entry_norm_bound_of_unitary O.property j0 j0)
  have hlin : (∫ O : Matrix.orthogonalGroup (Fin n) ℝ, (a * U O - b) * g O ∂orthogonalHaar n) =
      a * (∫ O, U O * g O ∂orthogonalHaar n) - b * (∫ O, g O ∂orthogonalHaar n) := by
    calc
      _ = ∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          a * (U O * g O) - b * g O ∂orthogonalHaar n := by
        apply integral_congr_ae
        exact Filter.Eventually.of_forall fun O => by ring
      _ = _ := by
        rw [integral_sub (hU.const_mul a) (hL1.const_mul b), integral_const_mul, integral_const_mul]
  rw [hstep, havg, hlin]
  have hn' : n - 1 + 1 = n := by omega
  have hp : (-b) ^ n = (-b) ^ (n - 1) * (-b) := by
    conv_lhs => rw [← hn', pow_succ]
  rw [hp]
  rw [neg_pow b (n - 1)]
  simp only [div_eq_mul_inv]
  ring


end AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantCancellation

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Borel h, E\|h(U)\| finite, actual full orthogonal Haar law; n>=3 and kappa>=4 where the precision normalizer is used. A selected reflected row belongs to S and differs from the first coordinate.	The same actual law and Borel/L1 source binders. Weighted minor integrability and its finite bounds are outputs/internal dependencies; no h boundedness, SO restriction or assumed cancellation is introduced.	same	The source sharp1 minor bound is replaced only for the finiteness subproof by continuous compact boundedness with a finite C. This is an explicit sufficient proof-route difference, not a source repair or changed theorem. All final constants, quantifiers and parity are exact.

Only the actual LemmaB6 signed normalization integral identity and finite weighted principal-minor cancellation. Gaussian laws/densities, Fubini, spherical Poisson identities, radial/Hellinger separation, determinant-conditioned posteriors and transcript equality, eigenbasis/Krylov reductions and both main lower bounds remain separate open obligations. The source sharp principal-minor bound1 and path norm lower bound2 are not separately claimed as compiled estimates: sufficient alternate finiteness/kernel routes are explicitly disclosed.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

objects: Source coordinate 1 is Lean Fin n coordinate 0; this is consistent in U, the excluded reflected index and singleton survivor. — Raw U:=O_11 and S={1}; module j0:=0 and survivor {j0}.
scopes: The Lean proof uses compactness to obtain a finite principal-minor bound rather than proving the source sharp bound one. The lesson explicitly states this limitation; the same L1 and cancellation conclusions follow. — Raw p3.3 sharp bound; private integrable_minor_weight uses continuous principal determinant and compactness before Integrable.bdd_mul.

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

Only the actual LemmaB6 signed normalization integral identity and finite weighted principal-minor cancellation. Gaussian laws/densities, Fubini, spherical Poisson identities, radial/Hellinger separation, determinant-conditioned posteriors and transcript equality, eigenbasis/Krylov reductions and both main lower bounds remain separate open obligations. The source sharp principal-minor bound1 and path norm lower bound2 are not separately claimed as compiled estimates: sufficient alternate finiteness/kernel routes are explicitly disclosed.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Matrix.detRowAlternating
AlternatingMap.map_add_univ
AlternatingMap.map_smul_univ
Matrix.det_piecewise_one_eq_submatrix_det
MeasureTheory.integral_finsetSum
Matrix.det_eq_one_of_card_eq_zero
Matrix.det_eq_elem_of_card_eq_one
MeasureTheory.integral_sub
entry_norm_bound_of_unitary

Mathematical sources

LemmaB6 and its complete author proof — The integral identity and scoped finite minor cancellation only.

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

Average the actual signed Gaussian normalization factor

Complete source statement (Samplinglib restatement)

(15)

Read the formalized proofs

Average the actual signed Gaussian normalization factor

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Reuse the signed pointwise normalizer

2. Expand the determinant by multilinearity

3. Pass only finite sums through the integral

4. Evaluate the two survivors

5. Keep the parity and normalization exact

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?