The selected Gaussian surface integral

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling. ASTIS expands the standard surface-law identification used by the source. Shared background is explicitly generalized to every existing coordinate and positive finite dimension.

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 selected Gaussian surface integral

Read this first

Mathematical statement

Move the selected actual Gaussian expectation onto canonical surface probability.

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

Lean statement · selected_surface_transport

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 selected_surface_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 τ : 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)
    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 σ ∧ 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

Actual surface-law identification is established; Poisson values 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.
\(\sigma\) is the literal normalized Euclidean volume-derived surface measure. Its equality with the actual Haar first-column law, its probability normalization, and \(f\in L^1(\sigma)\) are conclusions, with no additional public premises. The ambient quotient retains standard totalized real division/rpow; no off-sphere positivity or continuity is asserted.

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}\]
\(\tau,\sigma,\nu,f\): Use the canonical shared surface construction and the identical selected ambient kernel; the actual first-column law is now identified with this sigma.
\[\tau=\mathrm{vol}.\mathrm{toSphere},\quad\sigma=\tau(S)^{-1}\iota_*\tau,\quad\nu=(O\mapsto Oe_1)_*\mu,\quad 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}\]
\(t,\nu_\pm,\nu_\pm\mathrm{bind}\gamma\): The priors are the actual determinant-conditioned full-Haar probabilities on the orthogonal group, normalized by the factor two. Binding the actual Gaussian kernel gamma to either prior forms its Gaussian mixture. The test function is the literal selected radial tilt.
\[t(x)=e^{-\ell\|x\|_2^2},\qquad\nu_\pm=2\,\mu\!\restriction\{O:\det O=\pm1\},\qquad(\nu_\pm\mathrm{bind}\gamma)(B)=\int\gamma_O(B)\,d\nu_\pm(O).\]

Mathematical proof

Open a step to read its argument and formula.

1. Use the one canonical surface-law identity

Apply the shared full-Haar column identity to the first coordinate. All surface normalization, invariance and measure identification are proved inside that producer.

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

Corresponding Lean step

he calls the identical SphereHaar.column_map_eq_normalized_surface j0; no invariant-law or Poisson premise is accepted.

2. Transport probability and absolute integrability

The existing selected column producer gives an actual probability and absolute integrability of the unchanged kernel. Equality of the measures transfers both facts to the canonical surface law.

\[\nu(E)=1,\quad f\in L^1(\nu),\quad\nu=\sigma\quad\Longrightarrow\quad\sigma(E)=1,\ f\in L^1(\sigma).\]

Corresponding Lean step

hp is the identical ColumnTransport.selected_column_transport hn hκ. The second and third conjuncts rewrite by he and consume hp.1 and hp.2.2.2.1, preserving genuine absolute L1.

3. Keep the actual Gaussian expectation attached

Rewrite the measure in the existing selected Gaussian expectation. The actual determinant-conditioned Gaussian bind-mixture consumer then has the same surface integral with its required factor two. No numerical Poisson identity is used.

\[H_\gamma(\ell)=\beta_{n,\kappa}\int f\,d\sigma,\qquad\mathbb E_{\nu_+\mathrm{bind}\gamma}t-\mathbb E_{\nu_-\mathrm{bind}\gamma}t=2\beta_{n,\kappa}\int f\,d\sigma.\]

Corresponding Lean step

The final conjunct rewrites by he and uses hp.2.2.2.2. Tests.GaussianComplexitySurfaceLaw combines this actual integral with MixtureExpectation.actual_mixture_expectation_gap and the positive selected tilt, preserving the literal Gaussian and real odd-dimensional half powers.

Lean verification

Lean proof · selected_surface_transport

Actual measure identification by cone invariance and Tonelli, or its exact Gaussian consumer adapter.

Download module (.lean)

theorem selected_surface_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 τ : 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)
    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 σ ∧ 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 τ : 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)
  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 σ ∧ Integrable f σ ∧ _
  have he : ν = σ :=
    AutoSamplingTheory.TechnicalLemmas.Probability.SphereHaar.column_map_eq_normalized_surface j0
  have hp := ColumnTransport.selected_column_transport hn hκ
  refine ⟨he, ?_, ?_, ?_⟩
  · rw [← he]
    exact hp.1
  · rw [← he]
    exact hp.2.2.2.1
  · change (∫ 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 ∂σ)
    rw [← he]
    exact hp.2.2.2.2

end AutoSamplingTheory.ExampleCases.GaussianComplexity.SurfaceLaw

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, selected Eq22-23 parameters.	Exactly n>=3,kappa>=4; actual canonical surface equality/probability and L1 are conclusions.	same	No invariance, uniqueness, surface law, measurability, L1 or Poisson identity supplied as a hypothesis.
The Oe1 uniform sentence identifies the A1 normalized surface law before evaluating its Poisson integrals.	Makes that actual identity explicit, transporting the unchanged unevaluated selected Gaussian integral to it.	source-implicit	This closes the surface identification component only; both A1 numerical values and Eq24 remain separate.

Identify actual full-Haar first-column law with actual normalized volume-derived sphere probability, and transport existing absolute selected-kernel L1 and actual signed Gaussian integral to that same canonical surface law. Neither Poisson value, evaluated Eq24, actual positive TV ratio, amplification/oracle/query/cost, hidden-eigenbasis or main theorem is asserted. Surface normalization/invariance, any invariant-law uniqueness/transitivity and all measurability are proof dependencies, never new public premises.

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

Identify actual full-Haar first-column law with actual normalized volume-derived sphere probability, and transport existing absolute selected-kernel L1 and actual signed Gaussian integral to that same canonical surface law. Neither Poisson value, evaluated Eq24, actual positive TV ratio, amplification/oracle/query/cost, hidden-eigenbasis or main theorem is asserted. Surface normalization/invariance, any invariant-law uniqueness/transitivity and all measurability are proof dependencies, never new public premises.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Zhou–Suzuki, B.7/A.1: selected Gaussian surface integral — Identify actual full-Haar first-column law with actual normalized volume-derived sphere probability, and transport existing absolute selected-kernel L1 and actual signed Gaussian integral to that same canonical surface law. Neither Poisson value, evaluated Eq24, actual positive TV ratio, amplification/oracle/query/cost, hidden-eigenbasis or main theorem is asserted. Surface normalization/invariance, any invariant-law uniqueness/transitivity and all measurability are proof dependencies, never new public premises.

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 selected Gaussian surface integral

The selected Gaussian surface integral

Read the formalized proofs

The selected Gaussian surface integral

Mathematical statement

All objects and hypotheses

Notation and interpretation

Mathematical proof

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?