Optimisation · §12 · source p. 104

Stochastic optimization

Stable source-facing chapter environment inside the shared Samplinglib reader.

Partially formalizedsource mapFull source closure not claimed

Planned route

Source → theorem map → reusable Lean nodes

Source audit

Definitions, theorems, assumptions, proof route, and exact anchors.

Upstream alignment

Search Mathlib, Optlib, CvxLean, and shared Samplinglib interfaces; preserve the exact Chewi statement and use a small adapter when conventions differ.

Frontier Cells

Only genuinely missing mathematical edges become theorem-sized tasks.

Graph placement

Dependencies, consumers, cross-library bridges, and reusable shared interfaces.

Open exact Chewi source ↗

This page establishes a stable source route and truth boundary; it does not claim a completed formalization.

Library supplement: actual probability-law risk derivatives

An original reusable mathematics supplement placed by subject. It is not a theorem claim about the primary textbook or a complete stochastic/statistical model.

Samplinglib original mathematical supplement v1, 2026-10-20 · Complete authored units 0,1,4 and their formula proof steps in the immutable declaration lesson (historical source) · licensed original

Complete source statement (Samplinglib restatement)

The adjacent complete statements, assumptions and formula proofs describe the exact generic results; the optional Lean is initially folded.

E has finite-dimensional real inner-product and Borel structures. P is a true joint probability with standard Gaussian first marginal.
N>0. Only the two selected lists of feature slices are assumed to be in L²(Pₓ); global kernel measurability, a uniform feature bound, and nonsampled feature moments are not assumed.
W and X are measurable, and singletons in W are measurable. P is an actual joint probability; its response coordinate is in L²(P).
W is measurable; H is a complete real inner-product normed space.
p is any finite real polynomial, and the actual second-coordinate response belongs to L²(P). Input and response need not be independent.
μ and ν are probabilities. Φ is genuinely Bochner integrable under each; y is any vector in H.

Differentiating a quadratic risk along a probability segment

\[\left.\frac{d}{dt}R((1-t)\mu+t\nu)\right|_{0^+}=\int V\,d\nu-\int V\,d\mu,\qquad R(\nu)-R(\mu)-\left(\int V\,d\nu-\int V\,d\mu\right)=\|m(\nu)-m(\mu)\|^2.\]

A finite empirical segment has the actual joint-risk derivative

\[\rho_a=\frac1N\sum_{j=1}^N\delta_{w_a^j},\qquad \left.\frac d{dt}F((1-t)\rho_0+t\rho_1)\right|_{0^+}=\int V\,d\rho_1-\int V\,d\rho_0.\]

An actual Gaussian joint-data risk has a first variation

\[\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).\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Differentiating a quadratic risk along a probability segment

AutoSamplingTheory.TechnicalLemmas.Analysis.ProbabilitySegmentRisk.quadratic_feature_probability_segment · theorem · Teaching coverage

Read this first

Mathematical statement

Let μ and ν be probability measures on a measurable parameter space W. Let Φ map W to a real Hilbert space H and be Bochner integrable under both laws, and let y be a fixed vector in H. Write m(ρ)=∫Φ dρ, R(ρ)=‖m(ρ)−y‖², and V(w)=2⟨m(μ)−y,Φ(w)⟩. For every 0≤t≤1, the actual positive measure ρₜ=(1−t)μ+tν is a probability, Φ is integrable under ρₜ, and its mean is the affine interpolation of the endpoint means. V is integrable under both endpoint laws. The right derivative of R(ρₜ) at zero is ∫V dν−∫V dμ. The exact remainder R(ν)−R(μ)−(∫V dν−∫V dμ) is ‖m(ν)−m(μ)‖², and is therefore nonnegative.

\[\left.\frac{d}{dt}R((1-t)\mu+t\nu)\right|_{0^+}=\int V\,d\nu-\int V\,d\mu,\qquad R(\nu)-R(\mu)-\left(\int V\,d\nu-\int V\,d\mu\right)=\|m(\nu)-m(\mu)\|^2.\]

Lean statement · quadratic_feature_probability_segment

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 quadratic_feature_probability_segment
    {W H : Type*} [MeasurableSpace W]
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (μ ν : Measure W) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (feature : W → H) (label : H)
    (hμ : Integrable feature μ) (hν : Integrable feature ν) :
    let curve : ℝ → Measure W := fun t =>
      ENNReal.ofReal (1 - t) • μ + ENNReal.ofReal t • ν
    let mean : Measure W → H := fun law => ∫ w, feature w ∂law
    let risk : Measure W → ℝ := fun law => ‖mean law - label‖ ^ 2
    let potential : W → ℝ := fun w => 2 * ⟪mean μ - label, feature w⟫_ℝ
    (∀ t ∈ Set.Icc (0 : ℝ) 1,
      IsProbabilityMeasure (curve t) ∧ Integrable feature (curve t) ∧
      mean (curve t) = (1 - t) • mean μ + t • mean ν) ∧
    Integrable potential μ ∧ Integrable potential ν ∧
    HasDerivWithinAt (fun t => risk (curve t))
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ))
      (Set.Icc (0 : ℝ) 1) 0 ∧
    (risk ν - risk μ - ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) =
      ‖mean ν - mean μ‖ ^ 2) ∧
    (risk μ + ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) ≤ risk ν)

Exact module and namespace context

Proof roadmap

1Stay within probability measures
On the closed interval the two nonnegative coefficients add to one. Scaling and adding genuine integrable functions preserves integrability under the resulting measure.
2Integrate the affine segment
Linearity of the Bochner integral identifies the actual segment mean, without replacing the measure path by an unrelated vector path.
3Compute the potential pairing
The bounded linear functional defined by the fixed residual commutes with the integral. This also proves the two scalar potential integrals exist.
4Differentiate and retain the square remainder
Apply real Hilbert-space squared-norm calculus to the affine mean. Restrict its derivative to the probability interval; expand the square to obtain the nonnegative remainder.

Full assumptions and notation

All objects and hypotheses

W is measurable; H is a complete real inner-product normed space.
μ and ν are probabilities. Φ is genuinely Bochner integrable under each; y is any vector in H.

Mathematical proof

1. Stay within probability measures

On the closed interval the two nonnegative coefficients add to one. Scaling and adding genuine integrable functions preserves integrability under the resulting measure.

