Samplinglib mathematical lesson

The actual first-column law

Read this first

Mathematical statement

Move the selected Gaussian expectation to the actual Euclidean first-column distribution, preserving probability, sphere support and full orthogonal invariance.

\[H_\gamma(\ell)=\beta_{n,\kappa}\int f\,d\nu,\qquad f\in L^1(\nu).\]

Lean statement · selected_column_transport

Exact preproof signature: only source n>=3 and kappa>=4; actual column law and every analytic side condition are outputs.

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 selected_column_transport {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) :
    let s : ℝ := Real.sqrt κ
    let r : ℝ := (1 - 1 / (n : ℝ)) * ((s - 1) / (s + 1))
    let ℓ : ℝ := (4 * (n : ℝ) * s + (s - 1) ^ 2) /
      (8 * (n : ℝ) * ((n : ℝ) - 1))
    let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
    let c : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) :=
      fun O => WithLp.toLp 2 (fun i => (O : Matrix (Fin n) (Fin n) ℝ) i j0)
    let ν : Measure (EuclideanSpace ℝ (Fin n)) := (orthogonalHaar n).map c
    let f : EuclideanSpace ℝ (Fin n) → ℝ := fun y =>
      ((s + 1) * WithLp.ofLp y j0 - (s - 1)) /
        (1 + r ^ 2 - 2 * r * WithLp.ofLp y j0) ^ ((n : ℝ) / 2)
    let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
      fun O => ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
        (singleBlockPrecision κ O)⁻¹
    IsProbabilityMeasure ν ∧
      (∀ᵐ y ∂ν, ‖y‖ = 1) ∧
      (∀ Q : Matrix.orthogonalGroup (Fin n) ℝ,
        ν.map (fun y => Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n) (Q : Matrix (Fin n) (Fin n) ℝ) y) = ν) ∧
      Integrable f ν ∧
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det *
          (∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-ℓ * ‖x‖ ^ 2) ∂γ O)
        ∂orthogonalHaar n) =
        (((-1 : ℝ) ^ (n - 1) * (s - 1) ^ (n - 1)) / (s + 1) ^ n) *
          (1 - 1 / (n : ℝ)) ^ ((n : ℝ) / 2) * (∫ y, f y ∂ν)

Exact module and namespace context

The column law and integral transport are proved; canonical surface identification and Poisson evaluation remain open.

Full assumptions and notation

All objects and hypotheses

Exactly \(n\in\mathbb N,\ n\ge3\) and \(\kappa\in\mathbb R,\ \kappa\ge4\), including \(\kappa=4\). All parameter divisions are real, and \(n/2\) is a real exponent even for odd dimensions.
\(\mu\) is the existing actual normalized Haar probability on full \(O(n)\), including reflections. \(c(O)=Oe_1\) uses the Euclidean l2 norm, and \(\nu=c_*\mu\) is its literal ambient pushforward.
Probability, unit-sphere support, invariance and absolute L1 are proved conclusions. The quotient need not be continuous or have positive denominator off the support; global Borel measurability suffices for transport. No sphere law or Poisson identity is a caller premise.

Notation and interpretation

\(s,r,\ell,\beta\): The identical source-selected parameters and coefficient, with real dimension arithmetic.
\[\begin{aligned}s&=\sqrt\kappa,& r&=\left(1-\frac1n\right)\frac{s-1}{s+1},\\\ell&=\frac{4ns+(s-1)^2}{8n(n-1)},&\beta_{n,\kappa}&=\frac{(-1)^{n-1}(s-1)^{n-1}}{(s+1)^n}\left(1-\frac1n\right)^{n/2}.\end{aligned}\]
\(c,\nu,f\): Index zero in Fin n is the source first coordinate. The measure is an actual pushforward; standard surface-measure equality is still open.
\[c(O)=Oe_1,\qquad\nu=c_*\mu,\qquad f(y)=\frac{(s+1)y_1-(s-1)}{(1+r^2-2ry_1)^{n/2}}.\]
\(A_O,\gamma_O,H_\gamma\): Literal source precision and the actual canonical Gaussian expectation. The rotation in the conclusion is the ordinary Euclidean matrix action.
\[\begin{aligned}A_O&=\frac{\kappa+1}{2}I-\frac{\kappa-1}{4}(O+O^\top),\\\gamma_O&=\mathcal N(0,A_O^{-1}),\\H_\gamma(\ell)&=\mathbb E_\mu\!\left[\det(O)\int e^{-\ell\|x\|_2^2}\,d\gamma_O\right].\end{aligned}\]

