OrthogonalHaar: 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.

The full orthogonal group has a unique Haar probability
Construct the full orthogonal Haar draw
Characterize the constructed probability law
A fixed rotation or reflection preserves the draw

Samplinglib mathematical lesson

The full orthogonal group has a unique Haar probability

AutoSamplingTheory.TechnicalLemmas.Probability.OrthogonalHaar.existsUnique_orthogonalHaar · theorem · Teaching coverage

Read this first

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.

\[\exists!\,\mu\in\mathcal M(O(n)):\quad \mu(O(n))=1\ \land\ \mu\text{ is Haar}\]

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.

Download module (.lean)

theorem existsUnique_orthogonalHaar (n : ℕ) :
    ∃! μ : Measure (Matrix.orthogonalGroup (Fin n) ℝ),
      IsProbabilityMeasure μ ∧ μ.IsHaarMeasure

Exact module and namespace context

Proof 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.

\[O(n)\subseteq[-1,1]^{n\times n},\qquad O(n)\text{ closed}\ \Longrightarrow\ O(n)\text{ compact}\]

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.

\[\mu(K_0)=1,\qquad \nu,\mu\text{ Haar probabilities}\ \Longrightarrow\nu=\mu\]

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.

Download module (.lean)

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 ν μ

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)

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.

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.

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.

Samplinglib mathematical lesson

Characterize the constructed probability law

AutoSamplingTheory.TechnicalLemmas.Probability.OrthogonalHaar.orthogonalHaar_spec · theorem · Teaching coverage

Read this first

Mathematical statement

For every natural finite dimension n, the constructed full orthogonal Haar law is a probability Haar measure. Every probability Haar measure on that same Borel group equals it.

\[\mu_n(O(n))=1,\quad\mu_n\text{ is Haar},\quad\forall\nu:\ (\nu(O(n))=1\land\nu\text{ is Haar})\Rightarrow\nu=\mu_n\]

Lean statement · orthogonalHaar_spec

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.

Download module (.lean)

theorem orthogonalHaar_spec (n : ℕ) :
    IsProbabilityMeasure (orthogonalHaar n) ∧ (orthogonalHaar n).IsHaarMeasure ∧
      ∀ μ : Measure (Matrix.orthogonalGroup (Fin n) ℝ),
        IsProbabilityMeasure μ → μ.IsHaarMeasure → μ = orthogonalHaar n

Exact module and namespace context

Proof roadmap

1Prove normalization and the Haar property for this constructor
Unfold the definition. The constructor normalization set is the entire group, so its normalization theorem gives total mass one; the actual constructor instance supplies the Haar property.
2Consume the existence/uniqueness theorem
The constructed measure and any competing Haar probability both satisfy the predicate proved uniquely inhabited above. Uniqueness therefore identifies them.

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. Prove normalization and the Haar property for this constructor

Unfold the definition. The constructor normalization set is the entire group, so its normalization theorem gives total mass one; the actual constructor instance supplies the Haar property.

\[\mu_n(O(n))=1,\qquad\mu_n\text{ is Haar}\]

Corresponding Lean step

Use haarMeasure_self and the actual IsHaarMeasure instance, not a probability premise supplied by the caller.

2. Consume the existence/uniqueness theorem

The constructed measure and any competing Haar probability both satisfy the predicate proved uniquely inhabited above. Uniqueness therefore identifies them.

\[\exists!\mu:\Phi(\mu),\quad\Phi(\nu),\Phi(\mu_n)\ \Longrightarrow\nu=\mu_n\]

Corresponding Lean step

The proof genuinely calls existsUnique_orthogonalHaar n and its unique field.

Lean verification

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

Lean proof · orthogonalHaar_spec

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

Download module (.lean)

theorem orthogonalHaar_spec (n : ℕ) :
    IsProbabilityMeasure (orthogonalHaar n) ∧ (orthogonalHaar n).IsHaarMeasure ∧
      ∀ μ : Measure (Matrix.orthogonalGroup (Fin n) ℝ),
        IsProbabilityMeasure μ → μ.IsHaarMeasure → μ = orthogonalHaar n := by
  have hprob : IsProbabilityMeasure (orthogonalHaar n) := ⟨by
    simpa only [orthogonalHaar, PositiveCompacts.coe_top] using
      (Measure.haarMeasure_self (K₀ :=
        (⊤ : PositiveCompacts (Matrix.orthogonalGroup (Fin n) ℝ))))⟩
  have hhaar : (orthogonalHaar n).IsHaarMeasure := by
    dsimp only [orthogonalHaar]
    infer_instance
  refine ⟨hprob, hhaar, ?_⟩
  intro μ hp hh
  exact (existsUnique_orthogonalHaar n).unique ⟨hp, hh⟩ ⟨hprob, hhaar⟩

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_self

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.

Samplinglib mathematical lesson

A fixed rotation or reflection preserves the draw

AutoSamplingTheory.TechnicalLemmas.Probability.OrthogonalHaar.orthogonalHaar_map_mul_left · theorem · Teaching coverage

Read this first

Mathematical statement

For every natural finite dimension n and every fixed Q in the full real orthogonal group O(n), the pushforward of the constructed Haar probability by O → Q O equals that same probability. This includes a fixed single-row reflection.

\[(O\mapsto QO)_{\#}\mu_n=\mu_n\qquad(Q\in O(n))\]

Lean statement · orthogonalHaar_map_mul_left

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.

Download module (.lean)

theorem orthogonalHaar_map_mul_left (n : ℕ)
    (Q : Matrix.orthogonalGroup (Fin n) ℝ) :
    (orthogonalHaar n).map (fun O => Q * O) = orthogonalHaar n

Exact module and namespace context

Proof roadmap

1Apply the Haar invariance of this actual law
Install the Haar property from the characterization of the constructed law. A fixed Q acts by continuous left multiplication in the orthogonal group; the Haar pushforward theorem gives the same measure. Q need not have determinant +1.

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.
Q is any fixed real orthogonal n by n matrix.

Mathematical proof

1. Apply the Haar invariance of this actual law

Install the Haar property from the characterization of the constructed law. A fixed Q acts by continuous left multiplication in the orthogonal group; the Haar pushforward theorem gives the same measure. Q need not have determinant +1.

\[\mu_n\text{ left invariant}\ \Longrightarrow\ (O\mapsto QO)_{\#}\mu_n=\mu_n\]

Corresponding Lean step

orthogonalHaar_spec supplies the actual Haar instance; map_mul_left_eq_self supplies the pushforward equality. The focused test constructs a diagonal single-row reflection with determinant -1 and checks it is measurable and measure preserving.

Lean verification

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

Lean proof · orthogonalHaar_map_mul_left

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

Download module (.lean)

theorem orthogonalHaar_map_mul_left (n : ℕ)
    (Q : Matrix.orthogonalGroup (Fin n) ℝ) :
    (orthogonalHaar n).map (fun O => Q * O) = orthogonalHaar n := by
  let := (orthogonalHaar_spec n).2.1
  exact map_mul_left_eq_self (orthogonalHaar n) Q

end AutoSamplingTheory.TechnicalLemmas.Probability.OrthogonalHaar

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.map_mul_left_eq_self

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.