Gaussian polynomial features vary continuously in L²
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging.continuous_gaussian_polynomial_ridge_L2 · theorem · Teaching coverage
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.
Lean statement · continuous_gaussian_polynomial_ridge_L2
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.
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.
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⟫_ℝ))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‖.
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.
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.
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.
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.
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).tendstoScope 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
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.