From Haar columns to surface measure
Mathematical statement
Every actual Haar column has the canonical Euclidean surface law.
Lean statement · column_map_eq_normalized_surface
Exact frozen signature; every normalization/analytic dependency is supplied 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 column_map_eq_normalized_surface {n : ℕ} (j : Fin n) :
let τ : Measure (Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1) :=
(volume : Measure (EuclideanSpace ℝ (Fin n))).toSphere
let σ : Measure (EuclideanSpace ℝ (Fin n)) :=
(τ Set.univ)⁻¹ • τ.map (fun y => y.val)
(orthogonalHaar n).map
(fun O : Matrix.orthogonalGroup (Fin n) ℝ => WithLp.toLp 2 (fun i => (O : Matrix (Fin n) (Fin n) ℝ) i j)) = σActual surface-law identification is established; Poisson values remain open.
Full assumptions and notation
All objects and hypotheses
- \(n\in\mathbb N\) and \(j\in\{1,\ldots,n\}\); a chosen coordinate forces \(n\ge1\). The source uses the first coordinate at \(n\ge3\); this canonical background includes every coordinate and positive finite dimension.
- \(E=\mathbb R^n\) has its genuine Euclidean norm and volume. \(\mu\) is the actual normalized Haar probability on full \(O(n)\), including reflections.
- The surface law is literally derived from Euclidean volume: \(\tau=\mathrm{volume}.\mathrm{toSphere}\), then \(\sigma=\tau(S)^{-1}\iota_*\tau\). Finite nonzero mass, normalization, invariance and equality are proved internally. No uniqueness, measurable-selection or uniform-law premise is supplied.
Notation and interpretation
- \(S,\tau,\sigma\)
The actual cone-derived surface measure on the sphere subtype, normalized and included in the ambient Euclidean space. The inverse scalar is an extended nonnegative real.
\[S=\{u:\|u\|_2=1\},\quad\tau(B)=n\,\mathrm{vol}\{ru:0<r<1,\ u\in B\},\quad\sigma=\frac{\iota_*\tau}{\tau(S)}.\]- \(c_j,\nu_j\)
Index j in Fin n is zero-based in Lean; e_j is the corresponding actual Euclidean basis vector.
\[c_j(O)=Oe_j,\qquad\nu_j=(c_j)_*\mu.\]
Mathematical proof
1. Normalize the actual surface measure
The cone construction has finite nonzero total mass in positive dimension. Normalize that measure on the sphere, then push it into Euclidean space. The result is a probability supported on the unit sphere.
Corresponding Lean step
Measure.toSphere_ne_zero and the canonical IsFiniteMeasure instance justify inverse scaling via isProbabilityMeasureSMul. hσ is the literal map_smul equality; hσprob and hσsphere use probability pushforward and ae_map_iff.
2. Use volume preservation on cones
Every linear isometry preserves Euclidean volume and commutes with positive radial scaling. Its action therefore preserves the cone-derived surface measure and its normalized ambient pushforward, including orientation-reversing maps.
Corresponding Lean step
hσiso constructs the actual sphere subtype map q. hτ applies Measure.toSphere_apply' and proves exact cone preimage equality hc; LinearIsometryEquiv.measurePreserving.measure_preimage_emb supplies actual volume preservation even for arbitrary cone sets. Measure.map_map/map_smul transport the result. hσinv uses Unitary.map_mem and Unitary.linearIsometryEquiv on Matrix.toEuclideanCLM.
3. Identify every unit-vector orbit law
For any unit vector y, a reflection sends e_j to y. Its matrix Q belongs to full O(n). Right multiplication by Q preserves the actual normalized Haar law, so O y and the j-th Haar column have the same law. No measurable choice of Q as a function of y is required.
Corresponding Lean step
horbit constructs one fixed reflection for each point using Submodule.reflection_sub, its orthonormal-basis matrix and LinearMap.toMatrix_mulVec_repr. hr derives right invariance from the identical orthogonalHaar_spec uniqueness and Measure.isHaarMeasure_map_mul_right. No clone or promotion of KernelAxis private helpers is used.
4. Compare Borel events by Haar averaging
For a Borel event B, integrate its indicator after the orthogonal action. Integrating in the sphere variable first gives sigma(B) by invariance; integrating in the Haar variable first gives nu_j(B) on the actual sphere support. The joint action is continuous, so Tonelli permits exchanging these nonnegative integrals.
Corresponding Lean step
hact proves joint Euclidean continuity from finite matrix-coordinate sums and PiLp topology. hg is the Borel indicator into ENNReal. hleft uses actual sigma invariance; hright uses horbit on hσsphere. lintegral_lintegral_swap applies with both actual probability measures; no signed Fubini or unstated L1 premise is needed.
5. Conclude equality of actual measures
The two probabilities agree on every Borel event, hence are the same ambient measure. The selected Gaussian consumer can now use the canonical surface law; conditional residual sphere laws and Poisson values remain separate.
Corresponding Lean step
Measure.ext closes the actual measure equality after Tonelli and both total masses one. The selected SurfaceLaw adapter calls this exact shared declaration, and the focused test compares two distinct actual column marginals through the same canonical node.
Lean verification
Lean proof · column_map_eq_normalized_surface
Actual measure identification by cone invariance and Tonelli, or its exact Gaussian consumer adapter.
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 column_map_eq_normalized_surface {n : ℕ} (j : Fin n) :
let τ : Measure (Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1) :=
(volume : Measure (EuclideanSpace ℝ (Fin n))).toSphere
let σ : Measure (EuclideanSpace ℝ (Fin n)) :=
(τ Set.univ)⁻¹ • τ.map (fun y => y.val)
(orthogonalHaar n).map
(fun O : Matrix.orthogonalGroup (Fin n) ℝ => WithLp.toLp 2 (fun i => (O : Matrix (Fin n) (Fin n) ℝ) i j)) = σ := by
classical
let : NeZero n := ⟨by have := j.isLt; omega⟩
let E := EuclideanSpace ℝ (Fin n)
let G := Matrix.orthogonalGroup (Fin n) ℝ
let S := Metric.sphere (0 : E) 1
let τ : Measure S := (volume : Measure E).toSphere
let σ : Measure E := (τ univ)⁻¹ • τ.map Subtype.val
let c : G → E := fun O => WithLp.toLp 2 (fun i => (O : Matrix (Fin n) (Fin n) ℝ) i j)
let T : G → E →L[ℝ] E := fun O =>
Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n) (O : Matrix (Fin n) (Fin n) ℝ)
let μ := orthogonalHaar n
let ν : Measure E := μ.map c
have hc : Continuous c :=
(PiLp.continuous_toLp 2 (fun _ : Fin n => ℝ)).comp
(continuous_pi (fun i => continuous_subtype_val.matrix_elem i j))
let := (orthogonalHaar_spec n).1
let : NeZero τ := ⟨Measure.toSphere_ne_zero volume⟩
let ρ : Measure S := (τ univ)⁻¹ • τ
have hρ : IsProbabilityMeasure ρ := inferInstance
have hσ : σ = ρ.map Subtype.val := by rw [Measure.map_smul]
let := hρ
have hσprob : IsProbabilityMeasure σ := by
rw [hσ]
exact Measure.isProbabilityMeasure_map measurable_subtype_coe.aemeasurable
let := hσprob
have hσsphere : ∀ᵐ y ∂σ, ‖y‖ = 1 := by
rw [hσ]
apply (ae_map_iff measurable_subtype_coe.aemeasurable
(isClosed_eq continuous_norm continuous_const).measurableSet).2
exact Filter.Eventually.of_forall (fun y => mem_sphere_zero_iff_norm.mp y.property)
have hσiso (Q : E ≃ₗᵢ[ℝ] E) : σ.map Q = σ := by
classical
let E := EuclideanSpace ℝ (Fin n)
let S := Metric.sphere (0 : E) 1
let τ : Measure S := (volume : Measure E).toSphere
let q : S → S := fun y => ⟨Q y, by
change Q (y : E) ∈ Metric.sphere (0 : E) 1
rw [mem_sphere_zero_iff_norm, Q.norm_map]
exact mem_sphere_zero_iff_norm.mp y.property⟩
have hq : Measurable q := (Q.continuous.comp continuous_subtype_val).subtype_mk _ |>.measurable
have hτ : τ.map q = τ := by
ext t ht
rw [Measure.map_apply hq ht]
change (volume : Measure E).toSphere (q ⁻¹' t) = (volume : Measure E).toSphere t
rw [Measure.toSphere_apply' _ (ht.preimage hq), Measure.toSphere_apply' _ ht]
congr 1
have hc : Ioo (0 : ℝ) 1 • (Subtype.val '' (q ⁻¹' t)) =
Q ⁻¹' (Ioo (0 : ℝ) 1 • (Subtype.val '' t)) := by
ext x
constructor
· rintro ⟨a, ha, z, ⟨y, hy, rfl⟩, rfl⟩
exact ⟨a, ha, Q y, ⟨q y, hy, rfl⟩, (Q.map_smul a y).symm⟩
· rintro ⟨a, ha, z, ⟨y, hy, rfl⟩, hxy⟩
let w : S := ⟨Q.symm y, by
change Q.symm (y : E) ∈ Metric.sphere (0 : E) 1
rw [mem_sphere_zero_iff_norm, Q.symm.norm_map]
exact mem_sphere_zero_iff_norm.mp y.property⟩
have hw : q w = y := by apply Subtype.ext; exact Q.apply_symm_apply y
refine ⟨a, ha, Q.symm y, ⟨w, ?_, rfl⟩, ?_⟩
· change q w ∈ t
rw [hw]
exact hy
· apply Q.injective
simpa using hxy
rw [hc]
exact Q.measurePreserving.measure_preimage_emb Q.toHomeomorph.measurableEmbedding _
change ((τ univ)⁻¹ • τ.map Subtype.val).map Q = (τ univ)⁻¹ • τ.map Subtype.val
rw [Measure.map_smul, Measure.map_map Q.continuous.measurable measurable_subtype_coe]
have he : (Q : E → E) ∘ Subtype.val = Subtype.val ∘ q := rfl
rw [he, ← Measure.map_map measurable_subtype_coe hq, hτ]
have hσinv (O : G) : σ.map (T O) = σ := by
let u : unitary (E →L[ℝ] E) :=
⟨T O, Unitary.map_mem (Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n)) O.property⟩
exact hσiso (Unitary.linearIsometryEquiv u)
have horbit : ∀ y : E, ‖y‖ = 1 → μ.map (fun O : G => T O y) = ν := by
classical
let E := EuclideanSpace ℝ (Fin n)
let G := Matrix.orthogonalGroup (Fin n) ℝ
let j0 : Fin n := j
let c : G → E := fun O => WithLp.toLp 2 (fun i => (O : Matrix (Fin n) (Fin n) ℝ) i j0)
let T : G → E →L[ℝ] E := fun O =>
Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n) (O : Matrix (Fin n) (Fin n) ℝ)
let e0 : E := PiLp.single 2 j0 (1 : ℝ)
have hc : Continuous c :=
(PiLp.continuous_toLp 2 (fun _ : Fin n => ℝ)).comp
(continuous_pi (fun i => continuous_subtype_val.matrix_elem i j0))
have he (O : G) : T O e0 = c O := by
apply (WithLp.equiv 2 (Fin n → ℝ)).injective
change (O : Matrix (Fin n) (Fin n) ℝ) *ᵥ Pi.single j0 1 = fun i =>
(O : Matrix (Fin n) (Fin n) ℝ) i j0
rw [Matrix.mulVec_single_one]
rfl
have hr (Q : G) : (orthogonalHaar n).map (fun O => O * Q) = orthogonalHaar n := by
let := (orthogonalHaar_spec n).1
let := (orthogonalHaar_spec n).2.1
exact (orthogonalHaar_spec n).2.2 _
(Measure.isProbabilityMeasure_map (measurable_mul_const Q).aemeasurable)
(Measure.isHaarMeasure_map_mul_right (orthogonalHaar n) Q)
change ∀ y : E, ‖y‖ = 1 → (orthogonalHaar n).map (fun O : G => T O y) = (orthogonalHaar n).map c
intro y hy
let w : E ≃ₗᵢ[ℝ] E := (ℝ ∙ (e0 - y))ᗮ.reflection
let b := EuclideanSpace.basisFun (Fin n) ℝ
let Q : G := ⟨w.toMatrix b.toBasis b.toBasis, w.toMatrix_mem_unitaryGroup b b⟩
have hw : w e0 = y := Submodule.reflection_sub (by
change ‖(PiLp.single 2 j0 (1 : ℝ) : E)‖ = ‖y‖
rw [PiLp.norm_single]
simpa using hy.symm)
have hQ : T Q e0 = y := by
apply (WithLp.equiv 2 (Fin n → ℝ)).injective
have hm := LinearMap.toMatrix_mulVec_repr b.toBasis b.toBasis w.toLinearEquiv.toLinearMap e0
change (Q : Matrix (Fin n) (Fin n) ℝ) *ᵥ WithLp.ofLp e0 = WithLp.ofLp (w e0) at hm
exact hm.trans (congrArg WithLp.ofLp hw)
have hm (O : G) : T O y = c (O * Q) := by
rw [← hQ, ← he]
change (Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n) (O : Matrix (Fin n) (Fin n) ℝ))
((Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n) (Q : Matrix (Fin n) (Fin n) ℝ)) e0) =
(Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n)
((O : Matrix (Fin n) (Fin n) ℝ) * (Q : Matrix (Fin n) (Fin n) ℝ))) e0
rw [map_mul]
rfl
change (orthogonalHaar n).map (fun O => T O y) = (orthogonalHaar n).map c
calc
_ = (orthogonalHaar n).map (c ∘ fun O => O * Q) := by congr 1; funext O; exact hm O
_ = ((orthogonalHaar n).map (fun O => O * Q)).map c :=
(Measure.map_map hc.measurable (measurable_mul_const Q)).symm
_ = _ := by rw [hr]
have hact : Continuous (fun p : G × E => T p.1 p.2) := by
change Continuous (fun p : G × E => WithLp.toLp 2
(fun i => ∑ k : Fin n, (p.1 : Matrix (Fin n) (Fin n) ℝ) i k * WithLp.ofLp p.2 k))
apply (PiLp.continuous_toLp 2 (fun _ : Fin n => ℝ)).comp
apply continuous_pi
intro i
apply continuous_finsetSum
intro k _
exact ((continuous_subtype_val.comp continuous_fst).matrix_elem i k).mul
((continuous_apply k).comp
((PiLp.continuous_ofLp 2 (fun _ : Fin n => ℝ)).comp continuous_snd))
change ν = σ
ext t ht
let g : E → ℝ≥0∞ := t.indicator (fun _ => 1)
have hg : Measurable g := measurable_const.indicator ht
have hgint (η : Measure E) : (∫⁻ x, g x ∂η) = η t := by
simp [g, lintegral_indicator ht]
have hleft (O : G) : (∫⁻ y, g (T O y) ∂σ) = σ t := by
rw [← lintegral_map hg (T O).continuous.measurable, hσinv, hgint]
have hright : ∀ᵐ y ∂σ, (∫⁻ O : G, g (T O y) ∂μ) = ν t := by
filter_upwards [hσsphere] with y hy
have hymeas : Measurable (fun O : G => T O y) :=
(hact.comp (continuous_id.prodMk (continuous_const (y := y)))).measurable
rw [← lintegral_map hg hymeas, horbit y hy, hgint]
calc
ν t = ∫⁻ y : E, ∫⁻ O : G, g (T O y) ∂μ ∂σ := by
rw [lintegral_congr_ae hright]
simp
_ = ∫⁻ O : G, ∫⁻ y : E, g (T O y) ∂σ ∂μ :=
(lintegral_lintegral_swap (μ := μ) (ν := σ)
(f := fun O : G => fun y : E => g (T O y))
(hg.comp hact.measurable).aemeasurable).symm
_ = σ t := by
simp_rw [hleft]
rw [lintegral_const, (orthogonalHaar_spec n).1.measure_univ, mul_one]
end AutoSamplingTheory.TechnicalLemmas.Probability.SphereHaarSource correspondence and review
Source assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The source invokes Oe1 uniform on the sphere for n>=3 and uses normalized surface measure in A1. | The actual cone-derived normalized measure is identified with every full-Haar column for each j:Fin n, hence n>=1. | generalization | A canonical source-implicit background expansion; the constructive proof covers all positive finite dimensions and coordinates. This does not generalize the paper lower bound or prove a conditional sphere law. |
| Normalized surface and Haar uniformity are implicit standard background. | Proves actual toSphere finite nonzero mass, probability/support, cone invariance, reflection transitivity, actual Haar right invariance and Tonelli measure identification internally. | source-implicit | Every missing bridge is a dependency, never a public hypothesis; volume-derived sigma is not defined as an invariant law. |
Actual unconditional full-Haar column equals normalized Euclidean volume-derived surface probability. No conditional residual/subspace law, seed independence, Poisson value, evaluated Eq24 or main lower bound.
Encoder–denoiser: accepted · equivalent-after-elaboration
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
- Actual unconditional full-Haar column equals normalized Euclidean volume-derived surface probability. No conditional residual/subspace law, seed independence, Poisson value, evaluated Eq24 or main lower bound.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- Measure.toSphere_ne_zero
- Measure.toSphere_apply'
- Measure.isProbabilityMeasure_map
- ae_map_iff
- LinearIsometryEquiv.measurePreserving
- MeasurePreserving.measure_preimage_emb
- Measure.map_map
- Measure.map_smul
- Submodule.reflection_sub
- LinearIsometryEquiv.toMatrix_mem_unitaryGroup
- Measure.isHaarMeasure_map_mul_right
- lintegral_map
- lintegral_lintegral_swap
Mathematical sources
- Zhou–Suzuki, B.7/A.1: Haar columns and normalized surface law — Actual unconditional full-Haar column equals normalized Euclidean volume-derived surface probability. No conditional residual/subspace law, seed independence, Poisson value, evaluated Eq24 or main lower bound.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.