Samplinglib mathematical lesson

Polynomial Gaussian ridges have one dimension-independent L2 norm

AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge.standard_gaussian_polynomial_ridge_uniform_L2 · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be any finite-dimensional real inner-product normed space with its Borel measurable structure, and p any real polynomial. Put phi(z)=p(z), gamma1=N(0,1), gammaE=stdGaussian(E), and U={w in E: norm(w)=1}. Then phi genuinely belongs to L2(gamma1). Define b=norm(phi)_{L2(gamma1)}+1. One has b>0, and every actual ridge x↦phi(<w,x>) for w in U genuinely belongs to L2(gammaE), with norm exactly norm(phi)_{L2(gamma1)} and hence at most b. The one base norm and the same b serve every direction and dimension. Neither positive dimension, a nonzero polynomial nor evenness is required; the feature conclusions are vacuous when U is empty. No feature moment, covariance or uniform bound is assumed.

\[\|\phi(\langle w,\cdot\rangle)\|_{L^2(\gamma_E)}=\|\phi\|_{L^2(\gamma_1)}<b:=\|\phi\|_{L^2(\gamma_1)}+1\quad(\|w\|=1).\]

Lean statement · standard_gaussian_polynomial_ridge_uniform_L2

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 standard_gaussian_polynomial_ridge_uniform_L2
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (p : Polynomial ℝ) :
    let phi : ℝ → ℝ := fun z => p.eval z
    ∃ hbase : MemLp phi 2 (ProbabilityTheory.gaussianReal 0 1),
      let b : ℝ := ‖hbase.toLp phi‖ + 1
      (0 < b) ∧
      ∃ hfeature : ∀ w : {w : E // ‖w‖ = 1},
        MemLp (fun x : E => phi ⟪w.1, x⟫_ℝ) 2 (ProbabilityTheory.stdGaussian E),
        ∀ w : {w : E // ‖w‖ = 1},
          ‖(hfeature w).toLp (fun x : E => phi ⟪w.1, x⟫_ℝ)‖ = ‖hbase.toLp phi‖ ∧
          ‖(hfeature w).toLp (fun x : E => phi ⟪w.1, x⟫_ℝ)‖ ≤ b

Exact module and namespace context

Proof roadmap

1Produce polynomial moments
The actual scalar Gaussian has every finite moment. Thus z^n belongs to L2 since its squared absolute value is |z|^(2n). Finite polynomial induction, addition and coefficient scaling produce L2 membership of phi; no moment premise is introduced.
2Identify the actual projection law
A continuous linear functional of the standard Gaussian is Gaussian with mean zero and variance equal to its squared dual norm. The inner-product functional at a unit vector has norm one, so the pushforward is exactly gamma1.
3Transport the genuine L2 class
This measurable projection preserves the indicated measures. Pull back phi and its actual almost-everywhere class. The induced L2 pullback is an isometry, proving membership and equality of norms simultaneously.
4Choose one positive common bound
A norm is nonnegative, so adding one makes b strictly positive. The exact isometry gives the same bound for every unit weight, with no dimension or direction in its definition.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product normed space; its measurable structure is Borel.
p is any finite real polynomial. The Gaussian measures are actual standard Gaussian laws, and feature weights range over the literal unit-norm subtype.

Mathematical proof

1. Produce polynomial moments

The actual scalar Gaussian has every finite moment. Thus z^n belongs to L2 since its squared absolute value is |z|^(2n). Finite polynomial induction, addition and coefficient scaling produce L2 membership of phi; no moment premise is introduced.

\[\int |z^n|^2\,d\gamma_1(z)=\int |z|^{2n}\,d\gamma_1(z)<\infty.\]

Corresponding Lean step

The adjacent initially folded Lean contains the exact statement and proof of this step.

2. Identify the actual projection law

A continuous linear functional of the standard Gaussian is Gaussian with mean zero and variance equal to its squared dual norm. The inner-product functional at a unit vector has norm one, so the pushforward is exactly gamma1.

\[(x\mapsto\langle w,x\rangle)_\#\gamma_E=\gamma_1\quad(\|w\|=1).\]

Corresponding Lean step

The adjacent initially folded Lean contains the exact statement and proof of this step.

3. Transport the genuine L2 class

This measurable projection preserves the indicated measures. Pull back phi and its actual almost-everywhere class. The induced L2 pullback is an isometry, proving membership and equality of norms simultaneously.

\[\|\phi(\langle w,\cdot\rangle)\|_{L^2(\gamma_E)}=\|\phi\|_{L^2(\gamma_1)}.\]

Corresponding Lean step

The adjacent initially folded Lean contains the exact statement and proof of this step.

4. Choose one positive common bound

A norm is nonnegative, so adding one makes b strictly positive. The exact isometry gives the same bound for every unit weight, with no dimension or direction in its definition.

\[b=\|\phi\|_{L^2(\gamma_1)}+1\ge1>0.\]

Corresponding Lean step

The adjacent initially folded Lean contains the exact statement and proof of this step.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · standard_gaussian_polynomial_ridge_uniform_L2

See the adjacent exact Lean and the four mathematical proof steps.

Download module (.lean)

theorem standard_gaussian_polynomial_ridge_uniform_L2
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (p : Polynomial ℝ) :
    let phi : ℝ → ℝ := fun z => p.eval z
    ∃ hbase : MemLp phi 2 (ProbabilityTheory.gaussianReal 0 1),
      let b : ℝ := ‖hbase.toLp phi‖ + 1
      (0 < b) ∧
      ∃ hfeature : ∀ w : {w : E // ‖w‖ = 1},
        MemLp (fun x : E => phi ⟪w.1, x⟫_ℝ) 2 (ProbabilityTheory.stdGaussian E),
        ∀ w : {w : E // ‖w‖ = 1},
          ‖(hfeature w).toLp (fun x : E => phi ⟪w.1, x⟫_ℝ)‖ = ‖hbase.toLp phi‖ ∧
          ‖(hfeature w).toLp (fun x : E => phi ⟪w.1, x⟫_ℝ)‖ ≤ b := by
  let phi : ℝ → ℝ := fun z => p.eval z
  have hpow : ∀ n : ℕ,
      MemLp (fun z : ℝ => z ^ n) 2 (gaussianReal 0 1) := by
    intro n
    apply (memLp_two_iff_integrable_sq (by fun_prop)).2
    have hid : MemLp (id : ℝ → ℝ) (↑(2 * n) : ℝ≥0∞) (gaussianReal 0 1) :=
      memLp_id_gaussianReal' (↑(2 * n) : ℝ≥0∞) (ENNReal.natCast_ne_top (2 * n))
    have hi := hid.integrable_norm_pow' (p := 2 * n)
    convert hi using 1
    funext z
    change (z ^ n) ^ 2 = ‖z‖ ^ (2 * n)
    rw [Nat.mul_comm 2 n, pow_mul, ← norm_pow, Real.norm_eq_abs, sq_abs]
  have hbase : MemLp phi 2 (gaussianReal 0 1) := by
    change MemLp (fun z : ℝ => p.eval z) 2 (gaussianReal 0 1)
    induction p using Polynomial.induction_on' with
    | add p q hp hq => simpa only [Polynomial.eval_add, Pi.add_def] using hp.add hq
    | monomial n a => simpa only [Polynomial.eval_monomial] using (hpow n).const_mul a
  have hmap : ∀ w : {w : E // ‖w‖ = 1},
      (stdGaussian E).map (fun x : E => ⟪w.1, x⟫_ℝ) = gaussianReal 0 1 := by
    intro w
    change (stdGaussian E).map (innerSL ℝ w.1) = _
    rw [IsGaussian.map_eq_gaussianReal, integral_strongDual_stdGaussian,
      variance_dual_stdGaussian, innerSL_apply_norm, w.2]
    norm_num
  let mp : ∀ w : {w : E // ‖w‖ = 1},
      MeasurePreserving (fun x : E => ⟪w.1, x⟫_ℝ) (stdGaussian E) (gaussianReal 0 1) :=
    fun w => ⟨by fun_prop, hmap w⟩
  let hfeature : ∀ w : {w : E // ‖w‖ = 1},
      MemLp (fun x : E => phi ⟪w.1, x⟫_ℝ) 2 (stdGaussian E) :=
    fun w => hbase.comp_measurePreserving (mp w)
  refine ⟨hbase, ?_, hfeature, ?_⟩
  · exact add_pos_of_nonneg_of_pos (norm_nonneg _) zero_lt_one
  · intro w
    have hn : ‖(hfeature w).toLp (fun x : E => phi ⟪w.1, x⟫_ℝ)‖ = ‖hbase.toLp phi‖ := by
      change ‖Lp.compMeasurePreserving (fun x : E => ⟪w.1, x⟫_ℝ) (mp w)
        (hbase.toLp phi)‖ = ‖hbase.toLp phi‖
      exact Lp.norm_compMeasurePreserving _ _
    exact ⟨hn, hn.trans_le (le_add_of_nonneg_right zero_le_one)⟩

end AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge

Exact module and namespace context

Scope and omitted-condition boundaries

The Gaussian law and unit norm are essential. This is not a theorem for arbitrary rotation-invariant heavy-tailed laws or unbounded directions.
No pointwise feature bound is claimed. No label moment, averaging over arbitrary parameter laws, global risk first variation or stochastic convergence is supplied.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

memLp_id_gaussianReal'
MemLp.integrable_norm_pow'
Polynomial.induction_on'
IsGaussian.map_eq_gaussianReal
integral_strongDual_stdGaussian
variance_dual_stdGaussian
Lp.norm_compMeasurePreserving

Mathematical sources

Samplinglib original Gaussian polynomial ridge supplementv1 (2026-10-20) (historical source) — Authored generic background proof from the listed pinned Mathlib facts; not a primary-book 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.