A non-first principal minor has finite weighted expectation zero

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 and let O be drawn from the actual normalized Haar probability on the full real orthogonal group O(n). Put U=O_11. Let h:R->R be Borel with E|h(U)| finite. If a principal index set S contains an index i other than the first coordinate, then det(O_(S,S))h(U) is integrable and its expectation is zero. The empty principal determinant equals one.

weighted minor

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

A non-first principal minor has finite weighted expectation zero

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

Read this first

Mathematical statement

Let n≥3 and let O be drawn from the actual normalized Haar probability on the full real orthogonal group O(n). Put U=O_11. Let h:R→R be Borel with E|h(U)| finite. If a principal index set S contains an index i other than the first coordinate, then det(O_(S,S))h(U) is integrable and its expectation is zero. The empty principal determinant equals one.

\[i\in S,\ i\ne1\quad\Longrightarrow\quad\det(O_{S,S})h(U)\in L^1(\mu_n),\qquad\mathbb E_{\mu_n}[\det(O_{S,S})h(U)]=0\]

Lean statement · principalMinor_weighted_integral_eq_zero

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 principalMinor_weighted_integral_eq_zero {n : ℕ} (hn : 3 ≤ n)
    (S : Finset (Fin n)) (i : Fin n) (hiS : i ∈ S) (hi0 : i ≠ (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n))
    (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)) :
    Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ => ((O : Matrix (Fin n) (Fin n) ℝ).submatrix (Subtype.val : S → Fin n) (Subtype.val : S → Fin n)).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) ∧
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ, ((O : Matrix (Fin n) (Fin n) ℝ).submatrix (Subtype.val : S → Fin n) (Subtype.val : S → Fin n)).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) = 0

Exact module and namespace context

Proof roadmap

1Establish finite weighted expectations first
A principal determinant is continuous as a function of O. The actual full orthogonal group is compact, as proved in the shared Haar module. Hence each such determinant has some finite uniform norm bound C. Multiplying the given L1 function h(U) by this bounded measurable multiplier is integrable. The source uses the sharper bound |det O_(S,S)|≤1; the Lean proof needs only finite C and does not claim the sharp estimate itself.
2Reflect exactly one selected row
Let D_i be diagonal with -1 in coordinate i and +1 elsewhere. Its square is identity, so it is genuinely orthogonal. Left multiplication flips precisely row i. On the S principal submatrix, the diagonal row multiplier has determinant -1. Since i differs from the first coordinate, U is unchanged.
3Use the existing law and cancel
The actual shared Haar law has the same pushforward under O→D_iO. The weighted integrand changes sign, so its integral equals its own negative. Together with the already proved L1 statement, this is a finite expectation equal to zero.

Full assumptions and notation

All objects and hypotheses

n≥3; S is a finite principal index set and i belongs to S but is not the first coordinate.
The probability law is the existing concrete full orthogonal Haar law, with inherited finite real matrix topology and its Borel sigma-algebra. No restriction to SO(n) or determinant-conditioned law.
h:R→R is Borel measurable, and its actual composition with U=O_11 is integrable under that Haar probability. h itself need not be bounded.

Mathematical proof

1. Establish finite weighted expectations first

A principal determinant is continuous as a function of O. The actual full orthogonal group is compact, as proved in the shared Haar module. Hence each such determinant has some finite uniform norm bound C. Multiplying the given L1 function h(U) by this bounded measurable multiplier is integrable. The source uses the sharper bound |det O_(S,S)|≤1; the Lean proof needs only finite C and does not claim the sharp estimate itself.

\[|\det O_{S,S}|\le C_{n,S}<\infty\quad\Longrightarrow\quad\mathbb E|\det(O_{S,S})h(U)|\le C_{n,S}\mathbb E|h(U)|<\infty\]

Corresponding Lean step

integrable_minor_weight uses Continuous.matrix_submatrix/matrix_det, IsCompact.exists_bound_of_continuousOn and Integrable.bdd_mul. The compactness instance is the actual one constructed in the shared orthogonal Haar module. No estimate is a new public hypothesis.

2. Reflect exactly one selected row

