A finite empirical segment has the actual joint-risk derivative
AutoSamplingTheory.TechnicalLemmas.Analysis.JointEmpiricalSegmentRisk.joint_empirical_probability_segment_derivative · theorem · Teaching coverage
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.
Lean statement · joint_empirical_probability_segment_derivative
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.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem joint_empirical_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) 0Proof 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.
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).
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.
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.
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.
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.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem joint_empirical_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.JointEmpiricalSegmentRiskScope 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
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.