Stat.Nonparametric.Moment­Problems.Residual­Quadratic

Moment-coordinate algebra for residual quadratic moment problems

This is the measure-free algebra layer for the MomentProblems folder. It works only with raw moments m₁, m₂, m₃, m₄, and proves the identities used by the measure-level L² projection and bounded-outcome envelope files.

The central residual is the squared L²(μ)-distance of y² to span{1, y}, i.e. the residual variance of regressing y² on 1 and y:

r(μ) = min_{b₀, b₁} ∫ (y² − b₀ − b₁ y)² dμ.

For any law with moments m₁, m₂, m₃, m₄ (and m₀ = 1) this residual has the closed form momentResidual m₁ m₂ m₃ m₄, the ratio of the two leading Hankel determinants. This file proves, purely at the level of moments (no measure theory):

* residualQuad_ge_momentResidual / residualQuad_optimalCoeff — momentResidual is exactly the minimum over (b₀, b₁) of the regression objective, whenever the design is nondegenerate (m₁² < m₂, i.e. positive variance). This is the reusable residual-variance formula. * extremalResidual_eq_envelope — the extremal three-point law on {0, xᵥ, 1} with second moment q, encoded through its moments M₁ = t, M₂ = q, M₃, M₄ (single fractions of the free support parameter t and q), has residual exactly the closed form momentEnvelope t q = ((t − q)(q − t²)) / (4 t (1 − t)), for every admissible t. * momentEnvelope_hasDerivAt / momentEnvelope_stationary_of_quartic — as a function of the support parameter t, the family residual momentEnvelope t q has derivative envelopeQuartic t q / (4 t² (t − 1)²), so its stationary points are exactly the roots of the quartic t⁴ − 2t³ + 2q t² − 2q² t + q² = 0. The maximizing root t = μᵥ ∈ (q, √q) therefore selects the value ρ(v) = momentEnvelope μᵥ q of the envelope. * momentResidual_le_momentEnvelope / momentEnvelope_le_root / momentResidual_le_envelope — the sharp upper bound r(μ) ≤ ρ(v) for every admissible law μ on [0,1] with ∫ y² = q, proved by an explicit dual (SOS) certificate rather than general moment-problem machinery: a pointwise polynomial identity whose right side y(1−y)(y−xᵥ)² is manifestly nonnegative on [0,1], plus the quartic-root maximality of the envelope over admissible first moments.

The existence/uniqueness of the maximizing root (u = μᵥ, taken here as a hypothesis of the sharp bound) is packaged at the measure/envelope layer in MomentProblems.BoundedOutcomeEnvelope.QuarticRoot.

Measure-level L² projection residual of y ↦ y² onto span{1, y}

This file is the measure bridge for the MomentProblems stack. MomentAlgebra.lean proves the closed-form residual purely in moment coordinates; this file turns that algebra into the actual L²(μ) projection residual for probability measures on ℝ with finite fourth moment:

r(μ) = ⨅_{b₀,b₁} ∫ (y² − b₀ − b₁ y)² dμ.

Writing mₖ = rawMoment μ k = ∫ yᵏ dμ for the raw moments (the shared MomentProblems.rawMoment), the closed form is the Hankel-determinant ratio

r(μ) = (m₄ − m₂²) − (m₃ − m₁ m₂)² / (m₂ − m₁²) = det H₃ / det H₂,

attained at the least-squares optimal coefficients b₁* = (m₃ − m₁ m₂)/(m₂ − m₁²), b₀* = m₂ − b₁* m₁ (here written optIntercept, optSlope).

Design

The moment-level algebra — that the quadratic objective residualQuad m₁ m₂ m₃ m₄ b₀ b₁ in (b₀, b₁) has minimum the Hankel ratio, via a completed-square / SOS certificate — is proven, measure-free, in Causalean.Stat.MomentProblems.ResidualQuadratic.MomentAlgebra (residualQuad_optimalCoeff, residualQuad_ge_momentResidual). This module supplies the measure-theoretic bridge:

* residualQuad_eq — the bridge: expanding the square and integrating term by term, ∫ (y² − b₀ − b₁ y)² dμ equals the moment polynomial MomentAlgebra.residualQuad m₁ m₂ m₃ m₄ b₀ b₁ (uses IsProbabilityMeasure for the constant term ∫ b₀² = b₀² and integrability of y, …, y⁴ to split the integral). * residualQuad_opt_eq, l2ResidualQuadratic_le, l2ResidualQuadratic_nonneg, iInf_residualQuad — the optimality / infimum bridge transporting the moment-level minimum to the ∫-form and the conditional infimum ⨅ b₀ b₁.

Finite fourth moment is packaged as FiniteMoment4 μ (integrability of y, y², y³, y⁴); for a probability measure with ∫ y⁴ < ∞ all these lower moments are finite, so this is exactly the "finite 4th moment" hypothesis. Non-degeneracy is m₁² < m₂ (positive variance).

Projection residual function for the moment score program

This file is the functional bridge between MomentProblems.ResidualQuadratic.MeasureBridge and the constrained score program. For a probability measure μ on ℝ with finite fourth moment and positive variance (m₁² < m₂), MeasureBridge.lean computes the closed-form residual value r(μ) = l2ResidualQuadratic μ; this file identifies the residual function that attains that value,

q(y) := y² − (optIntercept μ + optSlope μ · y),

and proves the four facts that make it the orthogonal projection residual of y² onto span{1,y}:

• integral_projResidual : ∫ q dμ = 0 (orthogonal to the constant 1)
• integral_id_mul_projResidual : ∫ y·q dμ = 0 (orthogonal to y)
• integral_sq_projResidual : ∫ q² dμ = r (its own L² norm² is the residual r)
• integral_sq_mul_projResidual : ∫ y²·q dμ = r (y²-moment of q equals r)

The first two are the normal equations of least squares; here they reduce, after splitting the integral into raw moments mₖ = ∫ yᵏ, to pure moment algebra in the definitions of optIntercept/optSlope (division by m₁² − m₂ ≠ 0). The last two reuse MeasureBridge.residualQuad_opt_eq, the attainment lemma for the closed-form residual.

These are the ingredients consumed by ScoreProgram.lean to solve the constrained minimum-norm "score program" dual to this projection.