Mathematical proof

Open a step to read its argument and formula.

1. Use the actual column pushforward

Each matrix entry varies continuously with O. The Euclidean identification preserves this continuity, so the column map is measurable and pushes the existing full-Haar probability to a probability.

\[\nu=c_*\mu,\qquad\nu(\mathbb R^n)=\mu(O(n))=1.\]

Corresponding Lean step

hc uses PiLp.continuous_toLp and continuous matrix entries. hprob consumes the identical OrthogonalHaar.orthogonalHaar_spec and canonical Measure.isProbabilityMeasure_map.

2. Prove genuine Euclidean sphere support

Transport the orthogonal matrix through the canonical star-algebra equivalence to Euclidean continuous linear maps. Its unitary norm-preservation acts on the first unit basis vector. The resulting column has norm one for every O, hence also almost surely under its pushforward.

\[\|c(O)\|_2=\|Oe_1\|_2=\|e_1\|_2=1,\qquad\nu\{y:\|y\|_2=1\}=1.\]

Corresponding Lean step

hnorm calls Unitary.map_mem and ContinuousLinearMap.norm_map_of_mem_unitary on Matrix.toEuclideanCLM, then Matrix.mulVec_single_one and PiLp.norm_single. hsphere applies ae_map_iff to the measurable norm level set. No l-infinity norm proxy is used.

3. Preserve the full orthogonal action

The actual matrix action commutes with taking the first column by left multiplication. Full Haar invariance, including reflections, therefore gives invariance of the literal column law. This alone is not an identification with canonical surface measure.

\[Qc(O)=c(QO),\qquad Q_*\nu=c_*((L_Q)_*\mu)=c_*\mu=\nu.\]

Corresponding Lean step

hinvariant proves the exact equivariance identity, reuses Measure.map_map twice and calls the identical compiled OrthogonalHaar.orthogonalHaar_map_mul_left. Q is an arbitrary element of full O(n), not SO(n).

4. Transport absolute integrability on the actual support

The normalized scalar Haar kernel is exactly f composed with c. Its existing absolute integrability transfers through the measurable pushforward. The ambient quotient is Borel measurable; no off-sphere positivity or continuity is asserted.

\[q(O)=f(c(O)),\qquad q\in L^1(\mu)\Longrightarrow f\in L^1(c_*\mu).\]

Corresponding Lean step

hf is global Borel measurability of the literal totalized real quotient. hp consumes the identical PoissonNormalization.selected_gaussian_normalization; hL uses integrable_map_measure with its actual L1 conclusion and the proved measurable c. Positivity and the chosen tilt are supplied by the existing producer, never extra hypotheses.

5. Keep the actual Gaussian expectation attached

Use change of variables for the same absolutely integrable function. Substitute the transported integral into the existing selected Gaussian normalization. The focused consumer performs the same substitution in the actual determinant-conditioned Gaussian bind-mixture expectation gap, retaining its factor two.

\[\int f\,d\nu=\int f(c(O))\,d\mu,\qquad H_\gamma(\ell)=\beta_{n,\kappa}\int f\,d\nu.\]

Corresponding Lean step

The final equality directly uses integral_map and hp.2. Tests.GaussianComplexityColumnTransport composes this exact declaration with MixtureExpectation.actual_mixture_expectation_gap; neither a canonical sphere law nor a Poisson value is assumed.