\[\rho_t(W)=(1-t)\mu(W)+t\nu(W)=1.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

2. Integrate the affine segment

Linearity of the Bochner integral identifies the actual segment mean, without replacing the measure path by an unrelated vector path.

\[m(\rho_t)=(1-t)m(\mu)+tm(\nu).\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

3. Compute the potential pairing

The bounded linear functional defined by the fixed residual commutes with the integral. This also proves the two scalar potential integrals exist.

\[\int V\,d\nu-\int V\,d\mu=2\langle m(\mu)-y,m(\nu)-m(\mu)\rangle.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

4. Differentiate and retain the square remainder

Apply real Hilbert-space squared-norm calculus to the affine mean. Restrict its derivative to the probability interval; expand the square to obtain the nonnegative remainder.

\[\|r+th\|^2=\|r\|^2+2t\langle r,h\rangle+t^2\|h\|^2.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

Lean verification

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

Lean proof · quadratic_feature_probability_segment

The formula proof above explains the mathematical moves; the adjacent folded Lean gives their exact implementation.

Download module (.lean)

theorem quadratic_feature_probability_segment
    {W H : Type*} [MeasurableSpace W]
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (μ ν : Measure W) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (feature : W → H) (label : H)
    (hμ : Integrable feature μ) (hν : Integrable feature ν) :
    let curve : ℝ → Measure W := fun t =>
      ENNReal.ofReal (1 - t) • μ + ENNReal.ofReal t • ν
    let mean : Measure W → H := fun law => ∫ w, feature w ∂law
    let risk : Measure W → ℝ := fun law => ‖mean law - label‖ ^ 2
    let potential : W → ℝ := fun w => 2 * ⟪mean μ - label, feature w⟫_ℝ
    (∀ t ∈ Set.Icc (0 : ℝ) 1,
      IsProbabilityMeasure (curve t) ∧ Integrable feature (curve t) ∧
      mean (curve t) = (1 - t) • mean μ + t • mean ν) ∧
    Integrable potential μ ∧ Integrable potential ν ∧
    HasDerivWithinAt (fun t => risk (curve t))
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ))
      (Set.Icc (0 : ℝ) 1) 0 ∧
    (risk ν - risk μ - ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) =
      ‖mean ν - mean μ‖ ^ 2) ∧
    (risk μ + ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) ≤ risk ν) := by
  dsimp only
  let curve : ℝ → Measure W := fun t =>
    ENNReal.ofReal (1 - t) • μ + ENNReal.ofReal t • ν
  let mean : Measure W → H := fun law => ∫ w, feature w ∂law
  let risk : Measure W → ℝ := fun law => ‖mean law - label‖ ^ 2
  let potential : W → ℝ := fun w => 2 * ⟪mean μ - label, feature w⟫_ℝ
  change (∀ t ∈ Set.Icc (0 : ℝ) 1,
    IsProbabilityMeasure (curve t) ∧ Integrable feature (curve t) ∧
    mean (curve t) = (1 - t) • mean μ + t • mean ν) ∧
    Integrable potential μ ∧ Integrable potential ν ∧
    HasDerivWithinAt (fun t => risk (curve t))
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) (Set.Icc (0 : ℝ) 1) 0 ∧
    (risk ν - risk μ - ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) =
      ‖mean ν - mean μ‖ ^ 2) ∧
    (risk μ + ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) ≤ risk ν)
  have hprops : ∀ t ∈ Set.Icc (0 : ℝ) 1,
      IsProbabilityMeasure (curve t) ∧ Integrable feature (curve t) ∧
      mean (curve t) = (1 - t) • mean μ + t • mean ν := by
    intro t ht
    have hleft : 0 ≤ 1 - t := sub_nonneg.mpr ht.2
    have hμt := hμ.smul_measure (c := ENNReal.ofReal (1 - t)) ENNReal.ofReal_ne_top
    have hνt := hν.smul_measure (c := ENNReal.ofReal t) ENNReal.ofReal_ne_top
    refine ⟨?_, hμt.add_measure hνt, ?_⟩
    · apply isProbabilityMeasure_iff.mpr
      simp only [curve, Measure.add_apply, Measure.smul_apply, measure_univ, smul_eq_mul,
        mul_one]
      rw [← ENNReal.ofReal_add hleft ht.1]
      norm_num
    · dsimp only [mean, curve]
      rw [integral_add_measure hμt hνt, integral_smul_measure, integral_smul_measure,
        ENNReal.toReal_ofReal hleft, ENNReal.toReal_ofReal ht.1]
  have hcalc := AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.quadratic_feature_mean_calculus
    μ ν feature label hμ hν
  dsimp only at hcalc
  rcases hcalc with ⟨hpotμ, hpotν, hpair, hbre, hsupport, hderiv⟩
  refine ⟨hprops, hpotμ, hpotν, ?_, hbre, hsupport⟩
  apply hderiv.hasDerivWithinAt.congr_of_mem
  · intro t ht
    change ‖mean (curve t) - label‖ ^ 2 = _
    rw [(hprops t ht).2.2]
    congr 2
    rw [sub_smul, one_smul, smul_sub]
    abel
  · exact ⟨le_rfl, zero_le_one⟩


end AutoSamplingTheory.TechnicalLemmas.Analysis.ProbabilitySegmentRisk

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Let μ and ν be probability measures on a measurable parameter space W. Let Φ map W to a real Hilbert space H and be Bochner integrable under both laws, and let y be a fixed vector in H. Write m(ρ)=∫Φ dρ, R(ρ)=‖m(ρ)−y‖², and V(w)=2⟨m(μ)−y,Φ(w)⟩. For every 0≤t≤1, the actual positive measure ρₜ=(1−t)μ+tν is a probability, Φ is integrable under ρₜ, and its mean is the affine interpolation of the endpoint means. V is integrable under both endpoint laws. The right derivative of R(ρₜ) at zero is ∫V dν−∫V dμ. The exact remainder R(ν)−R(μ)−(∫V dν−∫V dμ) is ‖m(ν)−m(μ)‖², and is therefore nonnegative.	The exact adjacent public signature preserves all displayed primitive structures and hypotheses, literal measures/functions, produced integrability and derivative scope.	same	Moments, radial domination, representative identities and Fubini are proved inside their respective producer nodes; none is added as a convenience premise.

This is a genuine probability-segment theorem for an H-valued feature mean. An actual scalar data-risk formula still requires a separate averaging identity.; The derivative is within [0,1] at zero. No two-sided derivative of the clipped positive-measure extension is asserted.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

This is a genuine probability-segment theorem for an H-valued feature mean. An actual scalar data-risk formula still requires a separate averaging identity.
The derivative is within [0,1] at zero. No two-sided derivative of the clipped positive-measure extension is asserted.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.quadratic_feature_mean_calculus

Mathlib API called (external library)

MeasureTheory.integral_add_measure
MeasureTheory.integral_smul_measure
HasDerivWithinAt.congr_of_mem

Mathematical sources

Samplinglib original probability and Gaussian feature regularity supplement v1 (2026-10-20) (historical source) — Original generic mathematical supplement from the cited pinned library prerequisites; no primary-textbook theorem or statistical convergence credit.

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

Samplinglib mathematical lesson

A finite empirical segment has the actual joint-risk derivative

AutoSamplingTheory.TechnicalLemmas.Analysis.JointEmpiricalSegmentRisk.joint_empirical_probability_segment_derivative · theorem · Teaching coverage

Read this first

Mathematical statement

Let P be a probability law on X×ℝ, with its actual input marginal Pₓ. Let K:W×X→ℝ be a scalar feature, and assume the actual response coordinate belongs to L²(P). Choose N>0 and two indexed parameter configurations w₀,w₁ of length N. Assume only their selected feature functions K(wₐʲ,·) belong to L²(Pₓ), for a=0,1 and every index j. Let ρ₀ and ρ₁ be their literal equally weighted Dirac empirical measures, retaining repeated indices. Define fρ(x)=∫K(w,x) dρ(w), F(ρ)=∫(fρ(x)−y)² dP(x,y), and V(w)=2∫(fρ₀(x)−y)K(w,x) dP(x,y). Every mixture (1−t)ρ₀+tρ₁ for 0≤t≤1 is a probability with integrable squared loss. V is integrable under both empirical laws, and the actual scalar risk along the mixture has right derivative ∫V dρ₁−∫V dρ₀ at zero.

\[\rho_a=\frac1N\sum_{j=1}^N\delta_{w_a^j},\qquad \left.\frac d{dt}F((1-t)\rho_0+t\rho_1)\right|_{0^+}=\int V\,d\rho_1-\int V\,d\rho_0.\]

Lean statement · joint_empirical_probability_segment_derivative

Download module (.lean)

theorem joint_empirical_probability_segment_derivative
    {W X : Type*} [MeasurableSpace W] [MeasurableSingletonClass W] [MeasurableSpace X]
    (P : Measure (X × ℝ)) [IsProbabilityMeasure P]
    (K : W → X → ℝ)
    (hlabel : MemLp (fun z : X × ℝ => z.2) 2 P)
    {N : ℕ} (hN : 0 < N) (w0 w1 : Fin N → W)
    (hfeature0 : ∀ j, MemLp (K (w0 j)) 2 (P.map Prod.fst))
    (hfeature1 : ∀ j, MemLp (K (w1 j)) 2 (P.map Prod.fst)) :
    let rho0 : Measure W := (N : ℝ≥0∞)⁻¹ • ∑ j, Measure.dirac (w0 j)
    let rho1 : Measure W := (N : ℝ≥0∞)⁻¹ • ∑ j, Measure.dirac (w1 j)
    let curve : ℝ → Measure W := fun t =>
      ENNReal.ofReal (1 - t) • rho0 + ENNReal.ofReal t • rho1
    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 rho0 z.1 - z.2) * K q z.1 ∂P
    (∀ t ∈ Set.Icc (0 : ℝ) 1,
      IsProbabilityMeasure (curve t) ∧
      Integrable (fun z : X × ℝ => (predictor (curve t) z.1 - z.2) ^ 2) P) ∧
    Integrable potential rho0 ∧ Integrable potential rho1 ∧
    HasDerivWithinAt (fun t => risk (curve t))
      ((∫ q, potential q ∂rho1) - (∫ q, potential q ∂rho0))
      (Set.Icc (0 : ℝ) 1) 0

