Differentiating a quadratic risk along a probability segment
AutoSamplingTheory.TechnicalLemmas.Analysis.ProbabilitySegmentRisk.quadratic_feature_probability_segment · theorem · Teaching coverage
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.
Lean statement · quadratic_feature_probability_segment
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.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem 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 ν)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.
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.
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.
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.
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.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem 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.ProbabilitySegmentRiskScope 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
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.