Samplinglib mathematical lesson

Normalize the actual positive and negative determinant Haar priors

AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantComponents.component_probabilities · theorem · Teaching coverage

Read this first

Mathematical statement

Let n be a positive natural number and mu the existing normalized Borel Haar probability on the full real orthogonal group O(n). Put Cplus={O:det(O)=1} and Cminus={O:det(O)=-1}. Then mu(Cplus)=mu(Cminus)=1/2, and both literal measures 2 times mu restricted to Cplus and 2 times mu restricted to Cminus are probability measures. All determinant-event measurability, partition, negative-determinant witness and invariance requirements are established internally. This explicitly generalizes the source application n≥3 to n≥1; dimension0 is excluded because its negative determinant event is empty. No Gaussian target-mixture measure or TV conclusion is asserted.

\[\mu(C_+)=\mu(C_-)=\frac12,\qquad \nu_\pm=2\,\mu|_{C_\pm},\qquad\nu_\pm(O(n))=1\]

Lean statement · component_probabilities

Exact preproof sealed signature: actual full Haar, determinant level sets, both half-masses and actual literal restriction probabilities.

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 component_probabilities {n : ℕ} (hn : 0 < n) :
    let μ := orthogonalHaar n
    let Cpos : Set (Matrix.orthogonalGroup (Fin n) ℝ) :=
      {O | (O : Matrix (Fin n) (Fin n) ℝ).det = 1}
    let Cneg : Set (Matrix.orthogonalGroup (Fin n) ℝ) :=
      {O | (O : Matrix (Fin n) (Fin n) ℝ).det = -1}
    μ Cpos = (2 : ℝ≥0∞)⁻¹ ∧ μ Cneg = (2 : ℝ≥0∞)⁻¹ ∧
    IsProbabilityMeasure ((2 : ℝ≥0∞) • μ.restrict Cpos) ∧
    IsProbabilityMeasure ((2 : ℝ≥0∞) • μ.restrict Cneg)

Exact module and namespace context

Proof roadmap

1Identify the actual two Borel events
The determinant is continuous on real matrices and hence on O(n), so its level sets are Borel. Orthogonality gives det(O)^2=1. Over the reals this says det(O)=1 or det(O)=-1, with disjoint alternatives. Thus Cminus is exactly the complement of Cplus.
2Construct a sign-changing symmetry in positive dimension
Because n≥1, the zeroth coordinate exists. Negate that coordinate and fix the others. The diagonal matrix R is orthogonal, its determinant is -1, and det(RO)=-det(O). Consequently the preimage of Cplus under left multiplication by R is Cminus.
3Use the same canonical full-Haar invariance
Left multiplication by the fixed R preserves the identical full-Haar probability already used elsewhere. Applying the map-measure formula to the Borel event Cplus and substituting the preimage identity yields equality of the two component masses. This elementary argument supplies the justification omitted from the source paragraph.
4Solve the mass equation using actual probability
The events partition the whole group and mu is a probability measure, so their masses sum to1. Combining equal masses with this identity gives each mass1/2. In Lean, finiteness permits a faithful ENNReal-to-real calculation and injectivity returns the ENNReal equality; no infinite-value cancellation is used.
5Normalize the literal restricted mixing priors
For either sign define the actual measure nu by scaling the restriction of mu by2. The mass of its whole carrier is2 times the already proved component mass, hence1. Therefore both literal measures are genuine probabilities. These are the normalized priors needed by later Gaussian mixtures; this step does not construct those mixtures.

Full assumptions and notation

All objects and hypotheses

Positive natural dimension n≥1; source application retains n≥3. The n=0 obstruction is explicit.
Identical actual normalized full-O(n) Borel Haar law; no arbitrary measure, SO replacement, equal-mass assumption or supplied negative-determinant matrix.
No kappa, ell, Gaussian, integrability or query-budget hypotheses are relevant to this probability-normalization prerequisite.

Mathematical proof

1. Identify the actual two Borel events

The determinant is continuous on real matrices and hence on O(n), so its level sets are Borel. Orthogonality gives det(O)^2=1. Over the reals this says det(O)=1 or det(O)=-1, with disjoint alternatives. Thus Cminus is exactly the complement of Cplus.

\[\det(O)^2=1,\quad C_-=C_+^c,\quad C_+\sqcup C_-=O(n)\]

Corresponding Lean step