Let D_i be diagonal with -1 in coordinate i and +1 elsewhere. Its square is identity, so it is genuinely orthogonal. Left multiplication flips precisely row i. On the S principal submatrix, the diagonal row multiplier has determinant -1. Since i differs from the first coordinate, U is unchanged.

\[(D_iO)_{11}=U,\qquad\det((D_iO)_{S,S})=-\det(O_{S,S})\]

Corresponding Lean step

Private rowReflection is the literal diagonal matrix, with orthogonality proved in its constructor. reflection_minor_det factors the restricted diagonal and uses det_mul, det_diagonal and the exact single negative factor.

3. Use the existing law and cancel

The actual shared Haar law has the same pushforward under O→D_iO. The weighted integrand changes sign, so its integral equals its own negative. Together with the already proved L1 statement, this is a finite expectation equal to zero.

\[I=\mathbb E[\det((D_iO)_{S,S})h((D_iO)_{11})]=-I\quad\Longrightarrow\quad I=0\]

Corresponding Lean step

The proof genuinely calls orthogonalHaar_map_mul_left, then MeasurableEmbedding.integral_map and integral_neg. The public conclusion includes integrability, so Lean's default value for a nonintegrable Bochner integral cannot masquerade as this finite expectation.

Lean verification

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

Lean proof · principalMinor_weighted_integral_eq_zero

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 principalMinor_weighted_integral_eq_zero {n : ℕ} (hn : 3 ≤ n)
    (S : Finset (Fin n)) (i : Fin n) (hiS : i ∈ S) (hi0 : i ≠ (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n))
    (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)) :
    Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ => ((O : Matrix (Fin n) (Fin n) ℝ).submatrix (Subtype.val : S → Fin n) (Subtype.val : S → Fin n)).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) ∧
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ, ((O : Matrix (Fin n) (Fin n) ℝ).submatrix (Subtype.val : S → Fin n) (Subtype.val : S → Fin n)).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) = 0 := by
  classical
  refine ⟨integrable_minor_weight S _ hL1, ?_⟩
  let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
  have hji : j0 ≠ i := Ne.symm hi0
  let F : Matrix.orthogonalGroup (Fin n) ℝ → ℝ := fun O =>
    ((O : Matrix (Fin n) (Fin n) ℝ).submatrix
      (Subtype.val : S → Fin n) (Subtype.val : S → Fin n)).det *
        h ((O : Matrix (Fin n) (Fin n) ℝ) j0 j0)
  change (∫ O, F O ∂orthogonalHaar n) = 0
  have hodd : ∀ O, F (rowReflection i * O) = -F O := by
    intro O
    dsimp only [F]
    rw [reflection_minor_det S i hiS O]
    have hu : (rowReflection i * O : Matrix.orthogonalGroup (Fin n) ℝ).val j0 j0 =
        (O : Matrix (Fin n) (Fin n) ℝ) j0 j0 := by
      simpa only [if_neg hji, one_mul] using reflection_mul_apply i O j0 j0
    rw [hu]
    ring
  have hemb : MeasurableEmbedding
      (fun O : Matrix.orthogonalGroup (Fin n) ℝ => rowReflection i * O) :=
    (MeasurableEquiv.mulLeft (rowReflection i)).measurableEmbedding
  have heq : (∫ O, F (rowReflection i * O) ∂orthogonalHaar n) =
      ∫ O, F O ∂orthogonalHaar n := by
    rw [← hemb.integral_map, orthogonalHaar_map_mul_left]
  have hz : -(∫ O, F O ∂orthogonalHaar n) = ∫ O, F O ∂orthogonalHaar n := by
    simpa only [hodd, integral_neg] using heq
  linarith

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)

Continuous.matrix_submatrix
Continuous.matrix_det
IsCompact.exists_bound_of_continuousOn
MeasureTheory.Integrable.bdd_mul
Matrix.det_mul
Matrix.det_diagonal
MeasurableEmbedding.integral_map
MeasureTheory.integral_neg

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.

A non-first principal minor has finite weighted expectation zero

Complete source statement (Samplinglib restatement)

weighted minor

Read the formalized proofs

A non-first principal minor has finite weighted expectation zero

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Establish finite weighted expectations first

2. Reflect exactly one selected row

3. Use the existing law and cancel

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?