Exact module and namespace context

Proof roadmap

1Use the actual finite support
Dirac integration turns the predictor into the indexed average. Colliding particles keep their multiplicity, and every scalar function is integrable under these finite empirical laws.
2Construct genuine joint L² classes
Pull each selected feature along the actual first-coordinate marginal. Finite sums and the supplied response class construct both endpoint means and their residual in L²(P).
3Identify the finite potential pairing
Cauchy–Schwarz gives integrability of every required sampled residual-feature product. Finite integration yields the actual potential pairing as twice the residual inner product with the mean change.
4Identify the scalar mixture risk
Linearity under the finite positive-measure mixture gives the actual predictor interpolation; its square is integrable and its integral equals the squared L² residual norm.
5Take the endpoint derivative
Differentiate this affine residual norm and restrict to the probability interval. Both finite outer potential integrals already exist.

Full assumptions and notation

All objects and hypotheses

W and X are measurable, and singletons in W are measurable. P is an actual joint probability; its response coordinate is in L²(P).
N>0. Only the two selected lists of feature slices are assumed to be in L²(Pₓ); global kernel measurability, a uniform feature bound, and nonsampled feature moments are not assumed.

Mathematical proof

1. Use the actual finite support

Dirac integration turns the predictor into the indexed average. Colliding particles keep their multiplicity, and every scalar function is integrable under these finite empirical laws.