Lean verification

Lean proof · selected_column_transport

Canonical unitary norm preservation, literal equivariance, full-Haar invariance and measurable integral transport join the existing actual Gaussian normalization.

Download module (.lean)

theorem selected_column_transport {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) :
    let s : ℝ := Real.sqrt κ
    let r : ℝ := (1 - 1 / (n : ℝ)) * ((s - 1) / (s + 1))
    let ℓ : ℝ := (4 * (n : ℝ) * s + (s - 1) ^ 2) /
      (8 * (n : ℝ) * ((n : ℝ) - 1))
    let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
    let c : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) :=
      fun O => WithLp.toLp 2 (fun i => (O : Matrix (Fin n) (Fin n) ℝ) i j0)
    let ν : Measure (EuclideanSpace ℝ (Fin n)) := (orthogonalHaar n).map c
    let f : EuclideanSpace ℝ (Fin n) → ℝ := fun y =>
      ((s + 1) * WithLp.ofLp y j0 - (s - 1)) /
        (1 + r ^ 2 - 2 * r * WithLp.ofLp y j0) ^ ((n : ℝ) / 2)
    let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
      fun O => ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
        (singleBlockPrecision κ O)⁻¹
    IsProbabilityMeasure ν ∧
      (∀ᵐ y ∂ν, ‖y‖ = 1) ∧
      (∀ Q : Matrix.orthogonalGroup (Fin n) ℝ,
        ν.map (fun y => Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n) (Q : Matrix (Fin n) (Fin n) ℝ) y) = ν) ∧
      Integrable f ν ∧
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (O : Matrix (Fin n) (Fin n) ℝ).det *
          (∫ x : EuclideanSpace ℝ (Fin n), Real.exp (-ℓ * ‖x‖ ^ 2) ∂γ O)
        ∂orthogonalHaar n) =
        (((-1 : ℝ) ^ (n - 1) * (s - 1) ^ (n - 1)) / (s + 1) ^ n) *
          (1 - 1 / (n : ℝ)) ^ ((n : ℝ) / 2) * (∫ y, f y ∂ν) := by
  classical
  let s : ℝ := Real.sqrt κ
  let r : ℝ := (1 - 1 / (n : ℝ)) * ((s - 1) / (s + 1))
  let ℓ : ℝ := (4 * (n : ℝ) * s + (s - 1) ^ 2) /
    (8 * (n : ℝ) * ((n : ℝ) - 1))
  let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
  let c : Matrix.orthogonalGroup (Fin n) ℝ → EuclideanSpace ℝ (Fin n) :=
    fun O => WithLp.toLp 2 (fun i => (O : Matrix (Fin n) (Fin n) ℝ) i j0)
  let ν : Measure (EuclideanSpace ℝ (Fin n)) := (orthogonalHaar n).map c
  let f : EuclideanSpace ℝ (Fin n) → ℝ := fun y =>
    ((s + 1) * WithLp.ofLp y j0 - (s - 1)) /
      (1 + r ^ 2 - 2 * r * WithLp.ofLp y j0) ^ ((n : ℝ) / 2)
  let γ : Matrix.orthogonalGroup (Fin n) ℝ → Measure (EuclideanSpace ℝ (Fin n)) :=
    fun O => ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
      (singleBlockPrecision κ O)⁻¹
  change IsProbabilityMeasure ν ∧ (∀ᵐ y ∂ν, ‖y‖ = 1) ∧
    (∀ Q : Matrix.orthogonalGroup (Fin n) ℝ,
      ν.map (fun y => Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n)
        (Q : Matrix (Fin n) (Fin n) ℝ) y) = ν) ∧ Integrable f ν ∧ _
  have hc : Continuous c :=
    (PiLp.continuous_toLp 2 (fun _ : Fin n => ℝ)).comp
      (continuous_pi (fun i => continuous_subtype_val.matrix_elem i j0))
  have hf : Measurable f := by dsimp [f]; fun_prop
  let := (orthogonalHaar_spec n).1
  have hprob : IsProbabilityMeasure ν := Measure.isProbabilityMeasure_map hc.measurable.aemeasurable
  have hnorm (O : Matrix.orthogonalGroup (Fin n) ℝ) : ‖c O‖ = 1 := by
    have hu := Unitary.map_mem (Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n)) O.property
    have hh := ContinuousLinearMap.norm_map_of_mem_unitary hu (PiLp.single 2 j0 (1 : ℝ))
    have he : Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n)
        (O : Matrix (Fin n) (Fin n) ℝ) (PiLp.single 2 j0 (1 : ℝ)) = 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
    rw [he] at hh
    simpa [PiLp.norm_single] using hh
  have hsphere : ∀ᵐ y ∂ν, ‖y‖ = 1 :=
    (ae_map_iff hc.measurable.aemeasurable
      (isClosed_eq continuous_norm continuous_const).measurableSet).2
        (Filter.Eventually.of_forall hnorm)
  have hinvariant (Q : Matrix.orthogonalGroup (Fin n) ℝ) :
      ν.map (fun y => Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n)
        (Q : Matrix (Fin n) (Fin n) ℝ) y) = ν := by
    let T := Matrix.toEuclideanCLM (𝕜 := ℝ) (n := Fin n)
      (Q : Matrix (Fin n) (Fin n) ℝ)
    have heq : (fun y => T y) ∘ c = c ∘ (fun O => Q * O) := by
      funext O
      apply (WithLp.equiv 2 (Fin n → ℝ)).injective
      ext i
      simp [T, c, Matrix.mul_apply, Matrix.mulVec, dotProduct]
    change ((orthogonalHaar n).map c).map (fun y => T y) = (orthogonalHaar n).map c
    rw [Measure.map_map T.continuous.measurable hc.measurable, heq,
      ← Measure.map_map hc.measurable (measurable_const_mul Q), orthogonalHaar_map_mul_left]
  have hp := PoissonNormalization.selected_gaussian_normalization hn hκ
  change Integrable (f ∘ c) (orthogonalHaar n) ∧ _ at hp
  have hL : Integrable f ν :=
    (integrable_map_measure hf.aestronglyMeasurable hc.measurable.aemeasurable).2 hp.1
  refine ⟨hprob, hsphere, hinvariant, hL, ?_⟩
  rw [integral_map hc.measurable.aemeasurable hL.aestronglyMeasurable]
  exact hp.2

