Stat.Nonparametric.MomentProblems.ScoreProgram
Dual score-program tools for moment problems: projection residual functions, feasible score directions, quadratic objectives, and minimum-norm identities.
ScoreProgram 4 core · 3 supporting This file solves the optimization problem that uses the projection residual from the neighboring ProjectionResidual.lean file. ★ scoreCost_eq
Constrained quadratic score program dual to the L² projection residual
This file solves the optimization problem that uses the projection residual from the neighboring
ProjectionResidual.lean file. For a probability measure μ on ℝ with finite fourth moment and
positive variance, consider the constrained minimum-norm score program: among all scores
s ∈ L²(μ) that are moment-orthogonal to 1 and y and carry a prescribed y²-moment x,
minimize ∫ s² dμ subject to ∫ s dμ = 0, ∫ y·s dμ = 0, ∫ y²·s dμ = x,
what is the least achievable L²(μ) norm² of s?
The answer is the duality identity
scoreCost μ x = x² / r, where r = l2ResidualQuadratic μ
is the (positive) L² residual of regressing y² on span{1, y} (ProjectionResidual.lean). This
is the classic Lagrangian / minimum-norm-interpolation duality: the constrained least-norm value is
(prescribed moment)² / (residual variance of the constrained direction).
Contents
* FeasibleScore μ x s — feasibility: s ∈ L²(μ) with the three moment constraints.
* optScore μ x — the optimal score s*(y) = (x/r)·q(y), q the projection residual.
* optScore_feasible, optScore_cost — s* is feasible and achieves cost x²/r (attainment).
* feasibleScore_cost_lower_bound — every feasible s has ∫ s² ≥ x²/r (completing the square:
∫ (s − (x/r)q)² = ∫ s² − x²/r ≥ 0, using ∫ q·s = x and ∫ q² = r).
* scoreCost, scoreCost_eq — the program value and the headline duality scoreCost μ x = x²/r.
Reuse
The identity is the reusable score-cost primitive for arm-specific moment problems: once an arm law
has residual variance r_{a,ν}, a target moment displacement x has least score norm
J_{a,ν}(x) = x² / r_{a,ν}.
Feasibility of a score. s : ℝ → ℝ is feasible for target x if it lies in L²(μ) and is moment-orthogonal to 1 and y while carrying prescribed y²-moment x: s ∈ L²(μ), ∫ s dμ = 0, ∫ y·s dμ = 0, ∫ y²·s dμ = x.
Definition (Lean source)
The optimal score s*(y) = (x / r)·q(y), where q is the L² projection residual of y² onto span{1, y} and r = l2ResidualQuadratic μ. This is the minimum-norm feasible score.
Definition (Lean source)
The value of the score program: the infimum of ∫ s² dμ over all feasible scores s.
Definition (Lean source)
The score-program duality (headline). For a probability measure μ on ℝ with a finite fourth moment and first moment squared strictly below the second moment (positive variance), if moreover the closed-form residual l2ResidualQuadratic μ is positive, then for every target y²-moment x, the value of the constrained minimum-norm score program equals x² / l2ResidualQuadratic μ:
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
optScore_feasibletheorem — Feasibility of the optimal score. s* = (x/r)·q is a feasible score for target x: it lies in L²(μ) and satisfies the three moment constraints. The y²-moment constraint uses ∫ y²·q = r and (x/r)·r = x (needs r ≠ 0).Proof (Lean source)
theorem optScore_feasible (μ : Measure ℝ) [IsProbabilityMeasure μ] (h : FiniteMoment4 μ) (hnd : moment μ 1 ^ 2 < moment μ 2) (hr : 0 < l2ResidualQuadratic μ) (x : ℝ) : FeasibleScore μ x (optScore μ x) := by refine ⟨?_, ?_, ?_, ?_⟩ · exact (projResidual_memL2 μ h).const_mul (x / l2ResidualQuadratic μ) · simp [optScore, integral_const_mul, integral_projResidual μ h hnd] · calc ∫ y, y * optScore μ x y ∂μ = ∫ y, (x / l2ResidualQuadratic μ) * (y * projResidual μ y) ∂μ := by apply integral_congr_ae filter_upwards with y simp [optScore] ring _ = 0 := by simp [integral_const_mul, integral_id_mul_projResidual μ h hnd] · calc ∫ y, y ^ 2 * optScore μ x y ∂μ = ∫ y, (x / l2ResidualQuadratic μ) * (y ^ 2 * projResidual μ y) ∂μ := by apply integral_congr_ae filter_upwards with y simp [optScore] ring _ = x := by rw [integral_const_mul, integral_sq_mul_projResidual μ h hnd] exact div_mul_cancel₀ x (ne_of_gt hr) -
optScore_costtheorem — Attainment. The optimal score s* achieves cost exactly x² / r: ∫ (s*)² dμ = ∫ (x/r)²·q² dμ = (x/r)²·r = x²/r.hypothesesconclusion∫ y, optScore μ x y ^ 2 ∂μ = x ^ 2 / l2ResidualQuadratic μProof (Lean source)
theorem optScore_cost (μ : Measure ℝ) [IsProbabilityMeasure μ] (h : FiniteMoment4 μ) (hnd : moment μ 1 ^ 2 < moment μ 2) (hr : 0 < l2ResidualQuadratic μ) (x : ℝ) : ∫ y, optScore μ x y ^ 2 ∂μ = x ^ 2 / l2ResidualQuadratic μ := by calc ∫ y, optScore μ x y ^ 2 ∂μ = ∫ y, (x / l2ResidualQuadratic μ) ^ 2 * projResidual μ y ^ 2 ∂μ := by apply integral_congr_ae filter_upwards with y simp [optScore, mul_pow] _ = x ^ 2 / l2ResidualQuadratic μ := by rw [integral_const_mul, integral_sq_projResidual μ h hnd] field_simp [ne_of_gt hr] -
feasibleScore_cost_lower_boundtheorem — Lower bound (duality ≤). Every feasible score has cost at least x² / r.hypothesesconclusionx ^ 2 / l2ResidualQuadratic μ ≤ ∫ y, s y ^ 2 ∂μProof (Lean source)
theorem feasibleScore_cost_lower_bound (μ : Measure ℝ) [IsProbabilityMeasure μ] (h : FiniteMoment4 μ) (hnd : moment μ 1 ^ 2 < moment μ 2) (hr : 0 < l2ResidualQuadratic μ) (x : ℝ) {s : ℝ → ℝ} (hs : FeasibleScore μ x s) : x ^ 2 / l2ResidualQuadratic μ ≤ ∫ y, s y ^ 2 ∂μ := by let r := l2ResidualQuadratic μ let c := x / r let q := projResidual μ have hq_mem : MemLp q 2 μ := by simpa [q] using projResidual_memL2 μ h have hs_int : Integrable s μ := hs.memL2.integrable (by norm_num) have hys_int : Integrable (fun y : ℝ => y * s y) μ := (memL2_id μ h).integrable_mul hs.memL2 have hy2s_int : Integrable (fun y : ℝ => y ^ 2 * s y) μ := (memL2_sq μ h).integrable_mul hs.memL2 have hqs_int : Integrable (fun y : ℝ => q y * s y) μ := hq_mem.integrable_mul hs.memL2 have hq2_int : Integrable (fun y : ℝ => q y ^ 2) μ := hq_mem.integrable_sq have hs2_int : Integrable (fun y : ℝ => s y ^ 2) μ := hs.memL2.integrable_sq have hqs : ∫ y, q y * s y ∂μ = x := by calc ∫ y, q y * s y ∂μ = ∫ y, y ^ 2 * s y - optIntercept μ * s y - optSlope μ * (y * s y) ∂μ := by apply integral_congr_ae filter_upwards with y simp [q, projResidual] ring _ = (∫ y, y ^ 2 * s y - optIntercept μ * s y ∂μ) - (∫ y, optSlope μ * (y * s y) ∂μ) := by exact integral_sub (hy2s_int.sub (hs_int.const_mul _)) (hys_int.const_mul _) _ = ((∫ y, y ^ 2 * s y ∂μ) - (∫ y, optIntercept μ * s y ∂μ)) - (∫ y, optSlope μ * (y * s y) ∂μ) := by rw [integral_sub hy2s_int (hs_int.const_mul _)] _ = (∫ y, y ^ 2 * s y ∂μ) - (∫ y, optIntercept μ * s y ∂μ) - (∫ y, optSlope μ * (y * s y) ∂μ) := by ring _ = x := by simp [integral_const_mul, hs.cov_sq, hs.mean_zero, hs.cov_id_zero] have hnn : 0 ≤ ∫ y, (s y - c * q y) ^ 2 ∂μ := integral_nonneg (fun y => sq_nonneg (s y - c * q y)) have hexpand : ∫ y, (s y - c * q y) ^ 2 ∂μ = (∫ y, s y ^ 2 ∂μ) - 2 * c * (∫ y, q y * s y ∂μ) + c ^ 2 * (∫ y, q y ^ 2 ∂μ) := by calc ∫ y, (s y - c * q y) ^ 2 ∂μ = ∫ y, s y ^ 2 - 2 * c * (q y * s y) + c ^ 2 * q y ^ 2 ∂μ := by apply integral_congr_ae filter_upwards with y ring _ = (∫ y, s y ^ 2 - 2 * c * (q y * s y) ∂μ) + (∫ y, c ^ 2 * q y ^ 2 ∂μ) := by exact integral_add (hs2_int.sub (hqs_int.const_mul _)) (hq2_int.const_mul _) _ = ((∫ y, s y ^ 2 ∂μ) - (∫ y, 2 * c * (q y * s y) ∂μ)) + (∫ y, c ^ 2 * q y ^ 2 ∂μ) := by rw [integral_sub hs2_int (hqs_int.const_mul _)] _ = (∫ y, s y ^ 2 ∂μ) - (∫ y, 2 * c * (q y * s y) ∂μ) + (∫ y, c ^ 2 * q y ^ 2 ∂μ) := by ring _ = (∫ y, s y ^ 2 ∂μ) - 2 * c * (∫ y, q y * s y ∂μ) + c ^ 2 * (∫ y, q y ^ 2 ∂μ) := by rw [integral_const_mul, integral_const_mul] have hnonneg : 0 ≤ (∫ y, s y ^ 2 ∂μ) - 2 * c * x + c ^ 2 * r := by rw [hexpand, hqs] at hnn simpa [q, r, integral_sq_projResidual μ h hnd] using hnn have halg : 2 * c * x - c ^ 2 * r = x ^ 2 / r := by subst c subst r field_simp [ne_of_gt hr] ring linarith