One indexed replacement has an exact quadratic remainder
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.empirical_squared_loss_replacement · theorem · Teaching coverage
Mathematical statement
Let H be any real inner-product normed space, N>0, a:Fin N→H, i:Fin N, and u,y in H. Let b be any real number and assume ||a_i||≤b and ||u||≤b. Define m=N^{-1} sum_j a_j and mNew=N^{-1} sum_j Function.update(a,i,u)_j. Then ||mNew-y||²-||m-y||²-2 inner(m-y,mNew-m)=||mNew-m||², and this squared remainder is at most4b²/N². The mean displacement is derived, not assumed. No bound on y or the other features, completeness, or measure hypothesis is needed.
Lean statement · empirical_squared_loss_replacement
Let H be any real inner-product normed space, N>0, a:Fin N->H, i:Fin N, and u,y in H. Let b be any real number and assume ||a_i||<=b and ||u||<=b. Define m=N^{-1} sum_j a_j and mNew=N^{-1} sum_j Function.update(a,i,u)_j. Then ||mNew-y||²-||m-y||²-2 inner(m-y,mNew-m)=||mNew-m||², and this squared remainder is at most4b²/N². The mean displacement is derived, not assumed. No bound on y or the other features, completeness, or measure hypothesis is needed.
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 empirical_squared_loss_replacement
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
{N : ℕ} (hN : 0 < N) (feature : Fin N → H) (i : Fin N)
(replacement label : H) (b : ℝ)
(hold : ‖feature i‖ ≤ b) (hnew : ‖replacement‖ ≤ b) :
let m : H := (N : ℝ)⁻¹ • ∑ j, feature j
let mNew : H := (N : ℝ)⁻¹ • ∑ j, Function.update feature i replacement j
(‖mNew - label‖ ^ 2 - ‖m - label‖ ^ 2 -
2 * ⟪m - label, mNew - m⟫_ℝ = ‖mNew - m‖ ^ 2) ∧
‖mNew - m‖ ^ 2 ≤ 4 * b ^ 2 / (N : ℝ) ^ 2Proof roadmap
- 1Cancel exactly one index
In the difference of the two finite sums all j≠i terms cancel, including terms whose vector values equal a_i.
- 2Bound the actual displacement
The triangle inequality and the two individual norm bounds give a bound on the derived displacement.
- 3Expand the unhalved quadratic loss
Write mNew-y=(m-y)+Delta and use the real inner-product norm expansion. The exact cross term has factor2.
- 4Square the nonnegative norm bound
Both norms and 2b/N are nonnegative; squaring produces the stated constant.
Full assumptions and notation
All objects and hypotheses
- N>0; only the selected old feature and its replacement have norm at most b.
- Repeated feature values are allowed; Function.update changes one index. The two norm bounds imply b≥0.
Mathematical proof
1. Cancel exactly one index
In the difference of the two finite sums all j≠i terms cancel, including terms whose vector values equal a_i.
Corresponding Lean step
The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.
2. Bound the actual displacement
The triangle inequality and the two individual norm bounds give a bound on the derived displacement.
Corresponding Lean step
The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.
3. Expand the unhalved quadratic loss
Write mNew-y=(m-y)+Delta and use the real inner-product norm expansion. The exact cross term has factor2.
Corresponding Lean step
The exact statement and proof are extracted from the adjacent compiled module; the mathematical step is explained here.
4. Square the nonnegative norm bound
Both norms and 2b/N are nonnegative; squaring produces the stated constant.
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_loss_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 empirical_squared_loss_replacement
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
{N : ℕ} (hN : 0 < N) (feature : Fin N → H) (i : Fin N)
(replacement label : H) (b : ℝ)
(hold : ‖feature i‖ ≤ b) (hnew : ‖replacement‖ ≤ b) :
let m : H := (N : ℝ)⁻¹ • ∑ j, feature j
let mNew : H := (N : ℝ)⁻¹ • ∑ j, Function.update feature i replacement j
(‖mNew - label‖ ^ 2 - ‖m - label‖ ^ 2 -
2 * ⟪m - label, mNew - m⟫_ℝ = ‖mNew - m‖ ^ 2) ∧
‖mNew - m‖ ^ 2 ≤ 4 * b ^ 2 / (N : ℝ) ^ 2 := by
classical
dsimp only
let m : H := (N : ℝ)⁻¹ • ∑ j, feature j
let mNew : H := (N : ℝ)⁻¹ • ∑ j, Function.update feature i replacement j
change (‖mNew - label‖ ^ 2 - ‖m - label‖ ^ 2 -
2 * ⟪m - label, mNew - m⟫_ℝ = ‖mNew - m‖ ^ 2) ∧ _
have hsum : (∑ j, Function.update feature i replacement j) - ∑ j, feature j =
replacement - feature i := by
rw [← Finset.sum_sub_distrib, Finset.sum_eq_single i]
· simp
· intro j _ hji
simp [Function.update_of_ne hji]
· simp
have hmean : mNew - m = (N : ℝ)⁻¹ • (replacement - feature i) := by
dsimp only [mNew, m]
rw [← smul_sub, hsum]
have hb : 0 ≤ b := (norm_nonneg (feature i)).trans hold
have hinv : 0 ≤ (N : ℝ)⁻¹ := (inv_pos.mpr (show (0 : ℝ) < N by exact_mod_cast hN)).le
have hsmall : ‖mNew - m‖ ≤ (N : ℝ)⁻¹ * (2 * b) := by
rw [hmean, norm_smul, Real.norm_eq_abs, abs_of_nonneg hinv]
apply mul_le_mul_of_nonneg_left _ hinv
calc
‖replacement - feature i‖ ≤ ‖replacement‖ + ‖feature i‖ := norm_sub_le _ _
_ ≤ b + b := add_le_add hnew hold
_ = 2 * b := by ring
constructor
· have hsplit : mNew - label = (m - label) + (mNew - m) := by abel
rw [hsplit, norm_add_sq_real]
ring
· calc
‖mNew - m‖ ^ 2 ≤ ((N : ℝ)⁻¹ * (2 * b)) ^ 2 := by gcongr
_ = 4 * b ^ 2 / (N : ℝ) ^ 2 := by
simp only [div_eq_mul_inv]
ringScope and omitted-condition boundaries
- This Hilbert expression alone is not a measure-functional Bregman identity.
- At b=0 the estimate is valid but4b² is not a strictly positive witness.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- Finset.sum_sub_distrib
- Finset.sum_eq_single
- norm_sub_le
- norm_add_sq_real
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.