\[f_{\rho_a}(x)=N^{-1}\sum_j K(w_a^j,x).\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

2. Construct genuine joint L² classes

Pull each selected feature along the actual first-coordinate marginal. Finite sums and the supplied response class construct both endpoint means and their residual in L²(P).

\[\|K(w,\cdot)\|_{L^2(P_X)}=\|K(w,X)\|_{L^2(P)}.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

3. Identify the finite potential pairing

Cauchy–Schwarz gives integrability of every required sampled residual-feature product. Finite integration yields the actual potential pairing as twice the residual inner product with the mean change.

\[\int V\,d\rho_1-\int V\,d\rho_0=2\langle m_0-Y,m_1-m_0\rangle_{L^2(P)}.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

4. Identify the scalar mixture risk

Linearity under the finite positive-measure mixture gives the actual predictor interpolation; its square is integrable and its integral equals the squared L² residual norm.

\[F((1-t)\rho_0+t\rho_1)=\|(1-t)m_0+tm_1-Y\|_{L^2(P)}^2.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

5. Take the endpoint derivative

Differentiate this affine residual norm and restrict to the probability interval. Both finite outer potential integrals already exist.

\[\left.\frac d{dt}\|m_0-Y+t(m_1-m_0)\|^2\right|_{0^+}=2\langle m_0-Y,m_1-m_0\rangle.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

Lean verification

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

Lean proof · joint_empirical_probability_segment_derivative

The formula proof above explains the mathematical moves; the adjacent folded Lean gives their exact implementation.

Download module (.lean)

theorem joint_empirical_probability_segment_derivative
    {W X : Type*} [MeasurableSpace W] [MeasurableSingletonClass W] [MeasurableSpace X]
    (P : Measure (X × ℝ)) [IsProbabilityMeasure P]
    (K : W → X → ℝ)
    (hlabel : MemLp (fun z : X × ℝ => z.2) 2 P)
    {N : ℕ} (hN : 0 < N) (w0 w1 : Fin N → W)
    (hfeature0 : ∀ j, MemLp (K (w0 j)) 2 (P.map Prod.fst))
    (hfeature1 : ∀ j, MemLp (K (w1 j)) 2 (P.map Prod.fst)) :
    let rho0 : Measure W := (N : ℝ≥0∞)⁻¹ • ∑ j, Measure.dirac (w0 j)
    let rho1 : Measure W := (N : ℝ≥0∞)⁻¹ • ∑ j, Measure.dirac (w1 j)
    let curve : ℝ → Measure W := fun t =>
      ENNReal.ofReal (1 - t) • rho0 + ENNReal.ofReal t • rho1
    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 rho0 z.1 - z.2) * K q z.1 ∂P
    (∀ t ∈ Set.Icc (0 : ℝ) 1,
      IsProbabilityMeasure (curve t) ∧
      Integrable (fun z : X × ℝ => (predictor (curve t) z.1 - z.2) ^ 2) P) ∧
    Integrable potential rho0 ∧ Integrable potential rho1 ∧
    HasDerivWithinAt (fun t => risk (curve t))
      ((∫ q, potential q ∂rho1) - (∫ q, potential q ∂rho0))
      (Set.Icc (0 : ℝ) 1) 0 := by
  classical
  dsimp only
  let rhoOf : (Fin N → W) → Measure W :=
    fun cfg => (N : ℝ≥0∞)⁻¹ • ∑ j, Measure.dirac (cfg j)
  let curve : ℝ → Measure W := fun t =>
    ENNReal.ofReal (1 - t) • rhoOf w0 + ENNReal.ofReal t • rhoOf w1
  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 w0) z.1 - z.2) * K q z.1 ∂P
  change (∀ t ∈ Set.Icc (0 : ℝ) 1,
      IsProbabilityMeasure (curve t) ∧
      Integrable (fun z : X × ℝ => (predictor (curve t) z.1 - z.2) ^ 2) P) ∧
    Integrable potential (rhoOf w0) ∧ Integrable potential (rhoOf w1) ∧
    HasDerivWithinAt (fun t => risk (curve t))
      ((∫ q, potential q ∂rhoOf w1) - (∫ q, potential q ∂rhoOf w0))
      (Set.Icc (0 : ℝ) 1) 0
  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 hmarg : MeasurePreserving (Prod.fst : X × ℝ → X) P (P.map Prod.fst) :=
    measurable_fst.measurePreserving P
  have hf0 (j : Fin N) : MemLp (fun z : X × ℝ => K (w0 j) z.1) 2 P :=
    (hfeature0 j).comp_measurePreserving hmarg
  have hf1 (j : Fin N) : MemLp (fun z : X × ℝ => K (w1 j) z.1) 2 P :=
    (hfeature1 j).comp_measurePreserving hmarg
  let mean (cfg : Fin N → W) (hf : ∀ j, MemLp (fun z : X × ℝ => K (cfg j) z.1) 2 P) :
      Lp ℝ 2 P := (N : ℝ)⁻¹ • ∑ j, (hf j).toLp (fun z => K (cfg j) z.1)
  let m0 : Lp ℝ 2 P := mean w0 hf0
  let m1 : Lp ℝ 2 P := mean w1 hf1
  let label : Lp ℝ 2 P := hlabel.toLp (fun z : X × ℝ => z.2)
  have hBase (cfg : Fin N → W) (hf : ∀ j, MemLp (fun z : X × ℝ => K (cfg j) z.1) 2 P) :=
    empirical_law_squared_risk_eq_L2_norm P hN cfg
      (fun q z => K q z.1) (fun z => z.2) hf hlabel
  have hMean (cfg : Fin N → W) (hf : ∀ j, MemLp (fun z : X × ℝ => K (cfg j) z.1) 2 P) :
      (fun z => mean cfg hf z) =ᵐ[P]
        (fun z : X × ℝ => predictor (rhoOf cfg) z.1) := by
    filter_upwards [Lp.coeFn_smul (N : ℝ)⁻¹ (∑ j, (hf j).toLp (fun z => K (cfg j) z.1)),
      Lp.coeFn_fun_finsetSum Finset.univ (fun j => (hf j).toLp (fun z => K (cfg j) z.1)),
      ae_all_iff.2 (fun j => (hf j).coeFn_toLp)] with z hsmul hsum hj
    change (((N : ℝ)⁻¹ • ∑ j, (hf j).toLp (fun z => K (cfg j) z.1)) z) = _
    simp only [Pi.smul_apply, smul_eq_mul] at hsmul
    rw [hsmul, hsum, hPred]
    congr 1
    exact Finset.sum_congr rfl (fun j _ => hj j)
  have hResidual : (fun z => (m0 - label) z) =ᵐ[P]
      (fun z : X × ℝ => predictor (rhoOf w0) z.1 - z.2) := by
    filter_upwards [Lp.coeFn_sub m0 label, hMean w0 hf0, hlabel.coeFn_toLp]
      with z hsub hm hy
    simp only [Pi.sub_apply] at hsub
    rw [hsub, hm, hy]
  have hPotMean (cfg : Fin N → W)
      (hf : ∀ j, MemLp (fun z : X × ℝ => K (cfg j) z.1) 2 P) :
      (∫ q, potential q ∂rhoOf cfg) = 2 * ⟪m0 - label, mean cfg hf⟫_ℝ := by
    have hpot (j : Fin N) : potential (cfg j) =
        2 * ⟪m0 - label, (hf j).toLp (fun z => K (cfg j) z.1)⟫_ℝ := by
      dsimp only [potential]
      rw [L2.inner_def]
      congr 1
      apply integral_congr_ae
      filter_upwards [hResidual, (hf j).coeFn_toLp] with z hr hj
      simp only [Real.inner_apply, hr, hj]
    rw [hEval]
    simp_rw [hpot]
    dsimp only [mean]
    rw [real_inner_smul_right, inner_sum, ← Finset.mul_sum]
    ring
  have hPair : ((∫ q, potential q ∂rhoOf w1) - (∫ q, potential q ∂rhoOf w0)) =
      2 * ⟪m0 - label, m1 - m0⟫_ℝ := by
    rw [hPotMean w1 hf1, hPotMean w0 hf0, inner_sub_right]
    dsimp only [m0, m1]
    ring
  have hCurvePred (t : ℝ) (ht : t ∈ Set.Icc (0 : ℝ) 1) (x : X) :
      predictor (curve t) x =
        (1 - t) * predictor (rhoOf w0) x + t * predictor (rhoOf w1) x := by
    dsimp only [predictor, curve]
    rw [integral_add_measure
      ((hInt w0 (fun q => K q x)).smul_measure ENNReal.ofReal_ne_top)
      ((hInt w1 (fun q => K q x)).smul_measure ENNReal.ofReal_ne_top)]
    simp only [integral_smul_measure, ENNReal.toReal_ofReal (sub_nonneg.mpr ht.2),
      ENNReal.toReal_ofReal ht.1, smul_eq_mul]
  have hPredLp (cfg : Fin N → W)
      (hf : ∀ j, MemLp (fun z : X × ℝ => K (cfg j) z.1) 2 P) :
      MemLp (fun z : X × ℝ => predictor (rhoOf cfg) z.1) 2 P := by
    have hs := (memLp_finsetSum Finset.univ (fun j _ => hf j)).const_smul (N : ℝ)⁻¹
    exact hs.ae_eq (Filter.Eventually.of_forall (fun z => (hPred cfg z.1).symm))
  have hMixLp (t : ℝ) (ht : t ∈ Set.Icc (0 : ℝ) 1) :
      MemLp (fun z : X × ℝ => predictor (curve t) z.1 - z.2) 2 P := by
    have hs := (((hPredLp w0 hf0).const_smul (1 - t)).add
      ((hPredLp w1 hf1).const_smul t)).sub hlabel
    exact hs.ae_eq (Filter.Eventually.of_forall (fun z => by
      change (1 - t) * predictor (rhoOf w0) z.1 +
        t * predictor (rhoOf w1) z.1 - z.2 = predictor (curve t) z.1 - z.2
      rw [hCurvePred t ht]))
  have hMixAE (t : ℝ) (ht : t ∈ Set.Icc (0 : ℝ) 1) :
      (fun z => ((1 - t) • m0 + t • m1 - label) z) =ᵐ[P]
        (fun z : X × ℝ => predictor (curve t) z.1 - z.2) := by
    filter_upwards [Lp.coeFn_sub ((1 - t) • m0 + t • m1) label,
      Lp.coeFn_add ((1 - t) • m0) (t • m1),
      Lp.coeFn_smul (1 - t) m0, Lp.coeFn_smul t m1,
      hMean w0 hf0, hMean w1 hf1, hlabel.coeFn_toLp]
      with z hsub hadd hsm0 hsm1 hm0 hm1 hy
    simp only [Pi.sub_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul] at hsub hadd hsm0 hsm1
    rw [hsub, hadd, hsm0, hsm1, hm0, hm1, hy, hCurvePred t ht]
  have hRiskCurve (t : ℝ) (ht : t ∈ Set.Icc (0 : ℝ) 1) :
      risk (curve t) = ‖(1 - t) • m0 + t • m1 - label‖ ^ 2 := by
    dsimp only [risk]
    rw [← real_inner_self_eq_norm_sq, L2.inner_def]
    symm
    apply integral_congr_ae
    filter_upwards [hMixAE t ht] with z hz
    simp only [Real.inner_apply, hz, pow_two]
  have hProps (t : ℝ) (ht : t ∈ Set.Icc (0 : ℝ) 1) :
      IsProbabilityMeasure (curve t) ∧
      Integrable (fun z : X × ℝ => (predictor (curve t) z.1 - z.2) ^ 2) P := by
    refine ⟨?_, (hMixLp t ht).integrable_sq⟩
    letI : IsProbabilityMeasure (rhoOf w0) := (hBase w0 hf0).1
    letI : IsProbabilityMeasure (rhoOf w1) := (hBase w1 hf1).1
    apply isProbabilityMeasure_iff.mpr
    simp only [curve, Measure.add_apply, Measure.smul_apply, measure_univ, smul_eq_mul, mul_one]
    rw [← ENNReal.ofReal_add (sub_nonneg.mpr ht.2) ht.1]
    norm_num
  refine ⟨hProps, hInt w0 potential, hInt w1 potential, ?_⟩
  rw [hPair]
  have hlin : HasDerivAt (fun t : ℝ => m0 + t • (m1 - m0) - label) (m1 - m0) 0 := by
    have hs : HasDerivAt (fun t : ℝ => t • (m1 - m0)) (m1 - m0) 0 := by
      simpa only [one_smul, id_eq] using (hasDerivAt_id (0 : ℝ)).smul_const (m1 - m0)
    exact (hs.const_add m0).sub_const label
  have hd : HasDerivAt (fun t : ℝ => ‖m0 + t • (m1 - m0) - label‖ ^ 2)
      (2 * ⟪m0 - label, m1 - m0⟫_ℝ) 0 := by
    simpa only [zero_smul, add_zero] using hlin.norm_sq
  apply hd.hasDerivWithinAt.congr_of_mem
  · intro t ht
    rw [hRiskCurve t ht]
    congr 2
    rw [sub_smul, one_smul, smul_sub]
    abel
  · exact ⟨le_rfl, zero_le_one⟩


end AutoSamplingTheory.TechnicalLemmas.Analysis.JointEmpiricalSegmentRisk

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Let P be a probability law on X×ℝ, with its actual input marginal Pₓ. Let K:W×X→ℝ be a scalar feature, and assume the actual response coordinate belongs to L²(P). Choose N>0 and two indexed parameter configurations w₀,w₁ of length N. Assume only their selected feature functions K(wₐʲ,·) belong to L²(Pₓ), for a=0,1 and every index j. Let ρ₀ and ρ₁ be their literal equally weighted Dirac empirical measures, retaining repeated indices. Define fρ(x)=∫K(w,x) dρ(w), F(ρ)=∫(fρ(x)−y)² dP(x,y), and V(w)=2∫(fρ₀(x)−y)K(w,x) dP(x,y). Every mixture (1−t)ρ₀+tρ₁ for 0≤t≤1 is a probability with integrable squared loss. V is integrable under both empirical laws, and the actual scalar risk along the mixture has right derivative ∫V dρ₁−∫V dρ₀ at zero.	The exact adjacent public signature preserves all displayed primitive structures and hypotheses, literal measures/functions, produced integrability and derivative scope.	same	Moments, radial domination, representative identities and Fubini are proved inside their respective producer nodes; none is added as a convenience premise.

No independence or product decomposition of P is used.; At parameters outside both finite supports the inner potential integral is only the totalized formula unless additional integrability is proved. This finite-law theorem does not assert an arbitrary-law global first variation.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

No independence or product decomposition of P is used.
At parameters outside both finite supports the inner potential integral is only the totalized formula unless additional integrability is proved. This finite-law theorem does not assert an arbitrary-law global first variation.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.empirical_law_squared_risk_eq_L2_norm

Mathlib API called (external library)

MeasureTheory.MemLp.comp_measurePreserving
MeasureTheory.integral_finsetSum_measure
HasDerivAt.norm_sq
HasDerivWithinAt.congr_of_mem

Mathematical sources

Samplinglib original probability and Gaussian feature regularity supplement v1 (2026-10-20) (historical source) — Original generic mathematical supplement from the cited pinned library prerequisites; no primary-textbook theorem or statistical convergence credit.

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

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

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

The exact statement and proof are available in the adjacent initially folded Lean.

2. Identify 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.

\[F(\rho)=\|m(\rho)-Y\|_{L^2(P)}^2<\infty.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

3. Identify 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.

\[V_{\rho_0}(w)=2\langle m(\rho_0)-Y,\Phi(w)\rangle_{L^2(P)}.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

4. Use 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.

\[m((1-t)\rho_0+t\rho_1)=(1-t)m(\rho_0)+tm(\rho_1).\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

5. Obtain 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.

\[F(\rho_1)-F(\rho_0)-\left(\int V_{\rho_0}\,d\rho_1-\int V_{\rho_0}\,d\rho_0\right)=\|m(\rho_1)-m(\rho_0)\|^2\ge0.\]

Corresponding Lean step

The exact statement and proof are available in the adjacent initially folded Lean.

Lean verification

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

Lean proof · gaussian_polynomial_joint_risk_first_variation

The formula proof above explains the mathematical moves; the adjacent folded Lean gives their exact implementation.

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 := by
  classical
  letI : CompleteSpace E := FiniteDimensional.complete ℝ E
  dsimp only
  let U := {w : E // ‖w‖ = 1}
  let K : U → E → ℝ := fun w x => p.eval ⟪w.1,x⟫_ℝ
  let predictor : Measure U → E → ℝ := fun rho x => ∫ w, K w 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) * K w z.1 ∂P
  change (∀ 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) * K w 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
  obtain ⟨hf,hcont,havg⟩ := AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging.gaussian_polynomial_parameter_average_L2 (E := E) p
  have hmarg : MeasurePreserving (Prod.fst : E × ℝ → E) P (stdGaussian E) :=
    ⟨measurable_fst,hGaussian⟩
  let T : Lp ℝ 2 (stdGaussian E) →L[ℝ] Lp ℝ 2 P :=
    (Lp.compMeasurePreservingₗᵢ ℝ Prod.fst hmarg).toContinuousLinearMap
  let hfP : ∀ w : U, MemLp (fun z : E × ℝ => K w z.1) 2 P :=
    fun w => (hf w).comp_measurePreserving hmarg
  let feature : U → Lp ℝ 2 P := fun w => (hfP w).toLp (fun z => K w z.1)
  let label : Lp ℝ 2 P := hlabel.toLp (fun z : E × ℝ => z.2)
  let mean : Measure U → Lp ℝ 2 P := fun rho => ∫ w, feature w ∂rho
  have hFint (rho : Measure U) (hrho : IsProbabilityMeasure rho) : Integrable feature rho := by
    have h := T.integrable_comp (havg rho hrho).2.1
    exact h
  have hMeanClass (rho : Measure U) (hrho : IsProbabilityMeasure rho) :
      ∃ hpred : MemLp (fun z : E × ℝ => predictor rho z.1) 2 P,
        hpred.toLp (fun z => predictor rho z.1) = mean rho := by
    obtain ⟨hscalar,hint,hmean,hident⟩ := havg rho hrho
    let hpred : MemLp (fun z : E × ℝ => predictor rho z.1) 2 P :=
      hmean.comp_measurePreserving hmarg
    refine ⟨hpred, ?_⟩
    calc
      hpred.toLp (fun z => predictor rho z.1) = T (hmean.toLp (predictor rho)) := rfl
      _ = T (∫ w, (hf w).toLp (K w) ∂rho) := congrArg T hident
      _ = mean rho := (T.integral_comp_comm hint).symm
  have hMeanAE (rho : Measure U) (hrho : IsProbabilityMeasure rho) :
      (fun z => mean rho z) =ᵐ[P] (fun z : E × ℝ => predictor rho z.1) := by
    obtain ⟨hpred,hident⟩ := hMeanClass rho hrho
    rw [← hident]
    exact hpred.coeFn_toLp
  have hResidual (rho : Measure U) (hrho : IsProbabilityMeasure rho) :
      (fun z => (mean rho-label) z) =ᵐ[P] (fun z : E × ℝ => predictor rho z.1-z.2) := by
    filter_upwards [Lp.coeFn_sub (mean rho) label, hMeanAE rho hrho,hlabel.coeFn_toLp]
      with z hsub hm hy
    simp only [Pi.sub_apply] at hsub
    rw [hsub,hm,hy]
  have hRisk (rho : Measure U) (hrho : IsProbabilityMeasure rho) :
      risk rho = ‖mean rho-label‖^2 := by
    rw [← real_inner_self_eq_norm_sq, L2.inner_def]
    apply integral_congr_ae
    filter_upwards [hResidual rho hrho] with z hz
    simp only [risk,Real.inner_apply,hz,pow_two]
  have hPot (rho : Measure U) (hrho : IsProbabilityMeasure rho) :
      potential rho = fun w => 2 * ⟪mean rho-label,feature w⟫_ℝ := by
    funext w
    change 2 * (∫ z, (predictor rho z.1-z.2) * K w z.1 ∂P) = _
    rw [L2.inner_def]
    congr 1
    apply integral_congr_ae
    filter_upwards [hResidual rho hrho,(hfP w).coeFn_toLp] with z hr hw
    change feature w z = K w z.1 at hw
    simp only [Real.inner_apply,hr,hw]
  refine ⟨?_,?_⟩
  · intro rho hrho
    obtain ⟨hpred,hident⟩ := hMeanClass rho hrho
    exact ⟨(hpred.sub hlabel).integrable_sq,fun w =>
      (hpred.sub hlabel).integrable_mul (hfP w)⟩
  · intro rho0 rho1 h0 h1
    letI : IsProbabilityMeasure rho0 := h0
    letI : IsProbabilityMeasure rho1 := h1
    dsimp only
    let curve : ℝ → Measure U := fun t => ENNReal.ofReal (1-t) • rho0 + ENNReal.ofReal t • rho1
    have hc := AutoSamplingTheory.TechnicalLemmas.Analysis.ProbabilitySegmentRisk.quadratic_feature_probability_segment
      rho0 rho1 feature label (hFint rho0 h0) (hFint rho1 h1)
    dsimp only at hc
    rcases hc with ⟨hprops,hpot0,hpot1,hderiv,hbre,hsupport⟩
    rw [hPot rho0 h0]
    refine ⟨hpot0,hpot1,?_,?_⟩
    · apply hderiv.congr_of_mem
      · intro t ht
        exact hRisk (curve t) (hprops t ht).1
      · exact ⟨le_rfl,zero_le_one⟩
    · rw [hRisk rho0 h0,hRisk rho1 h1]
      exact hsupport

end AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRisk

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
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ρ₀.	The exact adjacent public signature preserves all displayed primitive structures and hypotheses, literal measures/functions, produced integrability and derivative scope.	same	Moments, radial domination, representative identities and Fubini are proved inside their respective producer nodes; none is added as a convenience premise.

The potential is a constructed canonical first-variation representative. No pointwise identification with an unspecified preselected first variation is asserted.; The derivative is within the probability interval. Spatial gradient bounds, Wasserstein regularity, stochastic dynamics and statistical convergence are separate results.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

The potential is a constructed canonical first-variation representative. No pointwise identification with an unspecified preselected first variation is asserted.
The derivative is within the probability interval. Spatial gradient bounds, Wasserstein regularity, stochastic dynamics and statistical convergence are separate results.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Lp.compMeasurePreservingₗᵢ
ContinuousLinearMap.integral_comp_comm
MeasureTheory.MemLp.comp_measurePreserving
MeasureTheory.MemLp.integrable_mul
MeasureTheory.L2.inner_def
HasDerivWithinAt.congr_of_mem

Mathematical sources

Samplinglib original probability and Gaussian feature regularity supplement v1 (2026-10-20) (historical source) — Original generic mathematical supplement from the cited pinned library prerequisites; no primary-textbook theorem or statistical convergence credit.

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

Which proof obligations and prerequisites are covered?

Formalized proof edge; source adapter/review separate Differentiating a quadratic risk along a probability segment
Formalized proof edge; source adapter/review separate A finite empirical segment has the actual joint-risk derivative
Formalized proof edge; source adapter/review separate An actual Gaussian joint-data risk has a first variation

Library supplement: quadratic feature risks and empirical replacement

Samplinglib-authored background development attached by topic to stochastic optimization. These six generic results are not claimed as theorems from the primary lecture notes or as a stochastic convergence theorem.

Samplinglib original mathematical supplement v1, 2026-10-20 · Six interfaces: moving features, finite L2 residuals, empirical laws, indexed remainders, Bochner means and true joint data (historical source) · licensed original

Complete source statement (Samplinglib restatement)

The six complete adjacent statements develop squared-loss calculus from genuine feature derivatives and integrability, identify actual finite empirical risks with L2 norms, derive one-index quadratic replacement budgets, and distinguish arbitrary-law Bochner-mean calculus from finite joint-data scalar integration. All assumptions and endpoint conventions are stated per theorem.

Each interface uses exactly its adjacent complete assumptions; they are separate theorems, not one conjunction of all hypotheses.
Squared losses are unhalved; finite empirical probability laws require N>0.
The joint-data theorem uses P and its true input marginal, with explicit actual feature and label L2 membership.

quadratic remainder

\[\|m+\Delta-y\|^2-\|m-y\|^2-2\langle m-y,\Delta\rangle=\|\Delta\|^2.\]

actual indexed empirical budget

\[F(\rho^{\rm new})-F(\rho)-\left(\int Vd\rho^{\rm new}-\int Vd\rho\right)=\|f_{\rho^{\rm new}}-f_\rho\|_{L^2(P_X)}^2\le4b^2/N^2.\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Differentiate a moving feature and scale the risk

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

Read this first

Mathematical statement

Let H be a real inner-product normed space, with no completeness assumption. Let N be a positive natural number, lambda any real number, phi:R->H, and a,y,v in H. At a real time t assume the genuine derivative of phi is v. Then s↦||(a+phi(s))/N-y||² has derivative (2/N) inner((a+phi(t))/N-y,v) at t. Multiplying that risk by N/lambda gives derivative (2/lambda) times the same inner product. All divisions are real totalized divisions; lambda=0 is an algebraic zero-scaling case, not a temperature model.

\[R(s)=\|N^{-1}(a+\phi(s))-y\|^2,\quad R\prime(t)=\frac2N\langle N^{-1}(a+\phi(t))-y,v\rangle,\quad (NR/\lambda)\prime(t)=\frac2\lambda\langle N^{-1}(a+\phi(t))-y,v\rangle.\]

Lean statement · empirical_squared_feature_risk_derivatives

Download module (.lean)

theorem empirical_squared_feature_risk_derivatives
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    {N : ℕ} (hN : 0 < N) (lambda : ℝ)
    {phi : ℝ → H} {v a y : H} {t : ℝ} (hphi : HasDerivAt phi v t) :
    HasDerivAt (fun s => ‖(N : ℝ)⁻¹ • (a + phi s) - y‖ ^ 2)
      ((2 / (N : ℝ)) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) t ∧
    HasDerivAt (fun s => ((N : ℝ) / lambda) * ‖(N : ℝ)⁻¹ • (a + phi s) - y‖ ^ 2)
      ((2 / lambda) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) t

Exact module and namespace context

Proof roadmap

1Differentiate the actual mean
The derivative of N^{-1}(a+phi(s))-y is N^{-1}v; translations by fixed vectors contribute zero.
2Differentiate the squared norm
Apply the real Hilbert squared-norm chain rule to this residual, yielding its inner product with the derived derivative.
3Cancel the genuine nonzero particle count
Multiply by N/lambda and use N>0 to cancel N. This does not require lambda to be nonzero; totalized zero scaling remains valid.

Full assumptions and notation

All objects and hypotheses

N>0; phi has actual scalar-parameter derivative v at t.
H is a real inner-product normed space; a and y are fixed arbitrary vectors; lambda is any real number.

Mathematical proof

1. Differentiate the actual mean

The derivative of N^{-1}(a+phi(s))-y is N^{-1}v; translations by fixed vectors contribute zero.

\[\frac{d}{ds}(N^{-1}(a+\phi(s))-y)_{s=t}=N^{-1}v.\]

Corresponding Lean step

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

2. Differentiate the squared norm

Apply the real Hilbert squared-norm chain rule to this residual, yielding its inner product with the derived derivative.

\[R\prime(t)=2\langle N^{-1}(a+\phi(t))-y,N^{-1}v\rangle.\]

Corresponding Lean step

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

3. Cancel the genuine nonzero particle count

Multiply by N/lambda and use N>0 to cancel N. This does not require lambda to be nonzero; totalized zero scaling remains valid.

\[\frac N\lambda\frac2N=\frac2\lambda.\]

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_feature_risk_derivatives

See the adjacent exact Lean and the mathematical proof steps.

Download module (.lean)

theorem empirical_squared_feature_risk_derivatives
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    {N : ℕ} (hN : 0 < N) (lambda : ℝ)
    {phi : ℝ → H} {v a y : H} {t : ℝ} (hphi : HasDerivAt phi v t) :
    HasDerivAt (fun s => ‖(N : ℝ)⁻¹ • (a + phi s) - y‖ ^ 2)
      ((2 / (N : ℝ)) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) t ∧
    HasDerivAt (fun s => ((N : ℝ) / lambda) * ‖(N : ℝ)⁻¹ • (a + phi s) - y‖ ^ 2)
      ((2 / lambda) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) t := by
  have hNr : (N : ℝ) ≠ 0 := by exact_mod_cast hN.ne'
  have hsum : HasDerivAt (fun s => a + phi s) v t := hphi.const_add a
  have hmean : HasDerivAt (fun s => (N : ℝ)⁻¹ • (a + phi s)) ((N : ℝ)⁻¹ • v) t :=
    HasDerivAt.const_smul (N : ℝ)⁻¹ hsum
  have hcurve : HasDerivAt (fun s => (N : ℝ)⁻¹ • (a + phi s) - y) ((N : ℝ)⁻¹ • v) t :=
    hmean.sub_const y
  have hsq : HasDerivAt (fun s => ‖(N : ℝ)⁻¹ • (a + phi s) - y‖ ^ 2)
      ((2 / (N : ℝ)) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) t := by
    simpa only [real_inner_smul_right, div_eq_mul_inv, mul_assoc] using hcurve.norm_sq
  have hcancel : ((N : ℝ) / lambda) *
        ((2 / (N : ℝ)) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) =
      (2 / lambda) * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ := by
    simp only [div_eq_mul_inv]
    calc
      (N : ℝ) * lambda⁻¹ * (2 * (N : ℝ)⁻¹ * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) =
          ((N : ℝ) * (N : ℝ)⁻¹) *
            (2 * lambda⁻¹ * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ) := by ring
      _ = 2 * lambda⁻¹ * ⟪(N : ℝ)⁻¹ • (a + phi t) - y, v⟫_ℝ := by
        rw [mul_inv_cancel₀ hNr, one_mul]
  have hscaled := HasDerivAt.const_mul ((N : ℝ) / lambda) hsq
  rw [hcancel] at hscaled
  exact ⟨hsq, hscaled⟩

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Let H be a real inner-product normed space, with no completeness assumption. Let N be a positive natural number, lambda any real number, phi:R->H, and a,y,v in H. At a real time t assume the genuine derivative of phi is v. Then s↦\|\|(a+phi(s))/N-y\|\|² has derivative (2/N) inner((a+phi(t))/N-y,v) at t. Multiplying that risk by N/lambda gives derivative (2/lambda) times the same inner product. All divisions are real totalized divisions; lambda=0 is an algebraic zero-scaling case, not a temperature model.	The exact adjacent Lean signature states these same objects, domains and primitive inputs.	same	The supplement is a generic mathematical library development; no textbook stochastic-algorithm theorem is identified with it.
Each displayed scalar integral and norm uses its indicated measure and representative.	N>0; phi has actual scalar-parameter derivative v at t.; H is a real inner-product normed space; a and y are fixed arbitrary vectors; lambda is any real number.	source-implicit	Measurability, L2 representatives, normalization, positivity and totalized endpoints are explicit in the complete statement and proof.

No actual parameter-feature differentiability is constructed.; The algebraic lambda=0 case is not a statistical or dynamical interpretation.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

No actual parameter-feature differentiability is constructed.
The algebraic lambda=0 case is not a statistical or dynamical interpretation.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

HasDerivAt.const_smul
HasDerivAt.norm_sq
HasDerivAt.const_mul
mul_inv_cancel₀

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.

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

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

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
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.	The exact adjacent Lean signature states these same objects, domains and primitive inputs.	same	The supplement is a generic mathematical library development; no textbook stochastic-algorithm theorem is identified with it.
Each displayed scalar integral and norm uses its indicated measure and representative.	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.	source-implicit	Measurability, L2 representatives, normalization, positivity and totalized endpoints are explicit in the complete statement and proof.

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

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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.

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

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

1Normalize the actual finite measure
The sum of N Dirac masses has total mass N. Its nonzero finite reciprocal weight gives total mass one.
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.
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.

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

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
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.	The exact adjacent Lean signature states these same objects, domains and primitive inputs.	same	The supplement is a generic mathematical library development; no textbook stochastic-algorithm theorem is identified with it.
Each displayed scalar integral and norm uses its indicated measure and representative.	N>0; W has measurable singleton points.; Every selected feature K(w_j) and y is in L²(P); repeated atoms are allowed.	source-implicit	Measurability, L2 representatives, normalization, positivity and totalized endpoints are explicit in the complete statement and proof.

Fixed finite atomic laws only; no arbitrary parameter-law integration or parameter measurability is inferred.; No general first variation is identified.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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

AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.empirical_squared_risk_eq_L2_norm

Mathlib API called (external library)

ENNReal.inv_mul_cancel
integral_smul_measure
integral_finsetSum_measure
integrable_dirac

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.

Samplinglib mathematical lesson

One indexed replacement has an exact quadratic remainder

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

Read this first

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.

\[\Delta=m^{\rm new}-m=\frac{u-a_i}{N},\quad \|m^{\rm new}-y\|^2-\|m-y\|^2-2\langle m-y,\Delta\rangle=\|\Delta\|^2\le\frac{4b^2}{N^2}.\]

Lean statement · empirical_squared_loss_replacement

Download module (.lean)

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

Exact module and namespace context

Proof 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.

\[\Delta=N^{-1}(u-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.

\[\|\Delta\|\le N^{-1}(\|u\|+\|a_i\|)\le2b/N.\]

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.

\[\|r+\Delta\|^2=\|r\|^2+2\langle r,\Delta\rangle+\|\Delta\|^2.\]

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.

\[\|\Delta\|^2\le4b^2/N^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_squared_loss_replacement

See the adjacent exact Lean and the mathematical proof steps.

Download module (.lean)

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]
        ring

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
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.	The exact adjacent Lean signature states these same objects, domains and primitive inputs.	same	The supplement is a generic mathematical library development; no textbook stochastic-algorithm theorem is identified with it.
Each displayed scalar integral and norm uses its indicated measure and representative.	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.	source-implicit	Measurability, L2 representatives, normalization, positivity and totalized endpoints are explicit in the complete statement and proof.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope 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.

Samplinglib mathematical lesson

Integrate the quadratic potential before taking the remainder

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

Read this first

Mathematical statement

Let W be measurable and H a complete real inner-product space. Let mu and nu be arbitrary measures, feature:W->H Bochner integrable under each, and y in H. Put m=integral feature dmu, n=integral feature dnu and V(q)=2 inner(m-y,feature(q)). Then V is integrable under both measures. With D=integral V dnu-integral V dmu, one has D=2 inner(m-y,n-m), ||n-y||²-||m-y||²-D=||n-m||², and ||m-y||²+D<=||n-y||². The real function t↦||m+t(n-m)-y||² has derivative D at zero. No probability, finite-mass or equal-mass hypothesis is imposed: m and n are unnormalized integrals.

\[D=\int Vd\nu-\int Vd\mu=2\langle m-y,n-m\rangle,\qquad \|n-y\|^2-\|m-y\|^2-D=\|n-m\|^2.\]

Lean statement · quadratic_feature_mean_calculus

Download module (.lean)

theorem quadratic_feature_mean_calculus
    {W H : Type*} [MeasurableSpace W]
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (μ ν : Measure W) (feature : W → H) (label : H)
    (hμ : Integrable feature μ) (hν : Integrable feature ν) :
    let m : H := ∫ w, feature w ∂μ
    let n : H := ∫ w, feature w ∂ν
    let potential : W → ℝ := fun w => 2 * ⟪m - label, feature w⟫_ℝ
    Integrable potential μ ∧ Integrable potential ν ∧
    ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ) =
      2 * ⟪m - label, n - m⟫_ℝ) ∧
    (‖n - label‖ ^ 2 - ‖m - label‖ ^ 2 -
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) = ‖n - m‖ ^ 2) ∧
    (‖m - label‖ ^ 2 + ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) ≤
      ‖n - label‖ ^ 2) ∧
    HasDerivAt (fun t : ℝ => ‖m + t • (n - m) - label‖ ^ 2)
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) 0

Exact module and namespace context

Proof roadmap

1Produce scalar potential integrability
Pairing the actual feature with a fixed Hilbert vector is a continuous linear functional. It preserves Bochner integrability under either measure.
2Commute each integral with the linear pairing
Subtract the two actual finite scalar integrals and use linearity in the second inner-product argument. Here eta is restricted to mu or nu, precisely the two supplied integrability domains.
3Expand the loss and use positivity
Expand n-y=(m-y)+(n-m); the leftover squared norm is nonnegative and yields the support inequality.
4Differentiate the literal affine Hilbert curve
Its residual derivative is n-m. The squared-norm chain rule gives precisely D at zero.

Full assumptions and notation

All objects and hypotheses

H is complete; the H-valued feature is genuinely Bochner integrable under both measures.
The fixed label is any vector. The measures may have unequal or infinite total mass.

Mathematical proof

1. Produce scalar potential integrability

Pairing the actual feature with a fixed Hilbert vector is a continuous linear functional. It preserves Bochner integrability under either measure.

\[V(q)=2\langle m-y,\Phi(q)\rangle\in L^1(\mu)\cap L^1(\nu).\]

Corresponding Lean step

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

2. Commute each integral with the linear pairing

Subtract the two actual finite scalar integrals and use linearity in the second inner-product argument. Here eta is restricted to mu or nu, precisely the two supplied integrability domains.

\[\eta\in\{\mu,\nu\}:\quad\int Vd\eta=2\langle m-y,\int\Phi d\eta\rangle,\qquad D=2\langle m-y,n-m\rangle.\]

Corresponding Lean step

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

3. Expand the loss and use positivity

Expand n-y=(m-y)+(n-m); the leftover squared norm is nonnegative and yields the support inequality.

\[\|n-y\|^2=\|m-y\|^2+D+\|n-m\|^2.\]

Corresponding Lean step

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

4. Differentiate the literal affine Hilbert curve

Its residual derivative is n-m. The squared-norm chain rule gives precisely D at zero.

\[\frac d{dt}\|m+t(n-m)-y\|^2\big|_{t=0}=D.\]

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 · quadratic_feature_mean_calculus

See the adjacent exact Lean and the mathematical proof steps.

Download module (.lean)

theorem quadratic_feature_mean_calculus
    {W H : Type*} [MeasurableSpace W]
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (μ ν : Measure W) (feature : W → H) (label : H)
    (hμ : Integrable feature μ) (hν : Integrable feature ν) :
    let m : H := ∫ w, feature w ∂μ
    let n : H := ∫ w, feature w ∂ν
    let potential : W → ℝ := fun w => 2 * ⟪m - label, feature w⟫_ℝ
    Integrable potential μ ∧ Integrable potential ν ∧
    ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ) =
      2 * ⟪m - label, n - m⟫_ℝ) ∧
    (‖n - label‖ ^ 2 - ‖m - label‖ ^ 2 -
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) = ‖n - m‖ ^ 2) ∧
    (‖m - label‖ ^ 2 + ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) ≤
      ‖n - label‖ ^ 2) ∧
    HasDerivAt (fun t : ℝ => ‖m + t • (n - m) - label‖ ^ 2)
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) 0 := by
  dsimp only
  let m : H := ∫ w, feature w ∂μ
  let n : H := ∫ w, feature w ∂ν
  let potential : W → ℝ := fun w => 2 * ⟪m - label, feature w⟫_ℝ
  change Integrable potential μ ∧ Integrable potential ν ∧ _
  have hpotμ : Integrable potential μ :=
    (Integrable.const_inner (m - label) hμ).const_mul 2
  have hpotν : Integrable potential ν :=
    (Integrable.const_inner (m - label) hν).const_mul 2
  have hpμ : (∫ w, potential w ∂μ) = 2 * ⟪m - label, m⟫_ℝ := by
    dsimp only [potential, m]
    rw [integral_const_mul, integral_inner hμ]
  have hpν : (∫ w, potential w ∂ν) = 2 * ⟪m - label, n⟫_ℝ := by
    dsimp only [potential, n]
    rw [integral_const_mul, integral_inner hν]
  have hpair : (∫ w, potential w ∂ν) - (∫ w, potential w ∂μ) =
      2 * ⟪m - label, n - m⟫_ℝ := by
    rw [hpν, hpμ, inner_sub_right]
    ring
  have hbre : ‖n - label‖ ^ 2 - ‖m - label‖ ^ 2 -
      ((∫ w, potential w ∂ν) - (∫ w, potential w ∂μ)) = ‖n - m‖ ^ 2 := by
    rw [hpair]
    have hsplit : n - label = (m - label) + (n - m) := by abel
    rw [hsplit, norm_add_sq_real]
    ring
  refine ⟨hpotμ, hpotν, hpair, hbre, ?_, ?_⟩
  · linarith [sq_nonneg ‖n - m‖]
  · rw [hpair]
    have hcurve : HasDerivAt (fun t : ℝ => m + t • (n - m) - label) (n - m) 0 := by
      have hsmul : HasDerivAt (fun t : ℝ => t • (n - m)) (n - m) 0 := by
        simpa only [one_smul, id_eq] using (hasDerivAt_id (0 : ℝ)).smul_const (n - m)
      have hadd : HasDerivAt (fun t : ℝ => m + t • (n - m)) (n - m) 0 :=
        hsmul.const_add m
      exact hadd.sub_const label
    simpa only [zero_smul, add_zero] using hcurve.norm_sq

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Let W be measurable and H a complete real inner-product space. Let mu and nu be arbitrary measures, feature:W->H Bochner integrable under each, and y in H. Put m=integral feature dmu, n=integral feature dnu and V(q)=2 inner(m-y,feature(q)). Then V is integrable under both measures. With D=integral V dnu-integral V dmu, one has D=2 inner(m-y,n-m), \|\|n-y\|\|²-\|\|m-y\|\|²-D=\|\|n-m\|\|², and \|\|m-y\|\|²+D<=\|\|n-y\|\|². The real function t↦\|\|m+t(n-m)-y\|\|² has derivative D at zero. No probability, finite-mass or equal-mass hypothesis is imposed: m and n are unnormalized integrals.	The exact adjacent Lean signature states these same objects, domains and primitive inputs.	same	The supplement is a generic mathematical library development; no textbook stochastic-algorithm theorem is identified with it.
Each displayed scalar integral and norm uses its indicated measure and representative.	H is complete; the H-valued feature is genuinely Bochner integrable under both measures.; The fixed label is any vector. The measures may have unequal or infinite total mass.	source-implicit	Measurability, L2 representatives, normalization, positivity and totalized endpoints are explicit in the complete statement and proof.

