GaussianPolynomialAveraging: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Gaussian polynomial features vary continuously in L²
Scalar feature averages equal their Bochner L² means

Samplinglib mathematical lesson

Gaussian polynomial features vary continuously in L²

AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging.continuous_gaussian_polynomial_ridge_L2 · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space with its Borel measurable structure, γ its centered standard Gaussian law with identity covariance, and p any finite real polynomial. For every unit vector w, the actual scalar function x↦p(⟨w,x⟩) belongs to L²(γ). These membership witnesses can be chosen together so that their actual almost-everywhere equivalence classes form a continuous map from the unit sphere, with its subspace topology, into L²(γ). No feature moment, uniform bound, dominating function, or continuity assumption is supplied.

\[w\longmapsto [x\mapsto p(\langle w,x\rangle)]\quad\text{is continuous into }L^2(\gamma).\]

Lean statement · continuous_gaussian_polynomial_ridge_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 continuous_gaussian_polynomial_ridge_L2
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (p : Polynomial ℝ) :
    ∃ hfeature : ∀ w : {w : E // ‖w‖ = 1},
      MemLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ) 2 (ProbabilityTheory.stdGaussian E),
      Continuous (fun w : {w : E // ‖w‖ = 1} =>
        (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ))

Exact module and namespace context

Proof roadmap

1Construct an integrable radial envelope
Finite Gaussian norm moments put every radial power in L². Polynomial induction produces a nonnegative B∈L² bounding every unit-weight feature, using |⟨w,x⟩|≤‖x‖.
2Use the genuine feature classes
The actual Gaussian projection theorem supplies membership of each displayed feature. The target map takes its actual equivalence class, not an arbitrary substitute.
3Apply dominated convergence to the squared distance
Pointwise polynomial continuity and the common envelope control every squared difference. The integral is exactly the squared norm of the genuine class difference.
4Recover norm continuity
The dominated squared-distance integral tends to zero. Continuity of the square root gives convergence in the L² norm.

Full assumptions and notation

All objects and hypotheses

E has finite-dimensional real inner-product and Borel structures.
p is any finite real polynomial, including zero, constant and non-even polynomials. Weights form the literal unit-norm subtype.

Mathematical proof

1. Construct an integrable radial envelope

Finite Gaussian norm moments put every radial power in L². Polynomial induction produces a nonnegative B∈L² bounding every unit-weight feature, using |⟨w,x⟩|≤‖x‖.

\[|p(\langle w,x\rangle)|\le B(x),\qquad B\in L^2(\gamma).\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

2. Use the genuine feature classes

The actual Gaussian projection theorem supplies membership of each displayed feature. The target map takes its actual equivalence class, not an arbitrary substitute.

\[\Phi(w)=[p(\langle w,\cdot\rangle)]_{L^2(\gamma)}.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

3. Apply dominated convergence to the squared distance

Pointwise polynomial continuity and the common envelope control every squared difference. The integral is exactly the squared norm of the genuine class difference.

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

4. Recover norm continuity

The dominated squared-distance integral tends to zero. Continuity of the square root gives convergence in the L² norm.

\[\|\Phi(w)-\Phi(w_0)\|\longrightarrow0\quad(w\to w_0).\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

Lean verification

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

Lean proof · continuous_gaussian_polynomial_ridge_L2

The formula proof above explains the mathematical moves; the adjacent folded Lean gives their exact implementation.

Download module (.lean)

theorem continuous_gaussian_polynomial_ridge_L2
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (p : Polynomial ℝ) :
    ∃ hfeature : ∀ w : {w : E // ‖w‖ = 1},
      MemLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ) 2 (ProbabilityTheory.stdGaussian E),
      Continuous (fun w : {w : E // ‖w‖ = 1} =>
        (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ)) := by
  classical
  letI : CompleteSpace E := FiniteDimensional.complete ℝ E
  letI : SecondCountableTopology E := inferInstance
  let μ := stdGaussian E
  obtain ⟨B,hB,hBpos,hBbound⟩ := polynomial_norm_envelope (E := E) p
  obtain ⟨hb, hbpos, hf, hnorm⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge.standard_gaussian_polynomial_ridge_uniform_L2 (E := E) p
  refine ⟨hf, ?_⟩
  let F := fun w : {w : E // ‖w‖ = 1} => (hf w).toLp (fun x => p.eval ⟪w.1,x⟫_ℝ)
  change Continuous F
  apply continuous_iff_continuousAt.2
  intro w₀
  have hBsq : Integrable (fun x => 4 * (B x)^2) μ :=
    ((memLp_two_iff_integrable_sq hB.1).1 hB).const_mul 4
  have hn (w) : ‖F w - F w₀‖^2 =
      ∫ x, (p.eval ⟪w.1,x⟫_ℝ - p.eval ⟪w₀.1,x⟫_ℝ)^2 ∂μ := by
    rw [← real_inner_self_eq_norm_sq, L2.inner_def]
    apply integral_congr_ae
    filter_upwards [Lp.coeFn_sub (F w) (F w₀), (hf w).coeFn_toLp, (hf w₀).coeFn_toLp] with x hx hw hw₀
    simp only [hx, Pi.sub_apply, F] at *
    rw [hw,hw₀]
    simp [real_inner_self_eq_norm_sq, Real.norm_eq_abs, sq_abs]
  have hc : ContinuousAt (fun w : {w : E // ‖w‖ = 1} =>
      ∫ x, (p.eval ⟪w.1,x⟫_ℝ - p.eval ⟪w₀.1,x⟫_ℝ)^2 ∂μ) w₀ := by
    apply continuousAt_of_dominated (bound := fun x => 4 * (B x)^2)
    · exact Eventually.of_forall fun w => by fun_prop
    · exact Eventually.of_forall fun w => ae_of_all _ fun x => by
        rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
        have h := (norm_sub_le (p.eval ⟪w.1,x⟫_ℝ) (p.eval ⟪w₀.1,x⟫_ℝ)).trans
          (add_le_add (hBbound w x) (hBbound w₀ x))
        have hs := (sq_le_sq₀ (norm_nonneg _) (add_nonneg (hBpos x) (hBpos x))).2 h
        simpa only [Real.norm_eq_abs, sq_abs] using hs.trans_eq (by ring)
    · exact hBsq
    · exact ae_of_all _ fun x => by fun_prop
  have hsq : ContinuousAt (fun w => ‖F w - F w₀‖^2) w₀ := by
    simpa only [← hn] using hc
  rw [ContinuousAt, tendsto_iff_dist_tendsto_zero]
  simpa only [Function.comp_def, Real.sqrt_sq (norm_nonneg _), sub_self, norm_zero, zero_pow (by decide : 2 ≠ 0),
    Real.sqrt_zero, dist_eq_norm] using
    (Real.continuous_sqrt.continuousAt.comp hsq).tendsto

Exact module and namespace context

Scope and omitted-condition boundaries

This is a statement about actual standard Gaussian inputs, not every rotation-invariant or heavy-tailed law.
No parameter-law average, label, risk derivative, or spatial derivative is part of this continuity conclusion. The unit domain may be empty in dimension zero.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge.standard_gaussian_polynomial_ridge_uniform_L2

Mathlib API called (external library)

ProbabilityTheory.IsGaussian.memLp_id
MeasureTheory.MemLp.integrable_norm_pow'
Polynomial.induction_on'
MeasureTheory.continuousAt_of_dominated
MeasureTheory.L2.inner_def
Real.continuous_sqrt

Mathematical sources

Samplinglib original probability and Gaussian feature regularity supplement v1 (2026-10-20) (historical source) — Original generic mathematical supplement from the cited pinned library prerequisites; no primary-textbook theorem or statistical convergence credit.

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

Samplinglib mathematical lesson

Scalar feature averages equal their Bochner L² means

AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging.gaussian_polynomial_parameter_average_L2 · theorem · Teaching coverage

Read this first

Mathematical statement

Under the same finite-dimensional real inner-product, Borel and finite-polynomial assumptions, let Φ(w) be the actual L² class of x↦p(⟨w,x⟩) under the standard Gaussian γ. The feature membership witnesses are produced together with continuity of Φ. For every probability law ρ on the unit sphere, the scalar feature is genuinely integrable in w for every fixed x, and Φ is genuinely Bochner integrable under ρ. The literal scalar-average function x↦∫p(⟨w,x⟩) dρ(w) belongs to L²(γ), and its actual L² class equals ∫Φ dρ. All membership, measurability and integral-exchange obligations are conclusions of the theorem.

\[\left[x\mapsto\int p(\langle w,x\rangle)\,d\rho(w)\right]_{L^2(\gamma)}=\int\Phi(w)\,d\rho(w).\]

Lean statement · gaussian_polynomial_parameter_average_L2

Download module (.lean)

theorem gaussian_polynomial_parameter_average_L2
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (p : Polynomial ℝ) :
    ∃ hfeature : ∀ w : {w : E // ‖w‖ = 1},
      MemLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ) 2 (ProbabilityTheory.stdGaussian E),
      Continuous (fun w : {w : E // ‖w‖ = 1} =>
        (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ)) ∧
      ∀ rho : Measure {w : E // ‖w‖ = 1}, IsProbabilityMeasure rho →
        (∀ x : E, Integrable (fun w : {w : E // ‖w‖ = 1} => p.eval ⟪w.1, x⟫_ℝ) rho) ∧
        Integrable (fun w : {w : E // ‖w‖ = 1} =>
          (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ)) rho ∧
        ∃ hmean : MemLp (fun x : E => ∫ w : {w : E // ‖w‖ = 1},
            p.eval ⟪w.1, x⟫_ℝ ∂rho) 2 (ProbabilityTheory.stdGaussian E),
          hmean.toLp (fun x : E => ∫ w : {w : E // ‖w‖ = 1}, p.eval ⟪w.1, x⟫_ℝ ∂rho) =
            ∫ w : {w : E // ‖w‖ = 1},
              (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ) ∂rho

Exact module and namespace context

Proof roadmap

1Build the actual radial envelope
Gaussian norm moments and finite polynomial induction supply a common nonnegative L² envelope for all unit-weight scalar features.
2Produce both forms of parameter integrability
For fixed x the envelope is a finite constant on the parameter space. Continuity and the Gaussian ridge norm bound give Bochner integrability of the actual L² feature map under every probability law.
3Construct the scalar mean class first
Joint continuity makes the actual scalar average measurable. Its norm is bounded by B, so it belongs to L² before any class identity is used.
4Justify Fubini for every L² test class
For any genuine g∈L²(γ), Cauchy–Schwarz makes |g|B integrable. This dominates the actual product kernel, so Fubini interchanges its two genuine scalar integrals.
5Identify the two Hilbert-space elements
Each inner integral is the inner product with Φ(w). Commuting a bounded linear functional with the Bochner mean and testing against every g proves equality of the two actual classes.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space with its Borel structure; p is any finite real polynomial.
ρ is any probability measure on the literal unit-norm subtype. No domination, moment, Bochner integrability or averaging identity is assumed.

Mathematical proof

1. Build the actual radial envelope

Gaussian norm moments and finite polynomial induction supply a common nonnegative L² envelope for all unit-weight scalar features.

\[|p(\langle w,x\rangle)|\le B(x),\quad B\in L^2(\gamma).\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

2. Produce both forms of parameter integrability

For fixed x the envelope is a finite constant on the parameter space. Continuity and the Gaussian ridge norm bound give Bochner integrability of the actual L² feature map under every probability law.

\[\int|p(\langle w,x\rangle)|\,d\rho(w)\le B(x),\qquad \int\|\Phi(w)\|\,d\rho(w)<\infty.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

3. Construct the scalar mean class first

Joint continuity makes the actual scalar average measurable. Its norm is bounded by B, so it belongs to L² before any class identity is used.

\[m_\rho(x)=\int p(\langle w,x\rangle)\,d\rho(w),\qquad |m_\rho(x)|\le B(x).\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

4. Justify Fubini for every L² test class

For any genuine g∈L²(γ), Cauchy–Schwarz makes |g|B integrable. This dominates the actual product kernel, so Fubini interchanges its two genuine scalar integrals.

\[\int g(x)m_\rho(x)\,d\gamma(x)=\int\!\int g(x)p(\langle w,x\rangle)\,d\gamma(x)\,d\rho(w).\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

5. Identify the two Hilbert-space elements

Each inner integral is the inner product with Φ(w). Commuting a bounded linear functional with the Bochner mean and testing against every g proves equality of the two actual classes.

\[\langle g,[m_\rho]\rangle=\left\langle g,\int\Phi\,d\rho\right\rangle\quad\text{for every }g\in L^2(\gamma).\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

Lean verification

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

Lean proof · gaussian_polynomial_parameter_average_L2

The formula proof above explains the mathematical moves; the adjacent folded Lean gives their exact implementation.

Download module (.lean)

theorem gaussian_polynomial_parameter_average_L2
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (p : Polynomial ℝ) :
    ∃ hfeature : ∀ w : {w : E // ‖w‖ = 1},
      MemLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ) 2 (ProbabilityTheory.stdGaussian E),
      Continuous (fun w : {w : E // ‖w‖ = 1} =>
        (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ)) ∧
      ∀ rho : Measure {w : E // ‖w‖ = 1}, IsProbabilityMeasure rho →
        (∀ x : E, Integrable (fun w : {w : E // ‖w‖ = 1} => p.eval ⟪w.1, x⟫_ℝ) rho) ∧
        Integrable (fun w : {w : E // ‖w‖ = 1} =>
          (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ)) rho ∧
        ∃ hmean : MemLp (fun x : E => ∫ w : {w : E // ‖w‖ = 1},
            p.eval ⟪w.1, x⟫_ℝ ∂rho) 2 (ProbabilityTheory.stdGaussian E),
          hmean.toLp (fun x : E => ∫ w : {w : E // ‖w‖ = 1}, p.eval ⟪w.1, x⟫_ℝ ∂rho) =
            ∫ w : {w : E // ‖w‖ = 1},
              (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ) ∂rho := by
  classical
  letI : CompleteSpace E := FiniteDimensional.complete ℝ E
  letI : SecondCountableTopology E := inferInstance
  let μ := stdGaussian E
  obtain ⟨B,hB,hBpos,hBbound⟩ := polynomial_norm_envelope (E := E) p
  obtain ⟨hf,hcont⟩ := AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging.continuous_gaussian_polynomial_ridge_L2 (E := E) p
  obtain ⟨hb, hbpos, hf8, hnorm⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge.standard_gaussian_polynomial_ridge_uniform_L2 (E := E) p
  let U := {w : E // ‖w‖ = 1}
  let K : U → E → ℝ := fun w x => p.eval ⟪w.1,x⟫_ℝ
  let F := fun w : U => (hf w).toLp (K w)
  have hFcont : Continuous F := hcont
  have hFbound (w : U) : ‖F w‖ ≤ ‖hb.toLp (fun z : ℝ => p.eval z)‖ + 1 :=
    (hnorm w).2
  have hKcont : Continuous (fun z : U × E => K z.1 z.2) := by
    change Continuous (fun z : {w : E // ‖w‖ = 1} × E => p.eval ⟪z.1.1,z.2⟫_ℝ)
    fun_prop
  refine ⟨hf, hcont, ?_⟩
  intro rho hrho
  letI : IsProbabilityMeasure rho := hrho
  have hscalar (x : E) : Integrable (fun w : U => K w x) rho := by
    apply (integrable_const (B x)).mono' (by fun_prop)
    exact ae_of_all _ fun w => hBbound w x
  have hFint : Integrable F rho := by
    apply (integrable_const (‖hb.toLp (fun z : ℝ => p.eval z)‖ + 1)).mono'
      hFcont.aestronglyMeasurable
    exact ae_of_all _ hFbound
  let mean : E → ℝ := fun x => ∫ w, K w x ∂rho
  have hmeanmeas : StronglyMeasurable mean :=
    hKcont.stronglyMeasurable.integral_prod_left'
  have hmeanbound (x : E) : ‖mean x‖ ≤ B x := by
    have h := norm_integral_le_of_norm_le_const (μ := rho) (f := fun w : U => K w x)
      (ae_of_all _ fun w => hBbound w x)
    simpa only [probReal_univ, mul_one] using h
  have hmean : MemLp mean 2 μ := hB.mono' hmeanmeas.aestronglyMeasurable
    (ae_of_all _ hmeanbound)
  refine ⟨hscalar,hFint,hmean,?_⟩
  apply ext_inner_left ℝ
  intro g
  have hC : Integrable (fun x : E => ‖g x‖ * B x) μ :=
    (Lp.memLp g).norm.integrable_mul hB
  have hHmeas : AEStronglyMeasurable (fun z : U × E => g z.2 * K z.1 z.2) (rho.prod μ) :=
    (Lp.aestronglyMeasurable g).comp_snd.mul hKcont.aestronglyMeasurable
  have hHint : Integrable (fun z : U × E => g z.2 * K z.1 z.2) (rho.prod μ) := by
    apply (hC.comp_snd rho).mono' hHmeas
    exact ae_of_all _ fun z => by
      rw [norm_mul]
      exact mul_le_mul_of_nonneg_left (hBbound z.1 z.2) (norm_nonneg _)
  have hin (w : U) : ⟪g,F w⟫_ℝ = ∫ x, g x * K w x ∂μ := by
    rw [L2.inner_def]
    apply integral_congr_ae
    filter_upwards [(hf w).coeFn_toLp] with x hx
    change inner ℝ (g x) ((hf w).toLp (K w) x) = _
    rw [hx]
    simp only [RCLike.inner_apply, conj_trivial, K, mul_comm]
  calc
    ⟪g,hmean.toLp mean⟫_ℝ = ∫ x, g x * mean x ∂μ := by
      rw [L2.inner_def]
      apply integral_congr_ae
      filter_upwards [hmean.coeFn_toLp] with x hx
      rw [hx]
      simp only [RCLike.inner_apply, conj_trivial, K, mul_comm]
    _ = ∫ x, ∫ w, g x * K w x ∂rho ∂μ := by
      apply integral_congr_ae
      exact ae_of_all _ fun x => (integral_const_mul (g x) (fun w : U => K w x)).symm
    _ = ∫ w, ∫ x, g x * K w x ∂μ ∂rho := (integral_integral_swap hHint).symm
    _ = ∫ w, ⟪g,F w⟫_ℝ ∂rho := integral_congr_ae (ae_of_all _ fun w => (hin w).symm)
    _ = ⟪g,∫ w, F w ∂rho⟫_ℝ := integral_inner hFint g

end AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging

Exact module and namespace context

Scope and omitted-condition boundaries

Pointwise evaluation is not treated as a continuous functional on L². The proof uses scalar Fubini and actual test-class inner products.
This averaging theorem has no label or risk derivative conclusion. In dimension zero there is no probability law on the empty unit subtype.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.IsGaussian.memLp_id
Continuous.aestronglyMeasurable
MeasureTheory.MemLp.mono'
MeasureTheory.integral_integral_swap
integral_inner
ext_inner_left

Mathematical sources

Samplinglib original probability and Gaussian feature regularity supplement v1 (2026-10-20) (historical source) — Original generic mathematical supplement from the cited pinned library prerequisites; no primary-textbook theorem or statistical convergence credit.

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