Stat.Nonparametric.Moment­Problems.Bounded­Outcome­Envelope

Bounded-outcome residual envelope: definitions

This file starts the bounded-outcome branch of MomentProblems. It defines the sharp envelope ρ(v) of the L² residual of y² on span{1, y} over probability measures on [0,1] with fixed second moment v².

* maximizingRoot v — the unique interior root μᵥ ∈ (v², v) of the FOC quartic (from interior_quartic_exists), extracted by choice. * rhoEnvelope v := momentEnvelope μᵥ (v²) — the closed-form envelope value ρ(v). * Admissible v μ — μ is a probability measure a.e. supported in [0,1] with ∫ y² ∂μ = v². * residualSet v — the set of realized residuals { l2ResidualQuadratic μ | Admissible v μ }, whose supremum the main file shows equals rhoEnvelope v.

Attainment for the bounded-outcome residual envelope

This file proves the lower-bound/attainment half of the bounded-outcome residual envelope. The measure-level supremum ρ(v) is attained by an explicit three-point law on {0, xᵥ, 1}, where xᵥ = extremalMid μᵥ (v²) is the interior support point of the extremal law whose first moment is the maximizing root μᵥ = maximizingRoot v.

The weights w₀, w₁, w₂ are the unique solution of the three linear moment constraints w₀ + w₁ + w₂ = 1, w₁ xᵥ + w₂ = μᵥ, w₁ xᵥ² + w₂ = v², namely

w₁ = (μᵥ − v²) / (xᵥ (1 − xᵥ)), w₂ = (v² − μᵥ xᵥ) / (1 − xᵥ), w₀ = 1 − w₁ − w₂.

For μᵥ ∈ (v², v) these are nonnegative and xᵥ ∈ (0,1), so extremalMeasure v is a probability measure supported in [0,1]. Its raw moments are mₖ = w₁ xᵥᵏ + w₂ (k ≥ 1), which match the extremal moments (μᵥ, v², extremalM3 μᵥ (v²), extremalM4 μᵥ (v²)); hence by MomentAlgebra.extremalResidual_eq_envelope its residual equals momentEnvelope μᵥ (v²) = ρ(v).

Bounded-outcome residual envelope upper bound r(μ) ≤ ρ(v)

This file proves the upper-bound half of the bounded-outcome residual envelope. For every admissible law μ (probability measure a.e. supported in [0,1] with ∫ y² ∂μ = v²), the residual l2ResidualQuadratic μ is at most rhoEnvelope v.

The bridge to the moment-level MomentAlgebra.momentResidual_le_envelope needs three measure-level facts about the raw moments m = ∫ y, q = ∫ y² = v², m₃ = ∫ y³, m₄ = ∫ y⁴:

* finiteMoment4_of_admissible — all four powers are integrable (bounded support + finite measure). * moment2_le_moment1 — q ≤ m, since y² ≤ y a.e. on [0,1] (monotone integral). * moment1_sq_le_moment2 — m² ≤ q, i.e. Var ≥ 0 (Cauchy–Schwarz for a probability measure). * crossMoment_nonneg — 0 ≤ crossMoment m q m₃ m₄, because that moment combination equals the integral ∫ y (1 − y) (y − xᵥ)² ∂μ of a function nonnegative on [0,1].

The degenerate case m² = q (a point mass) is handled directly: l2ResidualQuadratic μ = 0 (vanishing denominator), and ρ(v) > 0.

Bounded-outcome residual envelope: IsLUB

This file assembles the bounded-outcome moment problem. For v ∈ (0,1), the measure-level residual envelope ρ(v) = rhoEnvelope v is the least upper bound of the residual l2ResidualQuadratic μ over all admissible laws μ (probability measures on [0,1] with second moment v²), and it is attained by the extremal three-point law.

• rho_envelope_isLUB — IsLUB (residualSet v) (rhoEnvelope v).
• rho_envelope_attained — the extremal law realizing ρ(v) (re-exported from Attainment).
• interior_quartic_unique_root — the unique interior root of the FOC quartic (from QuarticRoot).

The IsLUB combines the upper bound l2ResidualQuadratic_le_rho (every admissible residual is ≤ ρ(v)) with attainment (ρ(v) itself is a realized residual), so any upper bound of the set is ≥ ρ(v).

Quartic root selecting the bounded-outcome residual envelope

This file proves the root facts used by BoundedOutcomeEnvelope.Defs to define the envelope maximizer. The tangent-strength envelope ρ(v) = momentEnvelope μᵥ (v²) is selected by the maximizing support parameter μᵥ, which is the unique root of the FOC quartic envelopeQuartic t q = t⁴ − 2t³ + 2q t² − 2q² t + q² inside the open interval (q, v) with q = v². This file proves that root exists and is unique.

The two endpoint sign facts are elementary polynomial identities:

• envelopeQuartic q q = q² (1 − q)² > 0 (envelopeQuartic_pos_at_q);
• envelopeQuartic v (v²) = −2 v³ (v − 1)² < 0 (envelopeQuartic_neg_at_v).

Because t ↦ envelopeQuartic t q is a continuous polynomial with q = v² < v, the intermediate value theorem produces a root in (q, v) (interior_quartic_exists). The derivative 4 t³ − 6 t² + 4 q t − 2 q² is strictly negative on (q, v), so the quartic is strictly antitone there; hence the root is unique (interior_quartic_unique_root).

These facts feed Defs.lean, which uses the (unique) root to define maximizingRoot and rhoEnvelope.