Samplinglib mathematical lesson

Construct the full orthogonal Haar draw

AutoSamplingTheory.TechnicalLemmas.Probability.OrthogonalHaar.orthogonalHaar · def · Teaching coverage

Read this first

Mathematical statement

For every natural finite dimension n, define the full orthogonal Haar law by the actual Haar constructor normalized on the entire compact group O(n).

\[\mu_n=\operatorname{Haar}_{K_0}(O(n)),\qquad K_0=O(n),\quad\mu_n(K_0)=1\]

Lean statement · 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.

Download module (.lean)

noncomputable def orthogonalHaar (n : ℕ) :
    Measure (Matrix.orthogonalGroup (Fin n) ℝ)

Exact module and namespace context

Proof roadmap

1Define only after well-definedness
The preceding existence/uniqueness theorem was compiled and independently proof-reviewed before this production definition was written. Use the actual normalized Haar constructor on the same carrier, topology and Borel sigma-algebra. The separately named characterization follows.

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.

Construction and meaning

1. Define only after well-definedness

The preceding existence/uniqueness theorem was compiled and independently proof-reviewed before this production definition was written. Use the actual normalized Haar constructor on the same carrier, topology and Borel sigma-algebra. The separately named characterization follows.

\[K_0=O(n),\qquad\mu_n=\operatorname{Haar}_{K_0}\]

Corresponding Lean step

The body is Measure.haarMeasure (top : PositiveCompacts O(n)). It does not call the preceding existence theorem; that theorem gates introduction of the object, and its proof is genuinely consumed by the later uniqueness characterization. The pre-definition snapshot and independent audit are retained in haar-well-definedness-input.json and haar-well-definedness-review.json.

Lean verification

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

Lean construction · orthogonalHaar

The adjacent exact Lean constructs the law and discharges its topology, normalization and invariance dependencies internally.

Download module (.lean)

noncomputable def orthogonalHaar (n : ℕ) :
    Measure (Matrix.orthogonalGroup (Fin n) ℝ) :=
  Measure.haarMeasure (⊤ : PositiveCompacts (Matrix.orthogonalGroup (Fin n) ℝ))

Exact module and namespace context

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)

MeasureTheory.Measure.haarMeasure

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.