AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRisk

Samplinglib mathematical lesson

An actual Gaussian joint-data risk has a first variation

AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRisk.gaussian_polynomial_joint_risk_first_variation · theorem · Teaching coverage

Read this first

Mathematical statement

Let P be an actual probability law on E×ℝ, where E is a finite-dimensional real inner-product space with its Borel structure. Assume only that its input marginal is the standard Gaussian and its actual response coordinate Y is square-integrable. Let p be any finite real polynomial. For any probability ρ on the unit sphere define fρ(x)=∫p(⟨w,x⟩) dρ(w), F(ρ)=∫(fρ(x)−y)² dP(x,y), and Vρ(w)=2∫(fρ(x)−y)p(⟨w,x⟩) dP(x,y). Every squared loss is integrable, and every displayed inner residual-feature product is integrable at every unit direction. For any two parameter probabilities ρ₀,ρ₁, Vρ₀ is integrable under both laws. The actual scalar risk along (1−t)ρ₀+tρ₁ has right derivative ∫Vρ₀ dρ₁−∫Vρ₀ dρ₀ at zero, and F(ρ₁)≥F(ρ₀)+∫Vρ₀ dρ₁−∫Vρ₀ dρ₀.

\[\left.\frac d{dt}F((1-t)\rho_0+t\rho_1)\right|_{0^+}=\int V_{\rho_0}\,d\rho_1-\int V_{\rho_0}\,d\rho_0,\qquad F(\rho_1)\ge F(\rho_0)+\int V_{\rho_0}\,d(\rho_1-\rho_0).\]

Lean statement · gaussian_polynomial_joint_risk_first_variation

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 gaussian_polynomial_joint_risk_first_variation
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (P : Measure (E × ℝ)) [IsProbabilityMeasure P]
    (hGaussian : P.map Prod.fst = ProbabilityTheory.stdGaussian E)
    (p : Polynomial ℝ)
    (hlabel : MemLp (fun z : E × ℝ => z.2) 2 P) :
    let U := {w : E // ‖w‖ = 1}
    let predictor : Measure U → E → ℝ := fun rho x => ∫ w : U, p.eval ⟪w.1,x⟫_ℝ ∂rho
    let risk : Measure U → ℝ := fun rho => ∫ z, (predictor rho z.1 - z.2)^2 ∂P
    let potential : Measure U → U → ℝ := fun rho w =>
      2 * ∫ z, (predictor rho z.1 - z.2) * p.eval ⟪w.1,z.1⟫_ℝ ∂P
    (∀ rho : Measure U, IsProbabilityMeasure rho →
      Integrable (fun z : E × ℝ => (predictor rho z.1 - z.2)^2) P ∧
      ∀ w : U, Integrable (fun z : E × ℝ =>
        (predictor rho z.1 - z.2) * p.eval ⟪w.1,z.1⟫_ℝ) P) ∧
    ∀ rho0 rho1 : Measure U, IsProbabilityMeasure rho0 → IsProbabilityMeasure rho1 →
      let curve : ℝ → Measure U := fun t =>
        ENNReal.ofReal (1-t) • rho0 + ENNReal.ofReal t • rho1
      Integrable (potential rho0) rho0 ∧ Integrable (potential rho0) rho1 ∧
      HasDerivWithinAt (fun t => risk (curve t))
        ((∫ w, potential rho0 w ∂rho1) - (∫ w, potential rho0 w ∂rho0))
        (Set.Icc (0 : ℝ) 1) 0 ∧
      risk rho0 + ((∫ w, potential rho0 w ∂rho1) - (∫ w, potential rho0 w ∂rho0)) ≤
        risk rho1

Exact module and namespace context

Proof roadmap

1Pull the actual mean to the joint data law
The first-coordinate map preserves the actual marginal measures. Its continuous linear L² isometry commutes with Bochner integration, transporting the scalar-average class identity to L²(P).
2Identify the true squared risk
Subtract the actual label class. Its squared norm is the literal integrated squared residual. Cauchy–Schwarz also gives genuine residual-feature product integrability at every direction.
3Identify the actual potential
Almost-everywhere representative identities give the exact residual-feature inner-product formula. The bounded linear residual functional proves integrability of this scalar potential under both parameter laws.
4Use the positive probability segment
Apply the actual probability-segment mean calculus, and identify its norm risk with the literal scalar risk at every point of the interval. Restriction at zero gives the stated right derivative.
5Obtain linear convexity
The difference between the risk increment and the potential pairing is the squared mean increment. Its nonnegativity gives the supporting inequality with the correct sign and factor two.

Full assumptions and notation

All objects and hypotheses

E has finite-dimensional real inner-product and Borel structures. P is a true joint probability with standard Gaussian first marginal.
p is any finite real polynomial, and the actual second-coordinate response belongs to L²(P). Input and response need not be independent.

Mathematical proof

1. Pull the actual mean to the joint data law

The first-coordinate map preserves the actual marginal measures. Its continuous linear L² isometry commutes with Bochner integration, transporting the scalar-average class identity to L²(P).

\[[f_\rho(X)]_{L^2(P)}=\int[p(\langle w,X\rangle)]_{L^2(P)}\,d\rho(w).\]

Corresponding Lean step