The full orthogonal group has a unique Haar probability
AutoSamplingTheory.TechnicalLemmas.Probability.OrthogonalHaar.existsUnique_orthogonalHaar · theorem · Teaching coverage
Mathematical statement
For every natural finite dimension n, the full real orthogonal group O(n), with its inherited matrix topology and Borel sigma-algebra, has exactly one measure which is both a probability and a Haar measure. This explicates the standard Haar background invoked in the source.
Lean statement · existsUnique_orthogonalHaar
The measure lives on the actual full orthogonal subtype with its canonical Borel space. No abstract Haar law or compactness premise is supplied by the caller.
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.
theorem existsUnique_orthogonalHaar (n : ℕ) :
∃! μ : Measure (Matrix.orthogonalGroup (Fin n) ℝ),
IsProbabilityMeasure μ ∧ μ.IsHaarMeasureProof roadmap
- 1The group is compact in its actual matrix topology
Orthogonality bounds every real matrix entry in absolute value by one. The unitary set is closed, so O(n) is a closed subset of the finite product cube [-1,1]^(n times n). The cube is compact. Identity supplies nonemptiness even at n=0; the subspace is second countable and has its canonical Borel structure.
- 2Normalize and identify the unique law
Apply the actual Mathlib Haar constructor with positive compact normalization set K0 equal to the whole compact group. The constructor assigns K0 mass one. Haar uniqueness on the second-countable group shows that any other Haar probability is equal to this one.
Full assumptions and notation
All objects and hypotheses
- n is an arbitrary natural finite dimension. The paper applications use n≥3 or d≥2; the shared background also covers n=0.
- O(n) is the full real orthogonal group O^T O=I, equipped with the subspace topology of finite real matrices and its Borel sigma-algebra. Both determinant signs are allowed whenever they exist.
- Haar means left invariant, finite on compact sets and positive on nonempty open sets. Probability means total mass one. Compactness and second countability are proved internally, not assumed as public premises.
Mathematical proof
1. The group is compact in its actual matrix topology
Orthogonality bounds every real matrix entry in absolute value by one. The unitary set is closed, so O(n) is a closed subset of the finite product cube [-1,1]^(n times n). The cube is compact. Identity supplies nonemptiness even at n=0; the subspace is second countable and has its canonical Borel structure.
Corresponding Lean step
Private instances construct the canonical Borel space, induced second countability and compactness from entry_norm_bound_of_unitary, isClosed_unitary and isCompact_Icc. They do not add source assumptions.
2. Normalize and identify the unique law
Apply the actual Mathlib Haar constructor with positive compact normalization set K0 equal to the whole compact group. The constructor assigns K0 mass one. Haar uniqueness on the second-countable group shows that any other Haar probability is equal to this one.
Corresponding Lean step
haarMeasure_self and PositiveCompacts.coe_top give probability; the constructor supplies IsHaarMeasure; isHaarMeasure_eq_of_isProbabilityMeasure gives equality for every competing measure.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · existsUnique_orthogonalHaar
The adjacent exact Lean constructs the law and discharges its topology, normalization and invariance dependencies 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.
theorem existsUnique_orthogonalHaar (n : ℕ) :
∃! μ : Measure (Matrix.orthogonalGroup (Fin n) ℝ),
IsProbabilityMeasure μ ∧ μ.IsHaarMeasure := by
let μ : Measure (Matrix.orthogonalGroup (Fin n) ℝ) :=
Measure.haarMeasure (⊤ : PositiveCompacts (Matrix.orthogonalGroup (Fin n) ℝ))
have hprob : IsProbabilityMeasure μ := ⟨by
simpa only [μ, PositiveCompacts.coe_top] using
(Measure.haarMeasure_self (K₀ :=
(⊤ : PositiveCompacts (Matrix.orthogonalGroup (Fin n) ℝ))))⟩
have hhaar : μ.IsHaarMeasure := by dsimp only [μ]; infer_instance
refine ⟨μ, ⟨hprob, hhaar⟩, ?_⟩
intro ν hν
let := hprob
let := hhaar
let := hν.1
let := hν.2
exact Measure.isHaarMeasure_eq_of_isProbabilityMeasure ν μSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The paper invokes full orthogonal Haar probability in dimension n>=3 or d>=2 and uses fixed row-reflection invariance. | All natural finite dimensions, canonical Borel full group, actual Haar constructor. The n=0 case is a singleton; no determinant component or conditional law is asserted. | generalization | Standard background is expanded and proved internally. This disclosed dimension extension does not strengthen the paper conclusions or identify the two experiments beyond their common full Haar law. |
Only the common full orthogonal Haar probability and fixed left multiplication invariance. Determinant-conditioned laws, component half-mass, principal-minor sign/zero expectation, Gaussian densities, independence from an algorithm seed, adaptive posterior invariance, Krylov reduction and both main lower bounds remain open. Dimension zero is included as a singleton group; no two-components claim is made there.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: The shared Haar background is validly extended beyond the source application dimensions, including the singleton case n=0. — The raw applications are in n>=3 (Section B.2) or d>=2 (Section 4.1); the candidate expressly extends only the standard Haar background to all natural dimensions. The n=0 carrier is a singleton, so this extension is valid and does not import the source's two-component statement into dimension zero.
- scopes: The candidate explicates the standard Haar background invoked by the paper rather than reproducing a verbatim source theorem. — The pinned original_text is an attributed ASTIS explication of the source's Haar notation, rather than a verbatim theorem proved in the paper. The construction/uniqueness/topology details are checked here against the current full module and pinned APIs; source attribution and source scope identify them as shared background.
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 common full orthogonal Haar probability and fixed left multiplication invariance. Determinant-conditioned laws, component half-mass, principal-minor sign/zero expectation, Gaussian densities, independence from an algorithm seed, adaptive posterior invariance, Krylov reduction and both main lower bounds remain open. Dimension zero is included as a singleton group; no two-components claim is made there.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- entry_norm_bound_of_unitary
- isClosed_unitary
- isCompact_Icc
- MeasureTheory.Measure.haarMeasure_self
- MeasureTheory.Measure.isHaarMeasure_eq_of_isProbabilityMeasure
Mathematical sources
- Shared full Haar background — Background common to both experiments; only the fixed left-invariance part of the row-reflection argument.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.