Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Test.MainTheorem.ScalarBounds.EnvelopeBounds

Error cascade — envelope and root bounding machinery #

Internal helper lemmas for the error-cascade bookkeeping of Step 8. These provide the step-envelope interpolation (stepEnvelope), monotonicity under denominator enlargement, square-root scaling, and explicit numeric bounds on various rpow and sqrt expressions. All lemmas are technical and should not be part of downstream API.

References #

references/ldt-paper/inductive_step.tex, lines 187–234.

noncomputable def MIPStarRE.LDT.Test.stepEnvelope (params : Parameters) (k : ℕ) (eps n N : Error) :

A paper-local envelope with exponent 1/n and decay scale N.

Equations

MIPStarRE.LDT.Test.stepEnvelope params k eps n N = Real.rpow eps (1 / n) + Real.rpow (↑params.d / ↑params.q) (1 / n) + Real.exp (-(↑k / (N * ↑params.m ^ 2)))

Instances For

theorem MIPStarRE.LDT.Test.mainFormalEnvelope_eq_stepEnvelope (params : Parameters) (k : ℕ) (eps : Error) :

mainFormalEnvelope params k eps = stepEnvelope params k eps 40000 2560000

theorem MIPStarRE.LDT.Test.rpow_le_of_denom_le {x : Error} (hx : 0 ≤ x) (hx1 : x ≤ 1) {n₁ n₂ : Error} (hn₁Pos : 0 < n₁) (hn : n₁ ≤ n₂) :

Real.rpow x (1 / n₁) ≤ Real.rpow x (1 / n₂)

For x ∈ [0, 1], enlarging the denominator in x^(1/n) makes the exponent smaller and therefore the value larger.

theorem MIPStarRE.LDT.Test.exp_neg_le_of_denom_ge (k : ℕ) (m : Error) (hm : 0 < m) {N₁ N₂ : Error} (h₁ : 0 < N₁) (h₁₂ : N₁ ≤ N₂) :

Real.exp (-(↑k / (N₁ * m ^ 2))) ≤ Real.exp (-(↑k / (N₂ * m ^ 2)))

For k ≥ 0, m > 0, and N₁ ≤ N₂, the larger decay denominator gives the weaker exponential bound exp(-k/(N₁ m²)) ≤ exp(-k/(N₂ m²)).