Continuity, determinant product/transpose and mul_self_eq_one_iff produce the measurable partition; it is not a caller premise.

2. Construct a sign-changing symmetry in positive dimension

Because n≥1, the zeroth coordinate exists. Negate that coordinate and fix the others. The diagonal matrix R is orthogonal, its determinant is -1, and det(RO)=-det(O). Consequently the preimage of Cplus under left multiplication by R is Cminus.

\[R=\operatorname{diag}(-1,1,\ldots,1),\quad\det(R)=-1,\quad L_R^{-1}(C_+)=C_-\]

Corresponding Lean step

The proof constructs R as a local actual orthogonal matrix and proves its determinant and preimage identity internally. No reflection witness is supplied by the caller.

3. Use the same canonical full-Haar invariance

Left multiplication by the fixed R preserves the identical full-Haar probability already used elsewhere. Applying the map-measure formula to the Borel event Cplus and substituting the preimage identity yields equality of the two component masses. This elementary argument supplies the justification omitted from the source paragraph.

\[(L_R)_*\mu=\mu\quad\Longrightarrow\quad\mu(C_+)=\mu(L_R^{-1}C_+)=\mu(C_-)\]

Corresponding Lean step

The proof calls the exact compiled orthogonalHaar_map_mul_left and Measure.map_apply. The source omission stays explicit; no distinct Haar or SO law is introduced.

4. Solve the mass equation using actual probability

The events partition the whole group and mu is a probability measure, so their masses sum to1. Combining equal masses with this identity gives each mass1/2. In Lean, finiteness permits a faithful ENNReal-to-real calculation and injectivity returns the ENNReal equality; no infinite-value cancellation is used.

\[\mu(C_+)+\mu(C_-)=1,\quad\mu(C_+)=\mu(C_-)\quad\Longrightarrow\quad\mu(C_\pm)=\frac12\]

Corresponding Lean step

The exact orthogonalHaar_spec probability, measure_add_measure_compl, measure_ne_top and finite toReal equality discharge normalization.

5. Normalize the literal restricted mixing priors

For either sign define the actual measure nu by scaling the restriction of mu by2. The mass of its whole carrier is2 times the already proved component mass, hence1. Therefore both literal measures are genuine probabilities. These are the normalized priors needed by later Gaussian mixtures; this step does not construct those mixtures.

\[\nu_\pm(O(n))=2\,\mu(C_\pm)=2\cdot\frac12=1\]

Corresponding Lean step

Measure.smul_apply and Measure.restrict_apply_univ consume the actual half-mass equalities; ENNReal.mul_inv_cancel is used only for finite nonzero2.

Lean verification

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

Lean proof · component_probabilities

Construct a fixed coordinate reflection, apply the same canonical Haar-left-map theorem, use the measurable complement partition, and normalize both actual restrictions.

Download module (.lean)

