Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Construct the empirical law and evaluate its actual risk

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

Read this first

Mathematical statement

Let W be a measurable space with measurable singleton points, Omega a measurable data space and P any measure on Omega. Let N>0, w:Fin N→W, scalar features K:W→Omega→R, and a label y:Omega→R. Suppose K(w_j) and y are in L²(P). Define rho=N^{-1} sum_j Dirac(w_j), using reciprocal N as an ENNReal measure weight. Then rho is a probability measure, the actual loss (integral K(q,omega) drho(q)-y(omega))² is integrable under P, and its integral equals ||N^{-1} sum_j [K(w_j)]-[y]||². Particle values may coincide. No global measurability in q or probability assumption on P is required for this finite atomic assertion.

\[\rho=\frac1N\sum_j\delta_{w_j},\qquad \int\left(\int K(q,\omega)d\rho(q)-y(\omega)\right)^2dP=\left\|\frac1N\sum_j[K(w_j)]-[y]\right\|_2^2.\]
Lean statement · empirical_law_squared_risk_eq_L2_norm

Let W be a measurable space with measurable singleton points, Omega a measurable data space and P any measure on Omega. Let N>0, w:Fin N->W, scalar features K:W->Omega->R, and a label y:Omega->R. Suppose K(w_j) and y are in L²(P). Define rho=N^{-1} sum_j Dirac(w_j), using reciprocal N as an ENNReal measure weight. Then rho is a probability measure, the actual loss (integral K(q,omega) drho(q)-y(omega))² is integrable under P, and its integral equals ||N^{-1} sum_j [K(w_j)]-[y]||². Particle values may coincide. No global measurability in q or probability assumption on P is required for this finite atomic assertion.

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_law_squared_risk_eq_L2_norm
    {W Omega : Type*} [MeasurableSpace W] [MeasurableSingletonClass W]
    [MeasurableSpace Omega] (P : Measure Omega) {N : ℕ} (hN : 0 < N)
    (w : Fin N → W) (K : W → Omega → ℝ) (label : Omega → ℝ)
    (hfeature : ∀ i, MemLp (K (w i)) 2 P) (hlabel : MemLp label 2 P) :
    let rho : Measure W := (N : ℝ≥0∞)⁻¹ • ∑ i, Measure.dirac (w i)
    IsProbabilityMeasure rho ∧
    Integrable (fun omega => ((∫ q, K q omega ∂rho) - label omega) ^ 2) P ∧
    (∫ omega, ((∫ q, K q omega ∂rho) - label omega) ^ 2 ∂P) =
      ‖(N : ℝ)⁻¹ • ∑ i, (hfeature i).toLp (K (w i)) - hlabel.toLp label‖ ^ 2

Exact module and namespace context

Proof roadmap

  1. 1Normalize the actual finite measure

    The sum of N Dirac masses has total mass N. Its nonzero finite reciprocal weight gives total mass one.

  2. 2Evaluate each actual predictor slice

    Every function is integrable under a Dirac at a measurable singleton point. Finite-measure-sum and scalar integration give the literal predictor for every data point.

  3. 3Apply the finite residual identity

    The actual predictor is now the finite average, so the previous L² residual theorem yields both loss integrability and the exact risk norm.

Full assumptions and notation

All objects and hypotheses

  • N>0; W has measurable singleton points.
  • Every selected feature K(w_j) and y is in L²(P); repeated atoms are allowed.

Mathematical proof

1. Normalize the actual finite measure

The sum of N Dirac masses has total mass N. Its nonzero finite reciprocal weight gives total mass one.

\[\rho(W)=N^{-1}N=1.\]
Corresponding Lean step

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

2. Evaluate each actual predictor slice

Every function is integrable under a Dirac at a measurable singleton point. Finite-measure-sum and scalar integration give the literal predictor for every data point.

\[\int K(q,\omega)d\rho(q)=N^{-1}\sum_jK(w_j,\omega).\]
Corresponding Lean step

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

3. Apply the finite residual identity

The actual predictor is now the finite average, so the previous L² residual theorem yields both loss integrability and the exact risk norm.

\[F(\rho)=\left\|N^{-1}\sum_j[K(w_j)]-[y]\right\|_2^2.\]
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_law_squared_risk_eq_L2_norm

See the adjacent exact Lean and the mathematical proof steps.

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_law_squared_risk_eq_L2_norm
    {W Omega : Type*} [MeasurableSpace W] [MeasurableSingletonClass W]
    [MeasurableSpace Omega] (P : Measure Omega) {N : ℕ} (hN : 0 < N)
    (w : Fin N → W) (K : W → Omega → ℝ) (label : Omega → ℝ)
    (hfeature : ∀ i, MemLp (K (w i)) 2 P) (hlabel : MemLp label 2 P) :
    let rho : Measure W := (N : ℝ≥0∞)⁻¹ • ∑ i, Measure.dirac (w i)
    IsProbabilityMeasure rho ∧
    Integrable (fun omega => ((∫ q, K q omega ∂rho) - label omega) ^ 2) P ∧
    (∫ omega, ((∫ q, K q omega ∂rho) - label omega) ^ 2 ∂P) =
      ‖(N : ℝ)⁻¹ • ∑ i, (hfeature i).toLp (K (w i)) - hlabel.toLp label‖ ^ 2 := by
  classical
  dsimp only
  let rho : Measure W := (N : ℝ≥0∞)⁻¹ • ∑ i, Measure.dirac (w i)
  have hprob : IsProbabilityMeasure rho := by
    constructor
    simpa [rho, Measure.smul_apply] using
      ENNReal.inv_mul_cancel (show (N : ℝ≥0∞) ≠ 0 by exact_mod_cast hN.ne') (by simp)
  have hpred : ∀ omega, (∫ q, K q omega ∂rho) = (N : ℝ)⁻¹ * ∑ i, K (w i) omega := by
    intro omega
    change (∫ q, K q omega ∂((N : ℝ≥0∞)⁻¹ • ∑ i, Measure.dirac (w i))) = _
    rw [integral_smul_measure]
    rw [integral_finsetSum_measure (fun i _ => integrable_dirac (by simp))]
    simp [smul_eq_mul]
  have hbase := empirical_squared_risk_eq_L2_norm P N
    (fun i => K (w i)) label hfeature hlabel
  refine ⟨hprob, ?_, ?_⟩
  · change Integrable (fun omega => ((∫ q, K q omega ∂rho) - label omega) ^ 2) P
    simpa only [hpred] using hbase.1
  · change (∫ omega, ((∫ q, K q omega ∂rho) - label omega) ^ 2 ∂P) = _
    simpa only [hpred] using hbase.2

Exact module and namespace context

Scope and omitted-condition boundaries
  • Fixed finite atomic laws only; no arbitrary parameter-law integration or parameter measurability is inferred.
  • No general first variation is identified.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • ENNReal.inv_mul_cancel
  • integral_smul_measure
  • integral_finsetSum_measure
  • integrable_dirac

Mathematical sources

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