Samplinglib mathematical lesson

From Haar columns to surface measure

Read this first

Mathematical statement

Every actual Haar column has the canonical Euclidean surface law.

\[(O\mapsto Oe_j)_*\mu=\sigma.\]

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.

Download module (.lean)

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)) = σ

Exact module and namespace context

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

Open a step to read its argument and formula.

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.

\[0<\tau(S)<\infty,\qquad\sigma(E)=1,\qquad\sigma(\{y:\|y\|_2=1\})=1.\]

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.

\[Q^{-1}\{ru:u\in B,\ 0<r<1\}=\{rv:Qv\in B,\ 0<r<1\},\qquad Q_*\sigma=\sigma.\]

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.

\[Qe_j=y,\qquad OQ\stackrel{d}=O,\qquad (O\mapsto Oy)_*\mu=\nu_j\quad(\|y\|_2=1).\]

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.

\[\int\!\int 1_B(Oy)\,d\sigma(y)\,d\mu(O)=\sigma(B),\qquad\int\!\int 1_B(Oy)\,d\mu(O)\,d\sigma(y)=\nu_j(B).\]

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.

\[\forall B\in\mathcal B(E),\quad\nu_j(B)=\sigma(B)\qquad\Longrightarrow\qquad(c_j)_*\mu=\sigma.\]

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.

Download module (.lean)

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

Exact module and namespace context

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

AutoSamplingTheory.TechnicalLemmas.Probability.OrthogonalHaar.orthogonalHaar_spec

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.