A true joint-data risk has a positive empirical replacement budget
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.joint_empirical_squared_risk_replacement · theorem · Teaching coverage
Mathematical statement
Let W be measurable with measurable singleton points, X measurable, and P a probability measure on X×R with input marginal PX=P.map fst. Let K:W→X→R. Suppose each K(q) is genuinely in L²(PX), every corresponding L² norm is at most the same b>0, and the true response coordinate z↦z.2 is in L²(P). For any N>0, configuration w:Fin N→W, index i and replacement u, define rho=N^{-1} sum_j Dirac(w_j), rhoNew by replacing only index i, predictor_law(x)=integral K(q,x) dlaw(q), risk(law)=integral(predictor_law(z.1)-z.2)² dP(z), and V(q)=2 integral(predictor_rho(z.1)-z.2)K(q,z.1) dP(z). Put D=integral V drhoNew-integral V drho. Then4b²>0; both empirical laws are probabilities; both actual losses and both finite-law potential integrals are integrable; D=(V(u)-V(w_i))/N; and risk(rhoNew)-risk(rho)-D equals the input-marginal integral of (predictor_rhoNew-predictor_rho)². This remainder is nonnegative and at most4b²/N². No independence of input and response, global parameter measurability, or assumed pairing/remainder/displacement bound is used.
Lean statement · joint_empirical_squared_risk_replacement
Let W be measurable with measurable singleton points, X measurable, and P a probability measure on X×R with input marginal PX=P.map fst. Let K:W->X->R. Suppose each K(q) is genuinely in L²(PX), every corresponding L² norm is at most the same b>0, and the true response coordinate z↦z.2 is in L²(P). For any N>0, configuration w:Fin N->W, index i and replacement u, define rho=N^{-1} sum_j Dirac(w_j), rhoNew by replacing only index i, predictor_law(x)=integral K(q,x) dlaw(q), risk(law)=integral(predictor_law(z.1)-z.2)² dP(z), and V(q)=2 integral(predictor_rho(z.1)-z.2)K(q,z.1) dP(z). Put D=integral V drhoNew-integral V drho. Then4b²>0; both empirical laws are probabilities; both actual losses and both finite-law potential integrals are integrable; D=(V(u)-V(w_i))/N; and risk(rhoNew)-risk(rho)-D equals the input-marginal integral of (predictor_rhoNew-predictor_rho)². This remainder is nonnegative and at most4b²/N². No independence of input and response, global parameter measurability, or assumed pairing/remainder/displacement bound is used.
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 joint_empirical_squared_risk_replacement
{W X : Type*} [MeasurableSpace W] [MeasurableSingletonClass W]
[MeasurableSpace X] (P : Measure (X × ℝ)) [IsProbabilityMeasure P]
(K : W → X → ℝ) (b : ℝ) (hb : 0 < b)
(hfeature : ∀ q, MemLp (K q) 2 (P.map Prod.fst))
(hbound : ∀ q, ‖(hfeature q).toLp (K q)‖ ≤ b)
(hlabel : MemLp (fun z : X × ℝ => z.2) 2 P)
{N : ℕ} (hN : 0 < N) (w : Fin N → W) (i : Fin N) (u : W) :
let rho : Measure W := (N : ℝ≥0∞)⁻¹ • ∑ j, Measure.dirac (w j)
let rhoNew : Measure W :=
(N : ℝ≥0∞)⁻¹ • ∑ j, Measure.dirac (Function.update w i u j)
let predictor : Measure W → X → ℝ := fun law x => ∫ q, K q x ∂law
let risk : Measure W → ℝ :=
fun law => ∫ z, (predictor law z.1 - z.2) ^ 2 ∂P
let potential : W → ℝ :=
fun q => 2 * ∫ z, (predictor rho z.1 - z.2) * K q z.1 ∂P
let pairing : ℝ := (∫ q, potential q ∂rhoNew) - (∫ q, potential q ∂rho)
(0 < 4 * b ^ 2) ∧ IsProbabilityMeasure rho ∧ IsProbabilityMeasure rhoNew ∧
Integrable (fun z : X × ℝ => (predictor rho z.1 - z.2) ^ 2) P ∧
Integrable (fun z : X × ℝ => (predictor rhoNew z.1 - z.2) ^ 2) P ∧
Integrable potential rho ∧ Integrable potential rhoNew ∧
(pairing = (N : ℝ)⁻¹ * (potential u - potential (w i))) ∧
(risk rhoNew - risk rho - pairing =
∫ x, (predictor rhoNew x - predictor rho x) ^ 2 ∂(P.map Prod.fst)) ∧
(0 ≤ risk rhoNew - risk rho - pairing) ∧
(risk rhoNew - risk rho - pairing ≤ 4 * b ^ 2 / (N : ℝ) ^ 2)Proof roadmap
- 1Construct and evaluate both empirical laws
Normalize the actual N Dirac masses, and integrate each fixed scalar slice by the finite-sum identity. Updating the configuration changes exactly one index.
- 2Lift through the true marginal
Work in H=L²(P). Write a_q=[K(q) composed with fst], y=[z↦z.2], m=N^{-1} sum_j a_(w_j), and mNew=N^{-1} sum_j a_(updated w_j). The map fst preserves P to its actual pushforward PX. Its L² pullback is an isometry. Thus the actual lifted features have the supplied norm bound under the same joint P, and the actual residual is in L².
- 3Identify the actual potential
Identify the actual finite predictor residual with its L² class. Integrating its product with each actual lifted feature gives the Hilbert inner product; both factors are in L².
- 4Produce the finite signed pairing
Integrate this same potential under each actual empirical law. Finite-sum cancellation and linearity give both the indexed update and the mean-displacement pairing.
- 5Identify the exact scalar remainder
Apply the finite Hilbert replacement identity and identify both risk norms with their actual scalar losses. Push the squared predictor difference back to the true input marginal.
- 6Obtain the uniform positive budget
The two actual lifted feature norms are at most b; their indexed average changes by at most2b/N. Square that derived estimate. The supplied positive b makes the shared budget coefficient strictly positive.
Full assumptions and notation
All objects and hypotheses
- P is the true joint data probability; PX is its pushforward by fst, and z.2 is the actual response.
- For every q, K(q) is in L²(PX) with norm at most one common b>0; z.2 is in L²(P).
- N>0; measurable singleton points permit actual finite Dirac integration. Repeated particle values are allowed.
Mathematical proof
1. Construct and evaluate both empirical laws
Normalize the actual N Dirac masses, and integrate each fixed scalar slice by the finite-sum identity. Updating the configuration changes exactly one index.
Corresponding Lean step
The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.
2. Lift through the true marginal
Work in H=L²(P). Write a_q=[K(q) composed with fst], y=[z↦z.2], m=N^{-1} sum_j a_(w_j), and mNew=N^{-1} sum_j a_(updated w_j). The map fst preserves P to its actual pushforward PX. Its L² pullback is an isometry. Thus the actual lifted features have the supplied norm bound under the same joint P, and the actual residual is in L².
Corresponding Lean step
The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.
3. Identify the actual potential
Identify the actual finite predictor residual with its L² class. Integrating its product with each actual lifted feature gives the Hilbert inner product; both factors are in L².
Corresponding Lean step
The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.
4. Produce the finite signed pairing
Integrate this same potential under each actual empirical law. Finite-sum cancellation and linearity give both the indexed update and the mean-displacement pairing.
Corresponding Lean step
The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.
5. Identify the exact scalar remainder
Apply the finite Hilbert replacement identity and identify both risk norms with their actual scalar losses. Push the squared predictor difference back to the true input marginal.
Corresponding Lean step
The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.
6. Obtain the uniform positive budget
The two actual lifted feature norms are at most b; their indexed average changes by at most2b/N. Square that derived estimate. The supplied positive b makes the shared budget coefficient strictly positive.
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 · joint_empirical_squared_risk_replacement
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.
theorem joint_empirical_squared_risk_replacement
{W X : Type*} [MeasurableSpace W] [MeasurableSingletonClass W]
[MeasurableSpace X] (P : Measure (X × ℝ)) [IsProbabilityMeasure P]
(K : W → X → ℝ) (b : ℝ) (hb : 0 < b)
(hfeature : ∀ q, MemLp (K q) 2 (P.map Prod.fst))
(hbound : ∀ q, ‖(hfeature q).toLp (K q)‖ ≤ b)
(hlabel : MemLp (fun z : X × ℝ => z.2) 2 P)
{N : ℕ} (hN : 0 < N) (w : Fin N → W) (i : Fin N) (u : W) :
let rho : Measure W := (N : ℝ≥0∞)⁻¹ • ∑ j, Measure.dirac (w j)
let rhoNew : Measure W :=
(N : ℝ≥0∞)⁻¹ • ∑ j, Measure.dirac (Function.update w i u j)
let predictor : Measure W → X → ℝ := fun law x => ∫ q, K q x ∂law
let risk : Measure W → ℝ :=
fun law => ∫ z, (predictor law z.1 - z.2) ^ 2 ∂P
let potential : W → ℝ :=
fun q => 2 * ∫ z, (predictor rho z.1 - z.2) * K q z.1 ∂P
let pairing : ℝ := (∫ q, potential q ∂rhoNew) - (∫ q, potential q ∂rho)
(0 < 4 * b ^ 2) ∧ IsProbabilityMeasure rho ∧ IsProbabilityMeasure rhoNew ∧
Integrable (fun z : X × ℝ => (predictor rho z.1 - z.2) ^ 2) P ∧
Integrable (fun z : X × ℝ => (predictor rhoNew z.1 - z.2) ^ 2) P ∧
Integrable potential rho ∧ Integrable potential rhoNew ∧
(pairing = (N : ℝ)⁻¹ * (potential u - potential (w i))) ∧
(risk rhoNew - risk rho - pairing =
∫ x, (predictor rhoNew x - predictor rho x) ^ 2 ∂(P.map Prod.fst)) ∧
(0 ≤ risk rhoNew - risk rho - pairing) ∧
(risk rhoNew - risk rho - pairing ≤ 4 * b ^ 2 / (N : ℝ) ^ 2) := by
classical
dsimp only
let rhoOf : (Fin N → W) → Measure W :=
fun cfg => (N : ℝ≥0∞)⁻¹ • ∑ j, Measure.dirac (cfg j)
let cfgNew := Function.update w i u
let predictor : Measure W → X → ℝ := fun law x => ∫ q, K q x ∂law
let risk : Measure W → ℝ := fun law => ∫ z, (predictor law z.1 - z.2) ^ 2 ∂P
let potential : W → ℝ :=
fun q => 2 * ∫ z, (predictor (rhoOf w) z.1 - z.2) * K q z.1 ∂P
let pairing : ℝ := (∫ q, potential q ∂rhoOf cfgNew) - (∫ q, potential q ∂rhoOf w)
change (0 < 4 * b ^ 2) ∧ IsProbabilityMeasure (rhoOf w) ∧
IsProbabilityMeasure (rhoOf cfgNew) ∧ _
have hmarg : MeasurePreserving (Prod.fst : X × ℝ → X) P (P.map Prod.fst) :=
measurable_fst.measurePreserving P
have hfeatureP (q : W) : MemLp (fun z : X × ℝ => K q z.1) 2 P :=
(hfeature q).comp_measurePreserving hmarg
let feature : W → Lp ℝ 2 P :=
fun q => (hfeatureP q).toLp (fun z : X × ℝ => K q z.1)
let label : Lp ℝ 2 P := hlabel.toLp (fun z : X × ℝ => z.2)
let mean : (Fin N → W) → Lp ℝ 2 P :=
fun cfg => (N : ℝ)⁻¹ • ∑ j, feature (cfg j)
have hfeatureClass (q : W) : feature q =
Lp.compMeasurePreserving Prod.fst hmarg ((hfeature q).toLp (K q)) := rfl
have hnorm (q : W) : ‖feature q‖ ≤ b := by
rw [hfeatureClass, Lp.norm_compMeasurePreserving]
exact hbound q
have hinv : (N : ℝ≥0∞)⁻¹ ≠ ∞ := by
apply ENNReal.inv_ne_top.mpr
exact_mod_cast hN.ne'
have hInt (cfg : Fin N → W) (g : W → ℝ) :
Integrable g (rhoOf cfg) := by
apply Integrable.smul_measure (c := (N : ℝ≥0∞)⁻¹) _ hinv
exact integrable_finsetSum_measure.mpr (fun j _ => integrable_dirac (by simp))
have hEval (cfg : Fin N → W) (g : W → ℝ) :
(∫ q, g q ∂rhoOf cfg) = (N : ℝ)⁻¹ * ∑ j, g (cfg j) := by
dsimp only [rhoOf]
rw [integral_smul_measure,
integral_finsetSum_measure (fun j _ => integrable_dirac (by simp))]
simp [smul_eq_mul]
have hPred (cfg : Fin N → W) (x : X) :
predictor (rhoOf cfg) x = (N : ℝ)⁻¹ * ∑ j, K (cfg j) x :=
hEval cfg (fun q => K q x)
have hBase (cfg : Fin N → W) :=
empirical_law_squared_risk_eq_L2_norm P hN cfg
(fun q z => K q z.1) (fun z => z.2) (fun j => hfeatureP (cfg j)) hlabel
have hRisk (cfg : Fin N → W) : risk (rhoOf cfg) = ‖mean cfg - label‖ ^ 2 := by
simpa only [risk, predictor, rhoOf, mean, feature, label] using (hBase cfg).2.2
have hMean (cfg : Fin N → W) :
(fun z => mean cfg z) =ᵐ[P] (fun z : X × ℝ => predictor (rhoOf cfg) z.1) := by
filter_upwards [Lp.coeFn_smul (N : ℝ)⁻¹ (∑ j, feature (cfg j)),
Lp.coeFn_fun_finsetSum Finset.univ (fun j => feature (cfg j)),
ae_all_iff.2 (fun j => (hfeatureP (cfg j)).coeFn_toLp)]
with z hsmul hsum hf
change (((N : ℝ)⁻¹ • ∑ j, feature (cfg j)) z) = _
simp only [Pi.smul_apply, smul_eq_mul] at hsmul
rw [hsmul, hsum, hPred]
congr 1
apply Finset.sum_congr rfl
intro j _
exact hf j
have hResidual : (fun z => (mean w - label) z) =ᵐ[P]
(fun z : X × ℝ => predictor (rhoOf w) z.1 - z.2) := by
filter_upwards [Lp.coeFn_sub (mean w) label, hMean w, hlabel.coeFn_toLp]
with z hsub hm hy
simp only [Pi.sub_apply] at hsub
rw [hsub, hm, hy]
have hPotential (q : W) : potential q = 2 * ⟪mean w - label, feature q⟫_ℝ := by
dsimp only [potential]
rw [L2.inner_def]
congr 1
apply integral_congr_ae
filter_upwards [hResidual, (hfeatureP q).coeFn_toLp] with z hr hq
change feature q z = K q z.1 at hq
simp only [Real.inner_apply, hr, hq]
have hPotMean (cfg : Fin N → W) :
(∫ q, potential q ∂rhoOf cfg) = 2 * ⟪mean w - label, mean cfg⟫_ℝ := by
rw [hEval]
simp_rw [hPotential]
dsimp only [mean]
rw [real_inner_smul_right, inner_sum, ← Finset.mul_sum]
ring
have hPair : pairing = 2 * ⟪mean w - label, mean cfgNew - mean w⟫_ℝ := by
dsimp only [pairing]
rw [hPotMean, hPotMean, inner_sub_right]
ring
have hUpdate : (fun j => feature (cfgNew j)) =
Function.update (fun j => feature (w j)) i (feature u) := by
funext j
by_cases hji : j = i
· subst j
simp [cfgNew]
· simp [cfgNew, Function.update_of_ne hji]
have hBudget := empirical_squared_loss_replacement hN
(fun j => feature (w j)) i (feature u) label b (hnorm (w i)) (hnorm u)
change (‖(N : ℝ)⁻¹ • ∑ j, Function.update (fun j => feature (w j)) i (feature u) j - label‖ ^ 2 -
‖mean w - label‖ ^ 2 -
2 * ⟪mean w - label,
(N : ℝ)⁻¹ • ∑ j, Function.update (fun j => feature (w j)) i (feature u) j - mean w⟫_ℝ =
‖(N : ℝ)⁻¹ • ∑ j, Function.update (fun j => feature (w j)) i (feature u) j - mean w‖ ^ 2) ∧ _ at hBudget
rw [← hUpdate] at hBudget
change (‖mean cfgNew - label‖ ^ 2 - ‖mean w - label‖ ^ 2 -
2 * ⟪mean w - label, mean cfgNew - mean w⟫_ℝ = ‖mean cfgNew - mean w‖ ^ 2) ∧
‖mean cfgNew - mean w‖ ^ 2 ≤ 4 * b ^ 2 / (N : ℝ) ^ 2 at hBudget
have hBre : risk (rhoOf cfgNew) - risk (rhoOf w) - pairing =
‖mean cfgNew - mean w‖ ^ 2 := by
rw [hRisk, hRisk, hPair]
exact hBudget.1
have hMeanDiff : (fun z => (mean cfgNew - mean w) z) =ᵐ[P]
(fun z : X × ℝ => predictor (rhoOf cfgNew) z.1 - predictor (rhoOf w) z.1) := by
filter_upwards [Lp.coeFn_sub (mean cfgNew) (mean w), hMean cfgNew, hMean w]
with z hsub hn hm
simp only [Pi.sub_apply] at hsub
rw [hsub, hn, hm]
have hPredLp (cfg : Fin N → W) : MemLp (predictor (rhoOf cfg)) 2 (P.map Prod.fst) := by
have havg := (memLp_finsetSum Finset.univ (fun j _ => hfeature (cfg j))).const_smul (N : ℝ)⁻¹
exact MemLp.ae_eq (Filter.Eventually.of_forall (fun x => (hPred cfg x).symm)) havg
have hDiffLp := (hPredLp cfgNew).sub (hPredLp w)
have hNormInt : ‖mean cfgNew - mean w‖ ^ 2 =
∫ x, (predictor (rhoOf cfgNew) x - predictor (rhoOf w) x) ^ 2 ∂(P.map Prod.fst) := by
rw [← real_inner_self_eq_norm_sq, L2.inner_def]
calc
(∫ z, ⟪(mean cfgNew - mean w) z, (mean cfgNew - mean w) z⟫_ℝ ∂P) =
∫ z : X × ℝ, (predictor (rhoOf cfgNew) z.1 - predictor (rhoOf w) z.1) ^ 2 ∂P := by
apply integral_congr_ae
filter_upwards [hMeanDiff] with z hz
simp only [Real.inner_apply, hz, pow_two]
_ = _ := (integral_map measurable_fst.aemeasurable hDiffLp.integrable_sq.aestronglyMeasurable).symm
have hPairUpdate : pairing = (N : ℝ)⁻¹ * (potential u - potential (w i)) := by
dsimp only [pairing]
rw [hEval, hEval, ← mul_sub, ← Finset.sum_sub_distrib, Finset.sum_eq_single i]
· simp [cfgNew]
· intro j _ hji
simp [cfgNew, Function.update_of_ne hji]
· simp
refine ⟨mul_pos (by norm_num) (sq_pos_of_pos hb), (hBase w).1, (hBase cfgNew).1,
(hBase w).2.1, (hBase cfgNew).2.1, hInt w potential, hInt cfgNew potential,
hPairUpdate, ?_, ?_, ?_⟩
· exact hBre.trans hNormInt
· rw [hBre]
exact sq_nonneg _
· rw [hBre]
exact hBudget.2
end AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRiskScope and omitted-condition boundaries
- The literal residual potential is identified on fixed finite empirical laws; no global first-variation interface on all probability laws is asserted.
- Sectionwise L² membership does not produce global parameter measurability or non-atomic/random-configuration averaging.
- Specific activation and data families must supply their actual uniform moments; no stochastic convergence or geometric derivative theorem is included.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.empirical_law_squared_risk_eq_L2_normAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.empirical_squared_loss_replacement
Mathlib API called (external library)
- Measurable.measurePreserving
- MemLp.comp_measurePreserving
- Lp.compMeasurePreserving
- Lp.norm_compMeasurePreserving
- L2.inner_def
- integral_map
- integrable_dirac
- Integrable.smul_measure
- integrable_finsetSum_measure
- MemLp.ae_eq
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.