Samplinglib mathematical lesson

A literal finite-average risk equals its L² norm

AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.empirical_squared_risk_eq_L2_norm · theorem · Teaching coverage

Read this first

Mathematical statement

Let P be any measure on a measurable space Omega, N any natural number, a_j:Omega→R for j:Fin N, and y:Omega→R. Suppose every a_j and y belongs to L²(P). Then the actual scalar squared residual (N^{-1} sum_j a_j-y)^2 is integrable, and its integral equals the squared L² norm of N^{-1} sum_j [a_j]-[y], where brackets are the equivalence classes of the stated functions. No probability or finite-measure hypothesis is needed. N=0 uses the empty sum and totalized real inverse.

\[\int\left(N^{-1}\sum_j a_j-y\right)^2dP=\left\|N^{-1}\sum_j[a_j]-[y]\right\|_{L^2(P)}^2.\]

Lean statement · empirical_squared_risk_eq_L2_norm

Let P be any measure on a measurable space Omega, N any natural number, a_j:Omega->R for j:Fin N, and y:Omega->R. Suppose every a_j and y belongs to L²(P). Then the actual scalar squared residual (N^{-1} sum_j a_j-y)^2 is integrable, and its integral equals the squared L² norm of N^{-1} sum_j [a_j]-[y], where brackets are the equivalence classes of the stated functions. No probability or finite-measure hypothesis is needed. N=0 uses the empty sum and totalized real inverse.

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 empirical_squared_risk_eq_L2_norm
    {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) (N : ℕ)
    (feature : Fin N → Omega → ℝ) (label : Omega → ℝ)
    (hfeature : ∀ i, MemLp (feature i) 2 mu) (hlabel : MemLp label 2 mu) :
    Integrable (fun omega => ((N : ℝ)⁻¹ * ∑ i, feature i omega - label omega) ^ 2) mu ∧
    (∫ omega, ((N : ℝ)⁻¹ * ∑ i, feature i omega - label omega) ^ 2 ∂mu) =
      ‖(N : ℝ)⁻¹ • ∑ i, (hfeature i).toLp (feature i) - hlabel.toLp label‖ ^ 2

Exact module and namespace context

Proof roadmap

1Produce the actual residual in L²
Finite sums, scalar multiplication and subtraction preserve L² membership. Therefore its square is integrable.
2Identify the representative
Use the almost-everywhere representative identities for each actual toLp class, finite sum, scalar multiple and difference. The assembled class represents the actual scalar residual.
3Evaluate the Hilbert norm
The L² inner product is the actual integral of pointwise products, and the squared norm is the self inner product.

Full assumptions and notation

All objects and hypotheses

Every selected scalar feature a_j and the label function y is genuinely MemLp at exponent2 under P.
P is any measure; N may be zero in this finite-average identity.

Mathematical proof

1. Produce the actual residual in L²

Finite sums, scalar multiplication and subtraction preserve L² membership. Therefore its square is integrable.

\[r=N^{-1}\sum_j a_j-y\in L^2(P).\]

Corresponding Lean step

The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.

2. Identify the representative

Use the almost-everywhere representative identities for each actual toLp class, finite sum, scalar multiple and difference. The assembled class represents the actual scalar residual.

\[[r]=N^{-1}\sum_j[a_j]-[y].\]

Corresponding Lean step

The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.

3. Evaluate the Hilbert norm

The L² inner product is the actual integral of pointwise products, and the squared norm is the self inner product.

\[\|[r]\|_2^2=\langle[r],[r]\rangle=\int r^2dP.\]

Corresponding Lean step

The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.

Lean verification

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

Lean proof · empirical_squared_risk_eq_L2_norm

See the adjacent exact Lean and the mathematical proof steps.

Download module (.lean)

theorem empirical_squared_risk_eq_L2_norm
    {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) (N : ℕ)
    (feature : Fin N → Omega → ℝ) (label : Omega → ℝ)
    (hfeature : ∀ i, MemLp (feature i) 2 mu) (hlabel : MemLp label 2 mu) :
    Integrable (fun omega => ((N : ℝ)⁻¹ * ∑ i, feature i omega - label omega) ^ 2) mu ∧
    (∫ omega, ((N : ℝ)⁻¹ * ∑ i, feature i omega - label omega) ^ 2 ∂mu) =
      ‖(N : ℝ)⁻¹ • ∑ i, (hfeature i).toLp (feature i) - hlabel.toLp label‖ ^ 2 := by
  classical
  let z : Lp ℝ 2 mu :=
    (N : ℝ)⁻¹ • ∑ i, (hfeature i).toLp (feature i) - hlabel.toLp label
  have hres : MemLp (fun omega => (N : ℝ)⁻¹ * ∑ i, feature i omega - label omega) 2 mu := by
    have hs := memLp_finsetSum Finset.univ (fun i _ => hfeature i)
    exact (hs.const_smul (N : ℝ)⁻¹).sub hlabel
  refine ⟨hres.integrable_sq, ?_⟩
  have hz : (fun omega => z omega) =ᵐ[mu]
      (fun omega => (N : ℝ)⁻¹ * ∑ i, feature i omega - label omega) := by
    filter_upwards [Lp.coeFn_sub ((N : ℝ)⁻¹ • ∑ i, (hfeature i).toLp (feature i))
        (hlabel.toLp label),
      Lp.coeFn_smul (N : ℝ)⁻¹ (∑ i, (hfeature i).toLp (feature i)),
      Lp.coeFn_fun_finsetSum Finset.univ (fun i => (hfeature i).toLp (feature i)),
      ae_all_iff.2 (fun i => (hfeature i).coeFn_toLp), hlabel.coeFn_toLp]
      with omega hsub hsmul hsum hf hy
    change (((N : ℝ)⁻¹ • ∑ i, (hfeature i).toLp (feature i) - hlabel.toLp label) omega) = _
    simp only [Pi.sub_apply, Pi.smul_apply, smul_eq_mul] at hsub hsmul
    rw [hsub, hsmul, hsum, hy]
    simp only [hf]
  change (∫ omega, ((N : ℝ)⁻¹ * ∑ i, feature i omega - label omega) ^ 2 ∂mu) = ‖z‖ ^ 2
  rw [← real_inner_self_eq_norm_sq, L2.inner_def]
  symm
  apply integral_congr_ae
  filter_upwards [hz] with omega homega
  simp only [homega, real_inner_self_eq_norm_sq, Real.norm_eq_abs, sq_abs]

Exact module and namespace context

Scope and omitted-condition boundaries

This identity alone does not identify a weight-law predictor with this finite average.
It supplies no all-law first variation or feature differentiability.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

memLp_finsetSum
MemLp.integrable_sq
Lp.coeFn_sub
Lp.coeFn_smul
Lp.coeFn_fun_finsetSum
MemLp.coeFn_toLp
L2.inner_def
integral_congr_ae

Mathematical sources

Samplinglib quadratic feature-risk supplement, version1 (2026-10-20) (historical source) — Original library derivation from the explicitly listed Mathlib facts; not attributed to a theorem of the chapter source.

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