end AutoSamplingTheory.ExampleCases.GaussianComplexity.ColumnTransport

Exact module and namespace context

Scope and omitted-condition boundaries

Probability, unit-sphere support, full orthogonal invariance of the actual first-column law and transport of the existing actual signed Gaussian expectation to an absolutely integrable ambient first-column kernel. Canonical normalized surface measure identification/uniqueness and Poisson evaluations remain OPEN; no Eq24 value, positive TV ratio, query/cost, hidden-eigenbasis or main theorem.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

PiLp.continuous_toLp
Continuous.matrix_elem
Measure.isProbabilityMeasure_map
Unitary.map_mem
ContinuousLinearMap.norm_map_of_mem_unitary
Matrix.toEuclideanCLM
Matrix.mulVec_single_one
PiLp.norm_single
ae_map_iff
Measure.map_map
integrable_map_measure
integral_map

Mathematical sources

Zhou–Suzuki, B.7: actual first-column transport before Lemma A.1 — Probability, unit-sphere support, full orthogonal invariance of the actual first-column law and transport of the existing actual signed Gaussian expectation to an absolutely integrable ambient first-column kernel. Canonical normalized surface measure identification/uniqueness and Poisson evaluations remain OPEN; no Eq24 value, positive TV ratio, query/cost, hidden-eigenbasis or main theorem.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.