Stat.Nonparametric.MomentProblems.BoundedOutcomeEnvelope
Sharp bounded-outcome residual envelopes: quartic root selection, admissible laws, upper bounds, and extremal three-point attainment.
Defs 5 core · 3 supporting This file starts the bounded-outcome branch of MomentProblems. ★ rhoEnvelope_pos
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.
def maximizingRoot reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
For a real number , the selected maximizing root is the unique root in of the envelope first-order quartic when , and is otherwise.
Definition (Lean source)
parameters
v :
ℝ
def
maximizingRoot v :
ℝ
given by
if h : 0 < v ∧ v < 1 then (interior_quartic_exists v h.1 h.2).choose else 0
def rhoEnvelope reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
For a real number , the measure-level residual envelope is , where is the selected maximizing root at second moment .
Definition (Lean source)
theorem rhoEnvelope_pos reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
The envelope value ρ(v) is strictly positive for v strictly between 0 and 1: momentEnvelope μᵥ (v²) = (μᵥ − v²)(v² − μᵥ²) / (4 μᵥ (1 − μᵥ)) has all four factors positive when μᵥ ∈ (v², v).
Formal statement
Proof (Lean source)
theorem rhoEnvelope_pos (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : 0 < rhoEnvelope v := by
have hmem := maximizingRoot_mem v hv0 hv1
set u := maximizingRoot v with hu
have h1 : v ^ 2 < u := hmem.1
have h2 : u < v := hmem.2
have hu0 : 0 < u := lt_trans (by positivity) h1
have hu1 : u < 1 := lt_trans h2 hv1
have hnum1 : 0 < u - v ^ 2 := by linarith
have hnum2 : 0 < v ^ 2 - u ^ 2 := by nlinarith
have hden : 0 < 4 * u * (1 - u) := by nlinarith
rw [rhoEnvelope, momentEnvelope]
positivity
structure Admissible reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
μ is admissible for the envelope at level v: a probability measure a.e. supported in [0,1] with second moment ∫ y² ∂μ = v². These are exactly the laws over which the residual l2ResidualQuadratic is maximized to give ρ(v).
Definition (Lean source)
def residualSet reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
For a real number , the set of residual values realized by admissible laws contains exactly the quadratic least-squares residuals of probability measures that are almost surely supported on and have second moment .
Definition (Lean source)
parameters
v :
ℝ
def
given by
3 supporting declarations (lemmas, instances)
-
maximizingRoot_memtheorem — maximizingRoot v lies in the open interval (v², v).Proof (Lean source)
theorem maximizingRoot_mem (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : maximizingRoot v ∈ Ioo (v ^ 2) v := by rw [maximizingRoot, dif_pos ⟨hv0, hv1⟩] exact (interior_quartic_exists v hv0 hv1).choose_spec.1 -
maximizingRoot_quartictheorem — maximizingRoot v is a root of the FOC quartic at q = v².Proof (Lean source)
theorem maximizingRoot_quartic (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : envelopeQuartic (maximizingRoot v) (v ^ 2) = 0 := by rw [maximizingRoot, dif_pos ⟨hv0, hv1⟩] exact (interior_quartic_exists v hv0 hv1).choose_spec.2 -
moment2_eqtheorem — Second moment of an admissible law in rawMoment-form: rawMoment μ 2 = v².Proof (Lean source)
theorem Admissible.moment2_eq {v : ℝ} {μ : Measure ℝ} (h : Admissible v μ) : rawMoment μ 2 = v ^ 2 := by change ∫ y, y ^ 2 ∂μ = v ^ 2 exact h.moment2
Attainment 6 core · 11 supporting This file proves the lower-bound/attainment half of the bounded-outcome residual envelope. ★ rho_envelope_attained
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).
def extremalSupp reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
For a real number , the interior support point of the extremal three-point law is , where is the selected maximizing first moment at second moment .
Definition (Lean source)
def extremalW1 reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
For a real number , the weight on the interior support point is , where is the selected maximizing first moment and is the interior support point.
Definition (Lean source)
parameters
v :
ℝ
def
extremalW1 v :
ℝ
given by
def extremalW2 reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
For a real number , the weight on the support point is , where is the selected maximizing first moment and is the interior support point.
Definition (Lean source)
parameters
v :
ℝ
def
extremalW2 v :
ℝ
given by
def extremalW0 reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
For a real number , the weight on the support point is one minus the weights assigned to the interior support point and to .
Definition (Lean source)
def extremalMeasure reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
For a real number , the extremal three-point measure places the nonnegative parts of the three prescribed weights at , at the associated interior support point, and at , respectively.
Definition (Lean source)
parameters
v :
ℝ
def
given by
ofReal (extremalW0 v) • Measure.dirac 0
+ ofReal (extremalW2 v) • Measure.dirac 1
theorem rho_envelope_attained reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
Envelope attainment. For v strictly between 0 and 1, there is an admissible law whose residual is exactly ρ(v). Together with the upper bound this makes ρ(v) the supremum.
Formal statement
hypotheses
v :
ℝ
hv0 :
0 < v
hv1 :
v < 1
Proof (Lean source)
theorem rho_envelope_attained (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) :
∃ μ : Measure ℝ, Admissible v μ ∧ l2ResidualQuadratic μ = rhoEnvelope v :=
⟨extremalMeasure v, extremalMeasure_admissible v hv0 hv1, extremalMeasure_residual v hv0 hv1⟩
11 supporting declarations (lemmas, instances)
-
extremalSupp_memtheorem — The interior support point lies in (0,1): xᵥ = (μᵥ² − 2 μᵥ v² + v²)/(2 μᵥ (1 − μᵥ)) ∈ (0,1) for μᵥ ∈ (v², v). Proof: nlinarith from v² < μᵥ < v < 1.Proof (Lean source)
theorem extremalSupp_mem (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : extremalSupp v ∈ Ioo (0 : ℝ) 1 := by have hmem := maximizingRoot_mem v hv0 hv1 set u := maximizingRoot v with hu have hu0 : 0 < u := lt_trans (by positivity) hmem.1 have hu1 : u < 1 := lt_trans hmem.2 hv1 have hq1 : v ^ 2 < 1 := by nlinarith have hden : 0 < 2 * u * (1 - u) := by nlinarith unfold extremalSupp extremalMid rw [← hu] constructor · apply div_pos · have hnum : 0 < (u - v ^ 2) ^ 2 + v ^ 2 * (1 - v ^ 2) := by have hsq : 0 ≤ (u - v ^ 2) ^ 2 := sq_nonneg _ have hv2pos : 0 < v ^ 2 := by positivity have hv2one : 0 < 1 - v ^ 2 := by linarith have hprod : 0 < v ^ 2 * (1 - v ^ 2) := mul_pos hv2pos hv2one nlinarith nlinarith [hnum] · exact hden · rw [div_lt_one hden] nlinarith [hmem.1, hmem.2, hv0, hv1, hu0, hu1, sq_nonneg (u - v ^ 2), sq_nonneg (v - u), sq_nonneg (1 - v)] -
extremalW_nonnegtheorem — The three weights are nonnegative for v ∈ (0,1). Proof: w₁ > 0 since μᵥ > v² and xᵥ ∈ (0,1); w₂ ≥ 0 since v² ≥ μᵥ xᵥ; w₀ ≥ 0 since w₁ + w₂ ≤ 1. All via nlinarith from v² < μᵥ < v and extremalSupp_mem.hypothesesv :ℝhv0 :0 < vhv1 :v < 1Proof (Lean source)
theorem extremalW_nonneg (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : 0 ≤ extremalW0 v ∧ 0 ≤ extremalW1 v ∧ 0 ≤ extremalW2 v := by have hmem := maximizingRoot_mem v hv0 hv1 have hx := extremalSupp_mem v hv0 hv1 set u := maximizingRoot v with hu have hu0 : 0 < u := lt_trans (by positivity) hmem.1 have hu1 : u < 1 := lt_trans hmem.2 hv1 have hu2lt : u ^ 2 < v ^ 2 := by have hdiff : 0 < v - u := sub_pos.mpr hmem.2 have hsum : 0 < v + u := by nlinarith have hprod : 0 < (v - u) * (v + u) := mul_pos hdiff hsum nlinarith have hdenu : 0 < 2 * u * (1 - u) := by nlinarith have hnumx : 0 < u ^ 2 - 2 * u * v ^ 2 + v ^ 2 := by have hnum : 0 < (u - v ^ 2) ^ 2 + v ^ 2 * (1 - v ^ 2) := by have hsq : 0 ≤ (u - v ^ 2) ^ 2 := sq_nonneg _ have hv2pos : 0 < v ^ 2 := by positivity have hv2one : 0 < 1 - v ^ 2 := by nlinarith have hprod : 0 < v ^ 2 * (1 - v ^ 2) := mul_pos hv2pos hv2one nlinarith nlinarith [hnum] have h1xnum : 0 < 2 * u * (1 - u) - (u ^ 2 - 2 * u * v ^ 2 + v ^ 2) := by nlinarith [hmem.1, hmem.2, hv0, hv1, hu0, hu1, sq_nonneg (u - v ^ 2), sq_nonneg (v - u), sq_nonneg (1 - v)] have hw2num : 0 ≤ v ^ 2 - u * extremalSupp v := by have hformula : v ^ 2 - u * extremalSupp v = (v ^ 2 - u ^ 2) / (2 * (1 - u)) := by unfold extremalSupp extremalMid rw [← hu] field_simp [ne_of_gt hu0, ne_of_gt (sub_pos.mpr hu1)] ring rw [hformula] apply div_nonneg · nlinarith · nlinarith have hw0num : 0 ≤ v ^ 2 - u * extremalSupp v - u + extremalSupp v := by have hformula : v ^ 2 - u * extremalSupp v - u + extremalSupp v = (v ^ 2 - u ^ 2) / (2 * u) := by unfold extremalSupp extremalMid rw [← hu] field_simp [ne_of_gt hu0, ne_of_gt (sub_pos.mpr hu1)] ring rw [hformula] apply div_nonneg · nlinarith · positivity have hw0formula : extremalW0 v = (v ^ 2 - u * extremalSupp v - u + extremalSupp v) / extremalSupp v := by unfold extremalW0 extremalW1 extremalW2 rw [← hu] field_simp [ne_of_gt hx.1, ne_of_gt (sub_pos.mpr hx.2)] ring constructor · rw [hw0formula] exact div_nonneg hw0num (le_of_lt hx.1) constructor · unfold extremalW1 apply div_nonneg · exact sub_nonneg.mpr (le_of_lt hmem.1) · apply mul_nonneg · exact le_of_lt hx.1 · exact sub_nonneg.mpr (le_of_lt hx.2) · unfold extremalW2 apply div_nonneg hw2num exact sub_nonneg.mpr (le_of_lt hx.2) -
extremalMeasure_moment_powtheorem — Raw moments of the extremal law. For k ≥ 1, ∫ yᵏ ∂(extremalMeasure v) = w₁ xᵥᵏ + w₂ (the mass at 0 contributes nothing, the mass at 1 contributes w₂). Proof: expand via integral_add_measure, integral_smul_measure, integral_dirac, using w_i ≥ 0 to convert ENNReal.ofReal wᵢ back to wᵢ, and (0:ℝ)^k = 0, (1:ℝ)^k = 1.hypothesesv :ℝhv0 :0 < vhv1 :v < 1k :ℕhk :1 ≤ kconclusionProof (Lean source)
theorem extremalMeasure_moment_pow (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) {k : ℕ} (hk : 1 ≤ k) : rawMoment (extremalMeasure v) k = extremalW1 v * (extremalSupp v) ^ k + extremalW2 v := by have hw := extremalW_nonneg v hv0 hv1 have hk0 : k ≠ 0 := by omega let f : ℝ → ℝ := fun y => y ^ k have hI0 : Integrable f (ofReal (extremalW0 v) • Measure.dirac (0 : ℝ)) := Integrable.smul_measure (μ := Measure.dirac (0 : ℝ)) (c := ofReal (extremalW0 v)) (integrable_dirac (f := f) (a := (0 : ℝ)) (by simp [f, enorm])) (by simp) have hI1 : Integrable f (ofReal (extremalW1 v) • Measure.dirac (extremalSupp v)) := Integrable.smul_measure (μ := Measure.dirac (extremalSupp v)) (c := ofReal (extremalW1 v)) (integrable_dirac (f := f) (a := extremalSupp v) (by simp [f, enorm])) (by simp) have hI2 : Integrable f (ofReal (extremalW2 v) • Measure.dirac (1 : ℝ)) := Integrable.smul_measure (μ := Measure.dirac (1 : ℝ)) (c := ofReal (extremalW2 v)) (integrable_dirac (f := f) (a := (1 : ℝ)) (by simp [f, enorm])) (by simp) unfold rawMoment extremalMeasure change ∫ y, f y ∂(ofReal (extremalW0 v) • Measure.dirac (0 : ℝ) + ofReal (extremalW1 v) • Measure.dirac (extremalSupp v) + ofReal (extremalW2 v) • Measure.dirac (1 : ℝ)) = extremalW1 v * (extremalSupp v) ^ k + extremalW2 v rw [integral_add_measure (hI0.add_measure hI1) hI2] rw [integral_add_measure hI0 hI1] rw [integral_smul_measure, integral_smul_measure, integral_smul_measure] simp [f, hw.1, hw.2.1, hw.2.2, hk0, smul_eq_mul] -
extremalMeasure_isProbtheorem — extremalMeasure v is a probability measure (total mass w₀ + w₁ + w₂ = 1, weights ≥ 0).Proof (Lean source)
theorem extremalMeasure_isProb (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : IsProbabilityMeasure (extremalMeasure v) := by have hw := extremalW_nonneg v hv0 hv1 rw [isProbabilityMeasure_iff] unfold extremalMeasure rw [Measure.add_apply, Measure.add_apply, Measure.smul_apply, Measure.smul_apply, Measure.smul_apply] simp only [Measure.dirac_apply, Set.indicator_of_mem, Set.mem_univ, Pi.one_apply, smul_eq_mul, mul_one] rw [← ENNReal.ofReal_add hw.1 hw.2.1] rw [← ENNReal.ofReal_add (add_nonneg hw.1 hw.2.1) hw.2.2] have hsum : extremalW0 v + extremalW1 v + extremalW2 v = 1 := by unfold extremalW0 ring rw [hsum] simp -
extremalMeasure_supptheorem — extremalMeasure v is a.e. supported in [0,1] (its atoms 0, xᵥ, 1 all lie in [0,1]).Proof (Lean source)
theorem extremalMeasure_supp (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : ∀ᵐ y ∂(extremalMeasure v), y ∈ Icc (0 : ℝ) 1 := by have hx := extremalSupp_mem v hv0 hv1 rw [ae_iff] change (extremalMeasure v) {y : ℝ | y ∉ Icc (0 : ℝ) 1} = 0 unfold extremalMeasure rw [Measure.add_apply, Measure.add_apply, Measure.smul_apply, Measure.smul_apply, Measure.smul_apply] simp [hx.1.le, hx.2.le] -
extremalMeasure_moment1theorem — First moment: ∫ y ∂(extremalMeasure v) = μᵥ. Algebraic: w₁ xᵥ + w₂ = μᵥ.hypothesesv :ℝhv0 :0 < vhv1 :v < 1conclusionProof (Lean source)
theorem extremalMeasure_moment1 (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : rawMoment (extremalMeasure v) 1 = maximizingRoot v := by rw [extremalMeasure_moment_pow v hv0 hv1 (by norm_num : 1 ≤ 1)] have hmem := maximizingRoot_mem v hv0 hv1 have hx := extremalSupp_mem v hv0 hv1 set u := maximizingRoot v with hu unfold extremalW1 extremalW2 rw [← hu] field_simp [ne_of_gt hx.1, ne_of_gt (sub_pos.mpr hx.2)] ring -
extremalMeasure_moment2theorem — Second moment: ∫ y² ∂(extremalMeasure v) = v². Algebraic: w₁ xᵥ² + w₂ = v².Proof (Lean source)
theorem extremalMeasure_moment2 (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : rawMoment (extremalMeasure v) 2 = v ^ 2 := by rw [extremalMeasure_moment_pow v hv0 hv1 (by norm_num : 1 ≤ 2)] have hmem := maximizingRoot_mem v hv0 hv1 have hx := extremalSupp_mem v hv0 hv1 set u := maximizingRoot v with hu unfold extremalW1 extremalW2 rw [← hu] field_simp [ne_of_gt hx.1, ne_of_gt (sub_pos.mpr hx.2)] ring -
extremalMeasure_moment3theorem — Third moment matches the extremal M₃: w₁ xᵥ³ + w₂ = extremalM3 μᵥ (v²). Pure algebra (field_simp/ring) using xᵥ = extremalMid μᵥ (v²) and the weight formulas.hypothesesv :ℝhv0 :0 < vhv1 :v < 1conclusionProof (Lean source)
theorem extremalMeasure_moment3 (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : rawMoment (extremalMeasure v) 3 = extremalM3 (maximizingRoot v) (v ^ 2) := by rw [extremalMeasure_moment_pow v hv0 hv1 (by norm_num : 1 ≤ 3)] set u := maximizingRoot v with hu set q := v ^ 2 with hq have hmem : u ∈ Ioo q v := by simpa [hu, hq] using maximizingRoot_mem v hv0 hv1 set x := extremalSupp v with hx have hu0 : 0 < u := lt_trans (by positivity) hmem.1 have hu1 : u < 1 := lt_trans hmem.2 hv1 have hm1alg : extremalW1 v * x + extremalW2 v = u := by have h := extremalMeasure_moment1 v hv0 hv1 rw [extremalMeasure_moment_pow v hv0 hv1 (by norm_num : 1 ≤ 1)] at h simpa [hu, hx] using h have hm2alg : extremalW1 v * x ^ 2 + extremalW2 v = q := by have h := extremalMeasure_moment2 v hv0 hv1 rw [extremalMeasure_moment_pow v hv0 hv1 (by norm_num : 1 ≤ 2)] at h simpa [hq, hx] using h have hxformula : x = (u ^ 2 - 2 * u * q + q) / (2 * u * (1 - u)) := by rw [hx] unfold extremalSupp extremalMid rw [← hu, ← hq] change extremalW1 v * x ^ 3 + extremalW2 v = extremalM3 u q calc extremalW1 v * x ^ 3 + extremalW2 v = (1 + x) * (extremalW1 v * x ^ 2 + extremalW2 v) - x * (extremalW1 v * x + extremalW2 v) := by ring _ = (1 + x) * q - x * u := by rw [hm1alg, hm2alg] _ = extremalM3 u q := by rw [hxformula] unfold extremalM3 field_simp [ne_of_gt hu0, ne_of_gt (sub_pos.mpr hu1), sub_ne_zero.mpr (ne_of_lt hu1)] ring -
extremalMeasure_moment4theorem — Fourth moment matches the extremal M₄: w₁ xᵥ⁴ + w₂ = extremalM4 μᵥ (v²). Pure algebra.hypothesesv :ℝhv0 :0 < vhv1 :v < 1conclusionProof (Lean source)
theorem extremalMeasure_moment4 (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : rawMoment (extremalMeasure v) 4 = extremalM4 (maximizingRoot v) (v ^ 2) := by rw [extremalMeasure_moment_pow v hv0 hv1 (by norm_num : 1 ≤ 4)] set u := maximizingRoot v with hu set q := v ^ 2 with hq have hmem : u ∈ Ioo q v := by simpa [hu, hq] using maximizingRoot_mem v hv0 hv1 set x := extremalSupp v with hx have hu0 : 0 < u := lt_trans (by positivity) hmem.1 have hu1 : u < 1 := lt_trans hmem.2 hv1 have hm2alg : extremalW1 v * x ^ 2 + extremalW2 v = q := by have h := extremalMeasure_moment2 v hv0 hv1 rw [extremalMeasure_moment_pow v hv0 hv1 (by norm_num : 1 ≤ 2)] at h simpa [hq, hx] using h have hm3alg : extremalW1 v * x ^ 3 + extremalW2 v = extremalM3 u q := by have h := extremalMeasure_moment3 v hv0 hv1 rw [extremalMeasure_moment_pow v hv0 hv1 (by norm_num : 1 ≤ 3)] at h simpa [hu, hq, hx] using h have hxformula : x = (u ^ 2 - 2 * u * q + q) / (2 * u * (1 - u)) := by rw [hx] unfold extremalSupp extremalMid rw [← hu, ← hq] change extremalW1 v * x ^ 4 + extremalW2 v = extremalM4 u q calc extremalW1 v * x ^ 4 + extremalW2 v = (1 + x) * (extremalW1 v * x ^ 3 + extremalW2 v) - x * (extremalW1 v * x ^ 2 + extremalW2 v) := by ring _ = (1 + x) * extremalM3 u q - x * q := by rw [hm2alg, hm3alg] _ = extremalM4 u q := by rw [hxformula] unfold extremalM3 extremalM4 field_simp [ne_of_gt hu0, ne_of_gt (sub_pos.mpr hu1), sub_ne_zero.mpr (ne_of_lt hu1)] ring -
extremalMeasure_admissibletheorem — The extremal law is admissible.Proof (Lean source)
theorem extremalMeasure_admissible (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : Admissible v (extremalMeasure v) := by refine ⟨extremalMeasure_isProb v hv0 hv1, extremalMeasure_supp v hv0 hv1, ?_⟩ have := extremalMeasure_moment2 v hv0 hv1 simpa [rawMoment] using this -
extremalMeasure_residualtheorem — The extremal law realizes ρ(v). Its residual equals the envelope value: l2ResidualQuadratic (extremalMeasure v) = rhoEnvelope v.hypothesesv :ℝhv0 :0 < vhv1 :v < 1conclusionProof (Lean source)
theorem extremalMeasure_residual (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : l2ResidualQuadratic (extremalMeasure v) = rhoEnvelope v := by have hmem := maximizingRoot_mem v hv0 hv1 set u := maximizingRoot v with hu have hu0 : u ≠ 0 := ne_of_gt (lt_trans (by positivity) hmem.1) have hu1 : u ≠ 1 := ne_of_lt (lt_trans hmem.2 hv1) have huq : u ^ 2 ≠ v ^ 2 := by have hu0' : (0 : ℝ) < u := lt_trans (by positivity) hmem.1 have : u ^ 2 < v ^ 2 := by nlinarith [hmem.1, hmem.2, hu0'] exact ne_of_lt this have hm1 := extremalMeasure_moment1 v hv0 hv1 have hm2 := extremalMeasure_moment2 v hv0 hv1 have hm3 := extremalMeasure_moment3 v hv0 hv1 have hm4 := extremalMeasure_moment4 v hv0 hv1 have hkey := extremalResidual_eq_envelope u (v ^ 2) hu0 hu1 huq unfold l2ResidualQuadratic rw [hm1, hm2, hm3, hm4] -- `extremalM1 u = u`, so `momentResidual u (v²) (extremalM3 u (v²)) (extremalM4 u (v²))` -- is exactly the LHS of `hkey`. simpa [extremalM1, rhoEnvelope, hu] using hkey
Bounds 1 core · 5 supporting This file proves the upper-bound half of the bounded-outcome residual envelope. ★ l2ResidualQuadratic_le_rho
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.
theorem l2ResidualQuadratic_le_rho reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
Measure-level sharp upper bound. For v strictly between 0 and 1 and every admissible probability law μ on [0,1] with second moment v², the closed-form residual is at most the envelope value: l2ResidualQuadratic μ ≤ rhoEnvelope v.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem l2ResidualQuadratic_le_rho (v : ℝ) (μ : Measure ℝ) (h : Admissible v μ)
(hv0 : 0 < v) (hv1 : v < 1) :
l2ResidualQuadratic μ ≤ rhoEnvelope v := by
have hq0 : (0 : ℝ) < v ^ 2 := by positivity
have hq1 : v ^ 2 < 1 := by nlinarith
have hmom2 : rawMoment μ 2 = v ^ 2 := h.moment2_eq
have hqm : rawMoment μ 2 ≤ rawMoment μ 1 := moment2_le_moment1 h
have hmq_le : (rawMoment μ 1) ^ 2 ≤ rawMoment μ 2 := moment1_sq_le_moment2 h
have hmem := maximizingRoot_mem v hv0 hv1
have hqu : v ^ 2 < maximizingRoot v := hmem.1
have hroot : envelopeQuartic (maximizingRoot v) (v ^ 2) = 0 := maximizingRoot_quartic v hv0 hv1
rcases eq_or_lt_of_le hmq_le with hdeg | hlt
· -- degenerate point-mass case
rw [l2ResidualQuadratic_eq_zero_of_degenerate hdeg]
exact le_of_lt (rhoEnvelope_pos v hv0 hv1)
· -- nondegenerate case: bridge to `momentResidual_le_envelope`
have hu0 : 0 < maximizingRoot v := lt_trans hq0 hqu
have huq : (maximizingRoot v) ^ 2 < v ^ 2 := by nlinarith [hmem.2]
-- `hqm`, `hlt` in `v²`-coordinates:
have hqm' : v ^ 2 ≤ rawMoment μ 1 := by rw [← hmom2]; exact hqm
have hmq' : (rawMoment μ 1) ^ 2 < v ^ 2 := by rw [← hmom2]; exact hlt
have hcross := crossMoment_nonneg h
rw [hmom2] at hcross
have hbound :
momentResidual (rawMoment μ 1) (v ^ 2) (rawMoment μ 3) (rawMoment μ 4)
≤ momentEnvelope (maximizingRoot v) (v ^ 2) :=
momentResidual_le_envelope (rawMoment μ 1) (v ^ 2) (rawMoment μ 3) (rawMoment μ 4)
(maximizingRoot v) hq0 hq1 hqm' hmq' hcross hqu huq hroot
have hres : l2ResidualQuadratic μ
= momentResidual (rawMoment μ 1) (v ^ 2) (rawMoment μ 3) (rawMoment μ 4) := by
unfold l2ResidualQuadratic; rw [hmom2]
rw [hres, rhoEnvelope]
exact hbound
5 supporting declarations (lemmas, instances)
-
finiteMoment4_of_admissibletheorem — Every power y ↦ yᵏ (k ≤ 4) is integrable against an admissible law: on [0,1] we have |yᵏ| ≤ 1, and μ is a finite measure, so Integrable.mono' against the constant 1 applies.Proof (Lean source)
theorem finiteMoment4_of_admissible {v : ℝ} {μ : Measure ℝ} (h : Admissible v μ) : FiniteMoment4 μ := by haveI : IsProbabilityMeasure μ := h.isProb have hintPow (k : ℕ) : Integrable (fun y : ℝ => y ^ k) μ := by refine Integrable.of_bound ((continuous_pow k).aestronglyMeasurable) 1 ?_ filter_upwards [h.supp] with y hy rw [Real.norm_eq_abs, abs_of_nonneg (pow_nonneg hy.1 k)] exact pow_le_one₀ hy.1 hy.2 refine ⟨?_, hintPow 2, hintPow 3, hintPow 4⟩ simpa using hintPow 1 -
moment2_le_moment1theorem — q ≤ m: the second moment is at most the first, because y² ≤ y a.e. on [0,1]. Uses integral_mono_ae on the a.e. support bound plus integrability of y, y².Proof (Lean source)
theorem moment2_le_moment1 {v : ℝ} {μ : Measure ℝ} (h : Admissible v μ) : rawMoment μ 2 ≤ rawMoment μ 1 := by have hfin := finiteMoment4_of_admissible h unfold rawMoment refine integral_mono_ae hfin.int2 ?_ ?_ · simpa [pow_one] using hfin.int1 · filter_upwards [h.supp] with y hy nlinarith [hy.1, hy.2] -
moment1_sq_le_moment2theorem — m² ≤ q: the variance is nonnegative. For a probability measure, (∫ y)² ≤ ∫ y² (Cauchy–Schwarz / Jensen).Proof (Lean source)
theorem moment1_sq_le_moment2 {v : ℝ} {μ : Measure ℝ} (h : Admissible v μ) : (rawMoment μ 1) ^ 2 ≤ rawMoment μ 2 := by haveI : IsProbabilityMeasure μ := h.isProb have hfin := finiteMoment4_of_admissible h have hmem : MemLp (fun y : ℝ => y) 2 μ := by refine (memLp_two_iff_integrable_sq (continuous_id.aestronglyMeasurable)).2 ?_ simpa using hfin.int2 have hvar_nonneg := ProbabilityTheory.variance_nonneg (fun y : ℝ => y) μ have hvar_eq : variance (fun y : ℝ => y) μ = (∫ y : ℝ, y ^ 2 ∂μ) - (∫ y : ℝ, y ∂μ) ^ 2 := by rw [ProbabilityTheory.variance_eq_sub hmem] simp [pow_two] have hle : (∫ y : ℝ, y ∂μ) ^ 2 ≤ ∫ y : ℝ, y ^ 2 ∂μ := by rw [hvar_eq] at hvar_nonneg linarith simpa [rawMoment, pow_one] using hle -
crossMoment_nonnegtheorem — 0 ≤ crossMoment m q m₃ m₄. The certificate cross moment equals the integral ∫ y (1 − y) (y − xᵥ)² ∂μ (expand the degree-4 polynomial and integrate term by term, matching the definition of crossMoment); on [0,1] the integrand is ≥ 0, so the integral is ≥ 0.hypothesesconclusionProof (Lean source)
theorem crossMoment_nonneg {v : ℝ} {μ : Measure ℝ} (h : Admissible v μ) : 0 ≤ crossMoment (rawMoment μ 1) (rawMoment μ 2) (rawMoment μ 3) (rawMoment μ 4) := by have hfin := finiteMoment4_of_admissible h set c := extremalMid (rawMoment μ 1) (rawMoment μ 2) have hcross_eq : crossMoment (rawMoment μ 1) (rawMoment μ 2) (rawMoment μ 3) (rawMoment μ 4) = ∫ y, y * (1 - y) * (y - c) ^ 2 ∂μ := by unfold crossMoment rawMoment change -∫ y, y ^ 4 ∂μ + (1 + 2 * c) * ∫ y, y ^ 3 ∂μ - (2 * c + c ^ 2) * ∫ y, y ^ 2 ∂μ + c ^ 2 * ∫ y, y ^ 1 ∂μ = ∫ y, y * (1 - y) * (y - c) ^ 2 ∂μ have hpoly : (fun y : ℝ => y * (1 - y) * (y - c) ^ 2) = fun y : ℝ => ((((-1 : ℝ) * y ^ 4 + (1 + 2 * c) * y ^ 3) + (-(2 * c + c ^ 2)) * y ^ 2) + c ^ 2 * y) := by funext y ring rw [hpoly] have hi4 : Integrable (fun y : ℝ => (-1 : ℝ) * y ^ 4) μ := hfin.int4.const_mul _ have hi3 : Integrable (fun y : ℝ => (1 + 2 * c) * y ^ 3) μ := hfin.int3.const_mul _ have hi2 : Integrable (fun y : ℝ => (-(2 * c + c ^ 2)) * y ^ 2) μ := hfin.int2.const_mul _ have hi1 : Integrable (fun y : ℝ => c ^ 2 * y) μ := hfin.int1.const_mul _ have hs1 : Integrable (fun y : ℝ => (-1 : ℝ) * y ^ 4 + (1 + 2 * c) * y ^ 3) μ := hi4.add hi3 have hs2 : Integrable (fun y : ℝ => ((-1 : ℝ) * y ^ 4 + (1 + 2 * c) * y ^ 3) + (-(2 * c + c ^ 2)) * y ^ 2) μ := hs1.add hi2 rw [MeasureTheory.integral_add hs2 hi1] rw [MeasureTheory.integral_add hs1 hi2] rw [MeasureTheory.integral_add hi4 hi3] simp [MeasureTheory.integral_mul_const, MeasureTheory.integral_neg, mul_comm, pow_one] ring rw [hcross_eq] refine integral_nonneg_of_ae ?_ filter_upwards [h.supp] with y hy exact mul_nonneg (mul_nonneg hy.1 (by linarith [hy.2])) (sq_nonneg (y - c)) -
l2ResidualQuadratic_eq_zero_of_degeneratetheorem — In the degenerate case m² = q the closed-form residual is 0 (the Hankel ratio's denominator m₁² − m₂ vanishes, so momentResidual _ _ _ _ = _ / 0 = 0).hypothesesconclusionl2ResidualQuadratic μ = 0Proof (Lean source)
theorem l2ResidualQuadratic_eq_zero_of_degenerate {μ : Measure ℝ} (hdeg : (rawMoment μ 1) ^ 2 = rawMoment μ 2) : l2ResidualQuadratic μ = 0 := by unfold l2ResidualQuadratic momentResidual rw [show (rawMoment μ 1) ^ 2 - rawMoment μ 2 = 0 by rw [hdeg]; ring, div_zero]
Envelope 1 core · 0 supporting This file assembles the bounded-outcome moment problem. ★ rho_envelope_isLUB
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 fromAttainment).interior_quartic_unique_root— the unique interior root of the FOC quartic (fromQuarticRoot).
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).
theorem rho_envelope_isLUB reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
Measure-level sharp envelope (IsLUB). For v strictly between 0 and 1, rhoEnvelope v is the least upper bound of the set of residuals l2ResidualQuadratic μ over admissible laws μ. Equivalently: the sup over all probability measures on [0,1] with ∫ y² ∂μ = v² of the L² residual of y² on span{1, y} equals the closed form ρ(v), and is attained (by the extremal three-point law).
Formal statement
Proof (Lean source)
theorem rho_envelope_isLUB (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) :
IsLUB (residualSet v) (rhoEnvelope v) := by
constructor
· -- `rhoEnvelope v` is an upper bound of the residual set
rintro r ⟨μ, hμ, rfl⟩
exact l2ResidualQuadratic_le_rho v μ hμ hv0 hv1
· -- and it is the least such: any upper bound dominates the attained value
intro b hb
obtain ⟨μ, hμ, hres⟩ := rho_envelope_attained v hv0 hv1
exact hb ⟨μ, hμ, hres.symm⟩
QuarticRoot 1 core · 7 supporting This file proves the root facts used by BoundedOutcomeEnvelope.Defs to define the envelope maximizer. ★ interior_quartic_unique_root
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.
theorem interior_quartic_unique_root reviewed
⚑ flagged
Causalean.Stat.MomentProblems.BoundedOutcomeEnvelope
Unique interior root of the FOC quartic. For v strictly between 0 and 1 (write q = v²), there is a unique μᵥ ∈ (v², v) with envelopeQuartic μᵥ (v²) = 0. This μᵥ is the envelope maximizer selecting ρ(v). Existence is interior_quartic_exists; uniqueness follows from strict antitonicity (strictAntiOn_envelopeQuartic), whose InjOn forces two roots to coincide.
Formal statement
hypotheses
v :
ℝ
hv0 :
0 < v
hv1 :
v < 1
Proof (Lean source)
theorem interior_quartic_unique_root (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) :
∃! u, u ∈ Ioo (v ^ 2) v ∧ envelopeQuartic u (v ^ 2) = 0 := by
obtain ⟨u, hu, hfu⟩ := interior_quartic_exists v hv0 hv1
refine ⟨u, ⟨hu, hfu⟩, ?_⟩
rintro w ⟨hw, hfw⟩
have hinj := (strictAntiOn_envelopeQuartic v hv0 hv1).injOn
exact hinj (Ioo_subset_Icc_self hw) (Ioo_subset_Icc_self hu)
(show envelopeQuartic w (v ^ 2) = envelopeQuartic u (v ^ 2) by rw [hfw, hfu])
7 supporting declarations (lemmas, instances)
-
envelopeQuartic_pos_at_qtheorem — envelopeQuartic q q = q² (1 − q)² > 0 for q ∈ (0,1). This is the positive endpoint of the sign change that locates the interior root.Proof (Lean source)
theorem envelopeQuartic_pos_at_q (q : ℝ) (hq0 : 0 < q) (hq1 : q < 1) : 0 < envelopeQuartic q q := by have hid : envelopeQuartic q q = q ^ 2 * (1 - q) ^ 2 := by unfold envelopeQuartic; ring rw [hid] have h1 : (0 : ℝ) < 1 - q := by linarith positivity -
envelopeQuartic_neg_at_vtheorem — envelopeQuartic v (v²) = −2 v³ (v − 1)² < 0 for v ∈ (0,1). This is the negative endpoint of the sign change (at t = v = √q) that locates the interior root.Proof (Lean source)
theorem envelopeQuartic_neg_at_v (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : envelopeQuartic v (v ^ 2) < 0 := by have hid : envelopeQuartic v (v ^ 2) = -(2 * v ^ 3) * (v - 1) ^ 2 := by unfold envelopeQuartic; ring rw [hid] have hne : (v - 1) ≠ 0 := by intro h; apply absurd hv1; linarith [sub_eq_zero.mp h] have hsq : 0 < (v - 1) ^ 2 := by positivity have hpos : 0 < 2 * v ^ 3 := by positivity nlinarith [mul_pos hpos hsq] -
continuous_envelopeQuartictheorem — The continuous polynomial t ↦ envelopeQuartic t q.Proof (Lean source)
@[fun_prop] theorem continuous_envelopeQuartic (q : ℝ) : Continuous (fun t => envelopeQuartic t q) := by unfold envelopeQuartic; fun_prop -
hasDerivAt_envelopeQuartictheorem — Derivative of the quartic. d/dt envelopeQuartic t q = 4 t³ − 6 t² + 4 q t − 2 q².hypothesest q :ℝconclusionHasDerivAt (fun s => envelopeQuartic s q) (4 * t ^ 3 - 6 * t ^ 2 + 4 * q * t - 2 * q ^ 2) tProof (Lean source)
theorem hasDerivAt_envelopeQuartic (t q : ℝ) : HasDerivAt (fun s => envelopeQuartic s q) (4 * t ^ 3 - 6 * t ^ 2 + 4 * q * t - 2 * q ^ 2) t := by unfold envelopeQuartic -- Sum of monomials; assemble from `hasDerivAt_pow`, `const_mul`, `add`/`sub`. have e1 : HasDerivAt (fun s : ℝ => s ^ 4) (4 * t ^ 3) t := by simpa using hasDerivAt_pow 4 t have hp3 : HasDerivAt (fun s : ℝ => s ^ 3) (3 * t ^ 2) t := by simpa using hasDerivAt_pow 3 t have e2 := hp3.const_mul (2 : ℝ) have hp2 : HasDerivAt (fun s : ℝ => s ^ 2) (2 * t) t := by simpa using hasDerivAt_pow 2 t have e3 := hp2.const_mul (2 * q) have e4 : HasDerivAt (fun s : ℝ => (2 * q ^ 2) * s) (2 * q ^ 2) t := by simpa using (hasDerivAt_id t).const_mul (2 * q ^ 2) have h := (((e1.fun_sub e2).fun_add e3).fun_sub e4).add_const (q ^ 2) exact h.congr_deriv (by ring) -
interior_quartic_existstheorem — Interior existence. For v ∈ (0,1) and q = v², the quartic has a root strictly inside (v², v). Proof: the sign change envelopeQuartic (v²) (v²) > 0, envelopeQuartic v (v²) < 0 plus continuity, via the intermediate value theorem (intermediate_value_Ioo').hypothesesv :ℝhv0 :0 < vhv1 :v < 1conclusion∃ u ∈ Ioo (v ^ 2) v, envelopeQuartic u (v ^ 2) = 0Proof (Lean source)
theorem interior_quartic_exists (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : ∃ u ∈ Ioo (v ^ 2) v, envelopeQuartic u (v ^ 2) = 0 := by have hqv : v ^ 2 < v := by nlinarith have hpos : 0 < envelopeQuartic (v ^ 2) (v ^ 2) := envelopeQuartic_pos_at_q (v ^ 2) (by positivity) (by nlinarith) have hneg : envelopeQuartic v (v ^ 2) < 0 := envelopeQuartic_neg_at_v v hv0 hv1 have hcont : ContinuousOn (fun t => envelopeQuartic t (v ^ 2)) (Icc (v ^ 2) v) := (continuous_envelopeQuartic (v ^ 2)).continuousOn have hmem : (0 : ℝ) ∈ Ioo (envelopeQuartic v (v ^ 2)) (envelopeQuartic (v ^ 2) (v ^ 2)) := ⟨hneg, hpos⟩ have hsub := intermediate_value_Ioo' (le_of_lt hqv) hcont hmem obtain ⟨u, hu, hfu⟩ := hsub exact ⟨u, hu, hfu⟩ -
envelopeQuartic_deriv_negtheorem — Strict negativity of the derivative on (v², v). For v ∈ (0,1) and t ∈ (v², v), 4 t³ − 6 t² + 4 v² t − 2 v⁴ < 0. (This is the derivative of envelopeQuartic · (v²).) Proof: nlinarith from v² < t, t < v, 0 < v, v < 1.hypothesesv t :ℝhv0 :0 < vhv1 :v < 1ht1 :v ^ 2 < tht2 :t < vconclusion4 * t ^ 3 - 6 * t ^ 2 + 4 * (v ^ 2) * t - 2 * (v ^ 2) ^ 2 < 0Proof (Lean source)
theorem envelopeQuartic_deriv_neg (v t : ℝ) (hv0 : 0 < v) (hv1 : v < 1) (ht1 : v ^ 2 < t) (ht2 : t < v) : 4 * t ^ 3 - 6 * t ^ 2 + 4 * (v ^ 2) * t - 2 * (v ^ 2) ^ 2 < 0 := by -- nlinarith with products of the constraint slacks; strengthen hints if needed. have hmain : 4 * t ^ 3 - 6 * t ^ 2 + 4 * (v ^ 2) * t - 2 * (v ^ 2) ^ 2 < 0 := by nlinarith [ mul_pos (sub_pos.2 ht2) (sub_pos.2 ht1), mul_pos (sub_pos.2 ht2) hv0, mul_pos (sub_pos.2 ht1) hv0, mul_pos hv0 hv0, sq_nonneg (t - v), sq_nonneg (t - v ^ 2), mul_pos (mul_pos hv0 hv0) hv0, ht1, ht2, hv0] exact (fun _ : v < 1 => hmain) hv1 -
strictAntiOn_envelopeQuartictheorem — t ↦ envelopeQuartic t (v²) is strictly antitone on Icc (v²) v.hypothesesv :ℝhv0 :0 < vhv1 :v < 1conclusionStrictAntiOn (fun t => envelopeQuartic t (v ^ 2)) (Icc (v ^ 2) v)Proof (Lean source)
theorem strictAntiOn_envelopeQuartic (v : ℝ) (hv0 : 0 < v) (hv1 : v < 1) : StrictAntiOn (fun t => envelopeQuartic t (v ^ 2)) (Icc (v ^ 2) v) := by have hqv : v ^ 2 < v := by nlinarith apply strictAntiOn_of_deriv_neg (convex_Icc _ _) (continuous_envelopeQuartic (v ^ 2)).continuousOn intro t ht rw [interior_Icc] at ht rw [(hasDerivAt_envelopeQuartic t (v ^ 2)).deriv] exact envelopeQuartic_deriv_neg v t hv0 hv1 ht.1 ht.2