theorem component_probabilities {n : ℕ} (hn : 0 < n) :
    let μ := orthogonalHaar n
    let Cpos : Set (Matrix.orthogonalGroup (Fin n) ℝ) :=
      {O | (O : Matrix (Fin n) (Fin n) ℝ).det = 1}
    let Cneg : Set (Matrix.orthogonalGroup (Fin n) ℝ) :=
      {O | (O : Matrix (Fin n) (Fin n) ℝ).det = -1}
    μ Cpos = (2 : ℝ≥0∞)⁻¹ ∧ μ Cneg = (2 : ℝ≥0∞)⁻¹ ∧
    IsProbabilityMeasure ((2 : ℝ≥0∞) • μ.restrict Cpos) ∧
    IsProbabilityMeasure ((2 : ℝ≥0∞) • μ.restrict Cneg) := by
  classical
  dsimp only
  let μ := orthogonalHaar n
  let G := Matrix.orthogonalGroup (Fin n) ℝ
  let Cpos : Set G := {O | (O : Matrix (Fin n) (Fin n) ℝ).det = 1}
  let Cneg : Set G := {O | (O : Matrix (Fin n) (Fin n) ℝ).det = -1}
  let := (orthogonalHaar_spec n).1
  have hcont : Continuous (fun O : G => (O : Matrix (Fin n) (Fin n) ℝ).det) := by
    fun_prop
  have hpos : MeasurableSet Cpos := (isClosed_eq hcont continuous_const).measurableSet
  have hsign (O : G) : (O : Matrix (Fin n) (Fin n) ℝ).det = 1 ∨
      (O : Matrix (Fin n) (Fin n) ℝ).det = -1 := by
    have h := congrArg Matrix.det
      ((Matrix.mem_orthogonalGroup_iff (Fin n) ℝ).mp O.property)
    rw [Matrix.det_mul, Matrix.det_transpose, Matrix.det_one] at h
    exact mul_self_eq_one_iff.mp h
  let i : Fin n := ⟨0, hn⟩
  let R : G := ⟨Matrix.diagonal (fun j => if j = i then (-1 : ℝ) else 1), by
    apply (Matrix.mem_orthogonalGroup_iff (Fin n) ℝ).2
    rw [Matrix.diagonal_transpose, Matrix.diagonal_mul_diagonal]
    have heq : (fun j : Fin n => (if j = i then (-1 : ℝ) else 1) *
        (if j = i then (-1 : ℝ) else 1)) = fun _ => (1 : ℝ) := by
      funext j
      by_cases hj : j = i <;> simp [hj]
    rw [heq, Matrix.diagonal_one]⟩
  have hR : (R : Matrix (Fin n) (Fin n) ℝ).det = -1 := by
    simp [R, Matrix.det_diagonal]
  have hswap : (fun O : G => R * O) ⁻¹' Cpos = Cneg := by
    ext O
    change ((R : Matrix (Fin n) (Fin n) ℝ) *
      (O : Matrix (Fin n) (Fin n) ℝ)).det = 1 ↔
        (O : Matrix (Fin n) (Fin n) ℝ).det = -1
    rw [Matrix.det_mul, hR, neg_one_mul]
    constructor <;> intro h <;> linarith
  have hequal : μ Cpos = μ Cneg := by
    calc
      μ Cpos = (μ.map (fun O : G => R * O)) Cpos := by
        rw [orthogonalHaar_map_mul_left]
      _ = μ ((fun O : G => R * O) ⁻¹' Cpos) :=
        Measure.map_apply (by fun_prop) hpos
      _ = μ Cneg := by rw [hswap]
  have hcompl : Cposᶜ = Cneg := by
    ext O
    change ¬ (O : Matrix (Fin n) (Fin n) ℝ).det = 1 ↔
      (O : Matrix (Fin n) (Fin n) ℝ).det = -1
    rcases hsign O with h | h <;> norm_num [h]
  have hadd : μ Cpos + μ Cneg = 1 := by
    rw [← hcompl, measure_add_measure_compl hpos]
    exact measure_univ
  have hp : μ Cpos = (2 : ℝ≥0∞)⁻¹ := by
    apply (ENNReal.toReal_eq_toReal_iff' (measure_ne_top μ Cpos) (by simp)).mp
    have h := congrArg ENNReal.toReal hadd
    rw [ENNReal.toReal_add (measure_ne_top μ Cpos) (measure_ne_top μ Cneg),
      ← hequal] at h
    norm_num at h ⊢
    linarith
  have hm : μ Cneg = (2 : ℝ≥0∞)⁻¹ := hequal.symm.trans hp
  refine ⟨hp, hm, ⟨?_⟩, ⟨?_⟩⟩
  · rw [Measure.smul_apply, Measure.restrict_apply_univ, hp]
    exact ENNReal.mul_inv_cancel (by norm_num) (by norm_num)
  · rw [Measure.smul_apply, Measure.restrict_apply_univ, hm]
    exact ENNReal.mul_inv_cancel (by norm_num) (by norm_num)

end AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantComponents

Exact module and namespace context

Scope and omitted-condition boundaries

Actual full-Haar component masses and literal2*restriction mixing-prior probabilities only. No actual Gaussian-family kernel/target mixtures, H expectation split, TV, adaptive posterior/transcript, sphere/Poisson, parameter choice or either main lower bound. n≥1 is a disclosed background generalization; n=0 excluded. Source omits the elementary symmetry argument; the supplied background proof is not attributed as an explicit author proof.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Matrix.mem_orthogonalGroup_iff
Matrix.det_mul
Matrix.det_transpose
Matrix.det_diagonal
mul_self_eq_one_iff
Measure.map_apply
measure_add_measure_compl
ENNReal.toReal_eq_toReal_iff'
ENNReal.toReal_add
Measure.smul_apply
Measure.restrict_apply_univ
ENNReal.mul_inv_cancel

Mathematical sources

Determinant-component half-mass and normalized priors — Half-mass clause and explicitly supplied elementary background normalization 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.