No identification of a pointwise statistical predictor with this Bochner mean is supplied.; The affine Hilbert derivative is not by itself a probability-measure-segment first variation.; For arbitrary measures, adding a constant to V need not preserve D.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

No identification of a pointwise statistical predictor with this Bochner mean is supplied.
The affine Hilbert derivative is not by itself a probability-measure-segment first variation.
For arbitrary measures, adding a constant to V need not preserve D.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Integrable.const_inner
Integrable.const_mul
integral_const_mul
integral_inner
inner_sub_right
norm_add_sq_real
HasDerivAt.norm_sq

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.

Samplinglib mathematical lesson

A true joint-data risk has a positive empirical replacement budget

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

Read this first

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.

\[D=\frac{V(u)-V(w_i)}N,\quad F(\rho^{\rm new})-F(\rho)-D=\int(f_{\rho^{\rm new}}-f_\rho)^2dP_X\in[0,4b^2/N^2],\quad4b^2>0.\]

Lean statement · joint_empirical_squared_risk_replacement

Download module (.lean)

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)

Exact module and namespace context

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.

\[\rho=N^{-1}\sum_j\delta_{w_j},\quad f_\rho(x)=N^{-1}\sum_jK(w_j,x).\]

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².

\[\|[K(q)\circ\mathrm{fst}]\|_{L^2(P)}=\|[K(q)]\|_{L^2(P_X)}\le b.\]

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².

