Scalar feature averages equal their Bochner L² means
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging.gaussian_polynomial_parameter_average_L2 · theorem · Teaching coverage
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.
Lean statement · gaussian_polynomial_parameter_average_L2
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.
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 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⟫_ℝ) ∂rhoProof 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.
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.
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.
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.
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.
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.
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 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.GaussianPolynomialAveragingScope 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
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging.continuous_gaussian_polynomial_ridge_L2AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge.standard_gaussian_polynomial_ridge_uniform_L2
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.