Error cascade — bounds for ζ₂ and ζ₃ #
This module contains the middle cascade estimates used in Step 8 of the main
inductive step: the absorbing bounds for ζ₂ and ζ₃ obtained from the
σ and ζ₁ estimates.
References #
references/ldt-paper/inductive_step.tex, lines 205--217 and 230.
theorem
MIPStarRE.LDT.Test.cascadeZeta2_bound
{params : Parameters}
{k : ℕ}
{eps : Error}
(h : CascadeHypotheses params k eps)
{ν : Error}
(hνNN : 0 ≤ ν)
(hν : ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024)))
:
cascadeZeta2 (cascadeZeta1 params eps (cascadeSigma params k ν)) ≤ 2568 * ↑k * ↑params.m * stepEnvelope params k eps 16384 1280000
theorem
MIPStarRE.LDT.Test.zeta2_bound
{params : Parameters}
{k : ℕ}
{eps : Error}
(h : CascadeHypotheses params k eps)
{ν σ ζ₁ : Error}
(hνNN : 0 ≤ ν)
(hν : ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024)))
(hσEq : σ = cascadeSigma params k ν)
(hζ₁Eq : ζ₁ = cascadeZeta1 params eps σ)
:
Paper lines 205–212, with the formal ζ₂ widening. The concrete ζ₂
built from ζ₁ = cascadeZeta1 params eps σ and σ = cascadeSigma params k ν
is absorbed by mainFormalError.
theorem
MIPStarRE.LDT.Test.cascadeZeta3_bound
{params : Parameters}
{k : ℕ}
{eps : Error}
(h : CascadeHypotheses params k eps)
{ν : Error}
(hνNN : 0 ≤ ν)
(hν : ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024)))
:
cascadeZeta3 (cascadeZeta1 params eps (cascadeSigma params k ν))
(cascadeZeta2 (cascadeZeta1 params eps (cascadeSigma params k ν))) ≤ 150000 * ↑k ^ 2 * ↑params.m ^ 4 * stepEnvelope params k eps 16384 1280000
theorem
MIPStarRE.LDT.Test.zeta3_bound
{params : Parameters}
{k : ℕ}
{eps : Error}
(h : CascadeHypotheses params k eps)
{ν σ ζ₁ ζ₂ : Error}
(hνNN : 0 ≤ ν)
(hν : ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024)))
(hσEq : σ = cascadeSigma params k ν)
(hζ₁Eq : ζ₁ = cascadeZeta1 params eps σ)
(hζ₂Eq : ζ₂ = cascadeZeta2 ζ₁)
:
Paper lines 214–217 and 230. The concrete ζ₃ built from the cascade
chain is rewritten as ζ₃ ≤ 2 · mainFormalError.