\[V(q)=2\langle m-y,[K(q)\circ\mathrm{fst}]\rangle_{L^2(P)}.\]

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.

\[D=(V(u)-V(w_i))/N=2\langle m-y,m^{\rm new}-m\rangle.\]

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.

\[F(\rho^{\rm new})-F(\rho)-D=\|m^{\rm new}-m\|_{L^2(P)}^2=\int(f_{\rho^{\rm new}}-f_\rho)^2dP_X.\]

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.

\[\|m^{\rm new}-m\|\le2b/N,\quad0\le F(\rho^{\rm new})-F(\rho)-D\le4b^2/N^2,\quad4b^2>0.\]

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.

Download module (.lean)

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.QuadraticFeatureRisk

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
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.	The exact adjacent Lean signature states these same objects, domains and primitive inputs.	same	The supplement is a generic mathematical library development; no textbook stochastic-algorithm theorem is identified with it.
Each displayed scalar integral and norm uses its indicated measure and representative.	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.	source-implicit	Measurability, L2 representatives, normalization, positivity and totalized endpoints are explicit in the complete statement and proof.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope 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

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.

Which proof obligations and prerequisites are covered?

Formalized proof edge; source adapter/review separate Differentiate a moving feature and scale the risk
Formalized proof edge; source adapter/review separate A literal finite-average risk equals its L² norm
Formalized proof edge; source adapter/review separate Construct the empirical law and evaluate its actual risk
Formalized proof edge; source adapter/review separate One indexed replacement has an exact quadratic remainder
Formalized proof edge; source adapter/review separate Integrate the quadratic potential before taking the remainder
Formalized proof edge; source adapter/review separate A true joint-data risk has a positive empirical replacement budget