theorem MIPStarRE.LDT.Test.stepEnvelope_nonneg {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {n N : Error} :

0 ≤ stepEnvelope params k eps n N

theorem MIPStarRE.LDT.Test.stepEnvelope_le_stepEnvelope {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {n₁ n₂ N₁ N₂ : Error} (hn₁Pos : 0 < n₁) (hn : n₁ ≤ n₂) (hN₁Pos : 0 < N₁) (hN : N₁ ≤ N₂) :

stepEnvelope params k eps n₁ N₁ ≤ stepEnvelope params k eps n₂ N₂

theorem MIPStarRE.LDT.Test.stepEnvelope_le_mainFormalEnvelope {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {n N : Error} (hnPos : 0 < n) (hn : n ≤ 40000) (hNPos : 0 < N) (hN : N ≤ 2560000) :

stepEnvelope params k eps n N ≤ mainFormalEnvelope params k eps

A paper-local envelope with exponent 1/n and decay scale N is absorbed by mainFormalEnvelope whenever n ≤ 40000 and N ≤ 2560000.

theorem MIPStarRE.LDT.Test.sqrt_rpow_one_div {x n : Error} (hx : 0 ≤ x) (_hn : 0 < n) :

√(Real.rpow x (1 / n)) = Real.rpow x (1 / (2 * n))

theorem MIPStarRE.LDT.Test.sqrt_exp_neg_div (k : ℕ) (m N : Error) (hm : 0 < m) (hN : 0 < N) :

√(Real.exp (-(↑k / (N * m ^ 2)))) = Real.exp (-(↑k / (2 * N * m ^ 2)))

theorem MIPStarRE.LDT.Test.sqrt_stepEnvelope_le {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {n N : Error} (hn : 0 < n) (hN : 0 < N) :

√(stepEnvelope params k eps n N) ≤ stepEnvelope params k eps (2 * n) (2 * N)

theorem MIPStarRE.LDT.Test.stepEnvelope_le_sq_stepEnvelope {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {n N : Error} (hn : 0 < n) (hN : 0 < N) :

stepEnvelope params k eps n N ≤ stepEnvelope params k eps (2 * n) (2 * N) ^ 2

theorem MIPStarRE.LDT.Test.self_le_rpow_one_div {x : Error} (hx : 0 ≤ x) (hx1 : x ≤ 1) {n : Error} (hn : 1 ≤ n) :

x ≤ Real.rpow x (1 / n)

theorem MIPStarRE.LDT.Test.m_le_k2m4_aux {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) :

↑params.m ≤ ↑k ^ 2 * ↑params.m ^ 4

theorem MIPStarRE.LDT.Test.dq_le_rpow2048 {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) :

↑params.d / ↑params.q ≤ Real.rpow (↑params.d / ↑params.q) (1 / 2048)

theorem MIPStarRE.LDT.Test.dq_rpow2048_le_stepEnvelope2048 {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) :

Real.rpow (↑params.d / ↑params.q) (1 / 2048) ≤ stepEnvelope params k eps 2048 160000

theorem MIPStarRE.LDT.Test.mdq_le_k2m4_stepEnvelope2048 {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) :

↑params.m * (↑params.d / ↑params.q) ≤ ↑k ^ 2 * ↑params.m ^ 4 * stepEnvelope params k eps 2048 160000

theorem MIPStarRE.LDT.Test.four_mul_le_k2m4_mul {params : Parameters} {k : ℕ} {eps T : Error} (h : CascadeHypotheses params k eps) (hT : 0 ≤ T) :

4 * T ≤ 4 * (↑k ^ 2 * ↑params.m ^ 4) * T

theorem MIPStarRE.LDT.Test.sqrt_three_le_two :

theorem MIPStarRE.LDT.Test.sqrt20000_le_142 :

√20000 ≤ 142

theorem MIPStarRE.LDT.Test.sqrt20204_le_143 :

√20204 ≤ 143

theorem MIPStarRE.LDT.Test.sqrt150000_le_388 :

√150000 ≤ 388

theorem MIPStarRE.LDT.Test.sqrt170244_le_413 :

√170244 ≤ 413

theorem MIPStarRE.LDT.Test.two_sqrt40005_le_401 :

2 * √40005 ≤ 401

theorem MIPStarRE.LDT.Test.rpow20204_quarter_le_12 :

Real.rpow 20204 (1 / 4) ≤ 12

theorem MIPStarRE.LDT.Test.rpow20204_eighth_le_4 :

Real.rpow 20204 (1 / 8) ≤ 4

theorem MIPStarRE.LDT.Test.k2_rpow_quarter_le {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) :

Real.rpow (↑k ^ 2) (1 / 4) ≤ ↑k

theorem MIPStarRE.LDT.Test.m4_rpow_quarter_eq {params : Parameters} :

Real.rpow (↑params.m ^ 4) (1 / 4) = ↑params.m

theorem MIPStarRE.LDT.Test.k2_rpow_eighth_le {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) :

Real.rpow (↑k ^ 2) (1 / 8) ≤ ↑k

theorem MIPStarRE.LDT.Test.m4_rpow_eighth_le {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) :

Real.rpow (↑params.m ^ 4) (1 / 8) ≤ ↑params.m

theorem MIPStarRE.LDT.Test.rpow_one_four_eq_sqrt_sqrt {x : Error} (hx : 0 ≤ x) :

Real.rpow x (1 / 4) = √√x

theorem MIPStarRE.LDT.Test.rpow_one_eight_eq_sqrt_sqrt_sqrt {x : Error} (hx : 0 ≤ x) :

Real.rpow x (1 / 8) = √√√x

theorem MIPStarRE.LDT.Test.stepEnvelope_rpow_quarter_le {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) :

Real.rpow (stepEnvelope params k eps 2048 160000) (1 / 4) ≤ stepEnvelope params k eps 8192 640000

theorem MIPStarRE.LDT.Test.stepEnvelope_rpow_eighth_le {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) :

Real.rpow (stepEnvelope params k eps 2048 160000) (1 / 8) ≤ stepEnvelope params k eps 16384 1280000

theorem MIPStarRE.LDT.Test.sqrt_scaled_stepEnvelope_le {params : Parameters} {k : ℕ} {eps x C n N : Error} (h : CascadeHypotheses params k eps) (hC : 0 ≤ C) (hx : x ≤ C * ↑k ^ 2 * ↑params.m ^ 4 * stepEnvelope params k eps n N) (hn : 0 < n) (hN : 0 < N) :

√x ≤ √C * ↑k * ↑params.m ^ 2 * stepEnvelope params k eps (2 * n) (2 * N)

theorem MIPStarRE.LDT.Test.rpow_Z1_factor_le {params : Parameters} {k : ℕ} {Z1 k2 m4 E2048 r Crpow Erpow : Error} (hZ1NN : 0 ≤ Z1) (hZ1 : Z1 ≤ 20204 * k2 * m4 * E2048) (hrNN : 0 ≤ r) (hk2NN : 0 ≤ k2) (hm4NN : 0 ≤ m4) (hE2048NN : 0 ≤ E2048) (hA : Real.rpow 20204 r ≤ Crpow) (hB : Real.rpow k2 r ≤ ↑k) (hC : Real.rpow m4 r ≤ ↑params.m) (hD : Real.rpow E2048 r ≤ Erpow) :

Real.rpow Z1 r ≤ Crpow * ↑k * ↑params.m * Erpow