DeterminantCancellation: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

A non-first principal minor has finite weighted expectation zero
Average the actual signed Gaussian normalization factor

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

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.

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.

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

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

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.