The actual first-column law

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling. A bounded source-implicit component of the statement that the first orthogonal column is uniformly spherical, together with transport of the unevaluated selected Gaussian normalization. Identification with canonical normalized surface measure and both Poisson values remain separate.

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

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

Source correspondence and review

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
B7 n>=3, kappa>=4, actual full orthogonal Haar and source Gaussian.	Exactly those public assumptions and objects; actual first-column probability, l2 support, full orthogonal invariance and L1 are conclusions.	same	No measurability, support, invariance, L1 or sphere/Poisson identity added as a premise.
The source states that Oe1 is uniform on the sphere before applying A1, and leaves the probability/support/invariance and pushforward bookkeeping implicit.	Proves the actual column-law probability/support/invariance and selected-kernel integral transport only; canonical normalized surface identification/uniqueness and Poisson values remain explicit residuals.	source-implicit	This is a bounded dependency component, not equivalence of the entire uniform-sphere assertion or an evaluation of Eq24.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

objects: Definition expansion makes the existing Haar and Gaussian constructors explicit; it does not replace their laws. — orthogonalHaar is literally haarMeasure(top), singleBlockPrecision is literal S3.E4, multivariateGaussian is the existing CFC.sqrt pushforward, and GaussianLawDensity proves its source density under internally derived SPD.
domains: Fin n coordinate zero and WithLp.toLp 2 elaborate the source first coordinate and Euclidean l2 space; real half powers retain odd dimensions. — ColumnTransport hnorm applies canonical unitary Euclidean norm preservation to PiLp.single 2 j0 1; Tests includes n=3,kappa=4 and the universal consumer.
scopes: The ambient totalized real quotient is an implementation elaboration outside the source probability support. This does not change an integral or require an ambient positivity assumption. — hc/hf are internal; hL transfers L1 under nu. PoissonNormalization proves 0<r<1 and the positive denominator on actual orthogonal columns. On sphere support, D>=(1-r)^2>0.
conclusion: Probability, support, invariance and integral transport expand the declared bounded source-implicit component; they do not claim completion of the source uniform-sphere identification or A1/E24 evaluation. — Current publication statement, lesson boundary, source-only graph and source-lean-map keep canonical surface equality/uniqueness and both Poisson values open; backward closure has no residual nodes.

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

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.

The actual first-column law

Actual Gaussian-to-column transport

Read the formalized proofs

The actual first-column law

Mathematical statement

All objects and hypotheses

Notation and interpretation

Mathematical proof

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?