The error shape of thm:qld

Blueprint thm:qld states its error in one closed form (lem:qld-error),

δ_qld(ε, m, d, q) = a (md)^a (ε^b + q^{-b} + 2^{-bmd}), for universal constants a ≥ 1, 0 < b < 1.

The proof produces something else: a chain of explicit errors, each a polynomial with square roots in the one before it. deltaQ (lem:qld-combined-points) feeds kappaPairs and deltaPairsD, which feed deltaPairs (lem:qld-pairs-of-lines, at the collision probability md/q + 1/q), which feeds deltaGS (lem:qld-global-success); the seeded soundness theorem turns that into deltaLD = deltaSim q (4m) d 1 deltaGS; deltaS (lem:qld-simultaneous) and deltaSelfCons (lem:qld-pauli-selfcons) follow; and item 1 of lem:qld-swap (MirrorSimul.exists_aux_close) ends in 2 - 2 √(1 - η) with η = 2 √X + 2 X. This file shows every link is of the blueprint's form. It does so with a closure calculus rather than by bounding the composite in one go, so that item 2's bound, built from the same operations, joins the class by the same combinators.

The class

ErrSmall f says that there are a ≥ 1 and 0 < b < 1 with 0 ≤ f ε m d q ≤ errShape a b ε m d q at every tuple with 0 ≤ ε ≤ 1, m, d ≥ 1, q ≥ 2. The constants are quantified first: they may not depend on the parameters, which is what "universal" means in the blueprint. The range costs nothing. q ≥ 2 because q = |F|, and ε ≤ 1 because a failure probability above one may be read as one, the shape being monotone in ε (ErrSmall.exists_le_min_one).

Why it is closed

Write S_b = ε^b + q^{-b} + 2^{-bmd} (errSum). Three facts do all the work.

• On the range S_b is antitone in b, since ε ≤ 1 ≤ q, and (md)^a is monotone in a, since md ≥ 1. So two errors with different constants are both below the shape at the larger a and the smaller b: sums, nonnegative constant multiples and polynomial prefactors (md)^r.
• t ↦ t^B is subadditive for 0 < B ≤ 1 (Real.rpow_add_le_add_rpow), while a^B ≤ a and ((md)^a)^B ≤ (md)^a; so (a (md)^a S_b)^B ≤ a (md)^a S_{bB}. Square roots are B = 1/2. This is the only operation that shrinks the exponent, and the chain applies it a fixed finite number of times, which is why b stays universal.
• Each term of S_b is at most one on the range, so S_b ≤ 3 and S_b · S_b ≤ 3 S_b: products.

What is not in the class is a positive constant (not_errSmall_one, which also guards the definition against being vacuous): at fixed m, d the shape tends to a (md)^a 2^{-bmd} as q → ∞ and ε → 0, and that tends to zero with md. So every constant in the chain has to arrive multiplied by something small, and it does: 2/q, (md + 1)/q.

The base cases

ε, since ε ≤ ε^{1/2} on [0, 1]; q^{-B} and 2^{-Bmd} for each B > 0; and md/q = (md) q^{-1}. The seeded soundness theorem enters through ErrSmall.deltaSim_comp: at (q, 4m, d, 1) its error δ_sim is A (4md)^A (x^B + q^{-B} + 2^{-4Bmd}) with A = simA, B = clB, and (4md)^A = 4^A (md)^A, 2^{-4Bmd} ≤ 2^{-Bmd}, so it is small whenever x is. This is the absorption lidtError_le_deltaCL performs for the canonical-line error, run once more. MIPRE/Foundations/Introspection/ErrorBounds.lean does the same kind of normalization for the introspection error, whose shape a (x^a ε^b + x^{-b}) has no 2^{-bmd} term.

Item 1, and the trivial bound

2 - 2 √(1 - η) ≤ 2 η for every η ≥ 0 (two_sub_two_sqrt_one_sub): for η ≤ 1 because √t ≥ t on [0, 1], and for η > 1 because Real.sqrt of a negative number is 0. So item 1's bound is small as soon as η is (errSmall_swapItemOne), and that holds whether or not item 1's hypothesis η < 1 does.

Where that hypothesis, or the regime 48 m d ≤ q, fails, thm:qld takes the trivial bound. ErrSmall.of_cases and ErrSmall.of_regime say that this is free: a bounded error that is small wherever a small quantity g is below one is small, since C ≤ C g where it is not; and outside k m d ≤ q the small quantity k md/q exceeds one.

The shape

noncomputable def MIPRE.QLD.errShape (a b ε : ℝ) (m d q : ℕ) : ℝ

The shape of δ_qld (blueprint thm:qld): a (md)^a (ε^b + q^{-b} + 2^{-bmd}).

Equations

• MIPRE.QLD.errShape a b ε m d q = a * (↑m * ↑d) ^ a * (ε ^ b + ↑q ^ (-b) + 2 ^ (-(b * ↑m * ↑d)))

def MIPRE.QLD.ErrSmall (f : ℝ → ℕ → ℕ → ℕ → ℝ) : Prop

An error of the shape of thm:qld. There are universal constants a ≥ 1 and 0 < b < 1 such that, at every parameter tuple with 0 ≤ ε ≤ 1, m, d ≥ 1 and q ≥ 2, the error is nonnegative and at most errShape a b ε m d q. The constants come first: they may not depend on ε, m, d or q.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.QLD.errSum (b ε : ℝ) (m d q : ℕ) : ℝ

The bracket of the shape.

Equations

• MIPRE.QLD.errSum b ε m d q = ε ^ b + ↑q ^ (-b) + 2 ^ (-(b * ↑m * ↑d))

theorem MIPRE.QLD.errShape_eq (a b ε : ℝ) (m d q : ℕ) : errShape a b ε m d q = a * (↑m * ↑d) ^ a * errSum b ε m d q

theorem MIPRE.QLD.errSum_nonneg {ε : ℝ} (b : ℝ) (hε : 0 ≤ ε) (m d q : ℕ) : 0 ≤ errSum b ε m d q

theorem MIPRE.QLD.one_le_md_real {m d : ℕ} (hm : 1 ≤ m) (hd : 1 ≤ d) : 1 ≤ ↑m * ↑d

theorem MIPRE.QLD.one_le_q_real {q : ℕ} (hq : 2 ≤ q) : 1 ≤ ↑q

theorem MIPRE.QLD.errSum_anti {ε : ℝ} {m d q : ℕ} {b b' : ℝ} (hb' : 0 < b') (hbb : b' ≤ b) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hq : 1 ≤ ↑q) : errSum b ε m d q ≤ errSum b' ε m d q

A smaller exponent makes every term larger, since ε ≤ 1 ≤ q and 2 > 1.

theorem MIPRE.QLD.errSum_le_three {ε : ℝ} {m d q : ℕ} {b : ℝ} (hb : 0 ≤ b) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hq : 1 ≤ ↑q) : errSum b ε m d q ≤ 3

Each of the three terms is at most one, so the bracket is at most three.

theorem MIPRE.QLD.errSum_rpow_le {ε : ℝ} {m d q : ℕ} {b B : ℝ} (hB0 : 0 ≤ B) (hB1 : B ≤ 1) (hε0 : 0 ≤ ε) : errSum b ε m d q ^ B ≤ errSum (b * B) ε m d q

A power t ↦ t^B, 0 ≤ B ≤ 1, of the bracket is below the bracket at exponent bB: t ↦ t^B is subadditive.

The shape is closed under the operations the chain uses

theorem MIPRE.QLD.errShape_nonneg {ε : ℝ} {m d q : ℕ} {a b : ℝ} (ha : 0 ≤ a) (hε : 0 ≤ ε) : 0 ≤ errShape a b ε m d q

theorem MIPRE.QLD.md_rpow_mono {m d : ℕ} (hmd : 1 ≤ ↑m * ↑d) {r r' : ℝ} (h : r ≤ r') : (↑m * ↑d) ^ r ≤ (↑m * ↑d) ^ r'

theorem MIPRE.QLD.one_le_md_rpow {m d : ℕ} (hmd : 1 ≤ ↑m * ↑d) {r : ℝ} (hr : 0 ≤ r) : 1 ≤ (↑m * ↑d) ^ r

theorem MIPRE.QLD.errSum_le_errShape {ε : ℝ} {m d q : ℕ} {a b : ℝ} (ha : 1 ≤ a) (hε : 0 ≤ ε) (hmd : 1 ≤ ↑m * ↑d) : errSum b ε m d q ≤ errShape a b ε m d q

The bracket alone is of the shape, for any a ≥ 1.

theorem MIPRE.QLD.errShape_mono {ε : ℝ} {m d q : ℕ} {a a' b b' : ℝ} (ha : 1 ≤ a) (haa : a ≤ a') (hb' : 0 < b') (hbb : b' ≤ b) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hmd : 1 ≤ ↑m * ↑d) (hq : 1 ≤ ↑q) : errShape a b ε m d q ≤ errShape a' b' ε m d q

Weakening the constants: a larger a and a smaller b give a larger shape.

theorem MIPRE.QLD.errShape_add {ε : ℝ} {m d q : ℕ} {a₁ a₂ b₁ b₂ : ℝ} (ha₁ : 1 ≤ a₁) (ha₂ : 1 ≤ a₂) (hb₁ : 0 < b₁) (hb₂ : 0 < b₂) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hmd : 1 ≤ ↑m * ↑d) (hq : 1 ≤ ↑q) : errShape a₁ b₁ ε m d q + errShape a₂ b₂ ε m d q ≤ errShape (a₁ + a₂) (min b₁ b₂) ε m d q

Sums.

theorem MIPRE.QLD.errShape_const_mul {ε : ℝ} {m d q : ℕ} {a b c : ℝ} (ha : 1 ≤ a) (hc : 0 ≤ c) (hε0 : 0 ≤ ε) (hmd : 1 ≤ ↑m * ↑d) : c * errShape a b ε m d q ≤ errShape ((c + 1) * a) b ε m d q

Constant multiples.

theorem MIPRE.QLD.mdpow_mul_errShape {ε : ℝ} {m d q : ℕ} {a b r : ℝ} (ha : 1 ≤ a) (hr : 0 ≤ r) (hε0 : 0 ≤ ε) (hmd : 1 ≤ ↑m * ↑d) : (↑m * ↑d) ^ r * errShape a b ε m d q ≤ errShape (a + r) b ε m d q

Polynomial prefactors (md)^r, r ≥ 0.

theorem MIPRE.QLD.errShape_rpow_le {ε : ℝ} {m d q : ℕ} {a b B : ℝ} (ha : 1 ≤ a) (hB0 : 0 ≤ B) (hB1 : B ≤ 1) (hε0 : 0 ≤ ε) (hmd : 1 ≤ ↑m * ↑d) : errShape a b ε m d q ^ B ≤ errShape a (b * B) ε m d q

Powers t ↦ t^B, 0 ≤ B ≤ 1: the prefactor only shrinks, and the bracket is subadditive. The exponent becomes bB.

theorem MIPRE.QLD.errShape_mul {ε : ℝ} {m d q : ℕ} {a₁ a₂ b₁ b₂ : ℝ} (ha₁ : 1 ≤ a₁) (ha₂ : 1 ≤ a₂) (hb₁ : 0 < b₁) (hb₂ : 0 < b₂) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hmd : 1 ≤ ↑m * ↑d) (hq : 1 ≤ ↑q) : errShape a₁ b₁ ε m d q * errShape a₂ b₂ ε m d q ≤ errShape (3 * a₁ * a₂) (min b₁ b₂) ε m d q

Products: every term of the bracket is at most one, so the product of two brackets is at most three times the bracket at the smaller exponent.

The class ErrSmall and its closure

theorem MIPRE.QLD.ErrSmall.mono {f g : ℝ → ℕ → ℕ → ℕ → ℝ} (hg : ErrSmall g) (h : ∀ (ε : ℝ) (m d q : ℕ), 0 ≤ ε → ε ≤ 1 → 1 ≤ m → 1 ≤ d → 2 ≤ q → 0 ≤ f ε m d q ∧ f ε m d q ≤ g ε m d q) : ErrSmall f

Monotonicity: a nonnegative error below a small one is small.

theorem MIPRE.QLD.ErrSmall.congr {f g : ℝ → ℕ → ℕ → ℕ → ℝ} (hg : ErrSmall g) (h : ∀ (ε : ℝ) (m d q : ℕ), 0 ≤ ε → ε ≤ 1 → 1 ≤ m → 1 ≤ d → 2 ≤ q → f ε m d q = g ε m d q) : ErrSmall f

An error equal to a small one on the parameter range is small.

theorem MIPRE.QLD.ErrSmall.nonneg {f : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) {ε : ℝ} {m d q : ℕ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hm : 1 ≤ m) (hd : 1 ≤ d) (hq : 2 ≤ q) : 0 ≤ f ε m d q

A small error is nonnegative on the parameter range.

theorem MIPRE.QLD.ErrSmall.add {f g : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) (hg : ErrSmall g) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => f ε m d q + g ε m d q

Sums.

theorem MIPRE.QLD.ErrSmall.const_mul {f : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) {c : ℝ} (hc : 0 ≤ c) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => c * f ε m d q

Constant multiples, by a nonnegative constant.

theorem MIPRE.QLD.ErrSmall.div_const {f : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) {c : ℝ} (hc : 0 ≤ c) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => f ε m d q / c

Division by a nonnegative constant (at c = 0 the quotient is 0).

theorem MIPRE.QLD.ErrSmall.mdpow_mul {f : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) {r : ℝ} (hr : 0 ≤ r) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => (↑m * ↑d) ^ r * f ε m d q

Polynomial prefactors (md)^r, r ≥ 0.

theorem MIPRE.QLD.ErrSmall.md_mul {f : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => ↑m * ↑d * f ε m d q

The polynomial prefactor md.

theorem MIPRE.QLD.ErrSmall.rpow {f : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) {B : ℝ} (hB0 : 0 < B) (hB1 : B ≤ 1) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => f ε m d q ^ B

Powers t ↦ t^B, 0 < B ≤ 1. The exponent b becomes bB.

theorem MIPRE.QLD.ErrSmall.sqrt {f : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => √(f ε m d q)

Square roots.

theorem MIPRE.QLD.ErrSmall.mul {f g : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) (hg : ErrSmall g) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => f ε m d q * g ε m d q

Products.

theorem MIPRE.QLD.ErrSmall.of_le_errSum {f : ℝ → ℕ → ℕ → ℕ → ℝ} {b : ℝ} (hb0 : 0 < b) (hb1 : b < 1) (h : ∀ (ε : ℝ) (m d q : ℕ), 0 ≤ ε → ε ≤ 1 → 1 ≤ m → 1 ≤ d → 2 ≤ q → 0 ≤ f ε m d q ∧ f ε m d q ≤ errSum b ε m d q) : ErrSmall f

The bracket's own terms. An error below the bracket ε^b + q^{-b} + 2^{-bmd} at a fixed 0 < b < 1 is small, with a = 1.

The class is not trivial

A guard on the definition, since everything else rests on it: a positive constant is not small. At ε = 0, m = 1 the shape is a d^a (q^{-b} + 2^{-bd}), and taking first d and then q large makes it as small as desired.

theorem MIPRE.QLD.not_errSmall_one : ¬ErrSmall fun (x : ℝ) (x_1 x_2 x_3 : ℕ) => 1

The constant 1 is not small.

The base cases

theorem MIPRE.QLD.errSmall_eps : ErrSmall fun (ε : ℝ) (x x_1 x_2 : ℕ) => ε

ε is small: ε ≤ ε^{1/2} on [0, 1].

theorem MIPRE.QLD.errSmall_sqrt_eps : ErrSmall fun (ε : ℝ) (x x_1 x_2 : ℕ) => √ε

√ε is small.

theorem MIPRE.QLD.errSmall_q_rpow_neg {B : ℝ} (hB : 0 < B) : ErrSmall fun (x : ℝ) (x_1 x_2 q : ℕ) => ↑q ^ (-B)

q^{-B} is small for every B > 0.

theorem MIPRE.QLD.errSmall_inv_q : ErrSmall fun (x : ℝ) (x_1 x_2 q : ℕ) => (↑q)⁻¹

1/q is small.

theorem MIPRE.QLD.errSmall_two_rpow_neg {B : ℝ} (hB : 0 < B) : ErrSmall fun (x : ℝ) (m d x_1 : ℕ) => 2 ^ (-(B * ↑m * ↑d))

2^{-Bmd} is small for every B > 0.

theorem MIPRE.QLD.errSmall_md_div_q : ErrSmall fun (x : ℝ) (m d q : ℕ) => ↑m * ↑d / ↑q

md/q is small: the collision probability of an axis-parallel line.

theorem MIPRE.QLD.errSmall_const_div_q {c : ℝ} (hc : 0 ≤ c) : ErrSmall fun (x : ℝ) (x_1 x_2 q : ℕ) => c / ↑q

c/q is small for every c ≥ 0.

theorem MIPRE.QLD.ErrSmall.m_mul_m_mul {f : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => ↑m * ↑m * f ε m d q

The prefactor m², which δ_GS carries: m² ≤ (md)².

The chain

theorem MIPRE.QLD.errSmall_deltaQ : ErrSmall fun (ε : ℝ) (x x_1 x_2 : ℕ) => deltaQ ε

δ_Q, the error of lem:qld-combined-points.

theorem MIPRE.QLD.errSmall_kappaPairs : ErrSmall fun (ε : ℝ) (x x_1 x_2 : ℕ) => kappaPairs ε

theorem MIPRE.QLD.errSmall_deltaPairsD : ErrSmall fun (ε : ℝ) (x x_1 x_2 : ℕ) => deltaPairsD ε

theorem MIPRE.QLD.ErrSmall.deltaPairs_comp {g : ℝ → ℕ → ℕ → ℕ → ℝ} (hg : ErrSmall g) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => deltaPairs ε (g ε m d q)

δ_P, the error of lem:qld-pairs-of-lines, at any small collision probability.

theorem MIPRE.QLD.errSmall_deltaGS : ErrSmall fun (ε : ℝ) (m d q : ℕ) => deltaGS q m d ε

δ_GS, the padded strategy's failure in the seeded test (lem:qld-global-success).

theorem MIPRE.QLD.deltaSim_four_mul_le {q m d : ℕ} {x : ℝ} (hx : 0 ≤ x) : LIDT.Simul.deltaSim q (4 * m) d 1 x ≤ LIDT.Simul.simA * 4 ^ LIDT.Simul.simA * ((↑m * ↑d) ^ LIDT.Simul.simA * (x ^ LIDT.clB + ↑q ^ (-LIDT.clB) + 2 ^ (-(LIDT.clB * ↑m * ↑d))))

δ_sim at (q, 4m, d, 1) is of the shape, with 4m read as m: (4md)^A = 4^A (md)^A, and 2^{-B·4md} ≤ 2^{-Bmd}.

theorem MIPRE.QLD.ErrSmall.deltaSim_comp {g : ℝ → ℕ → ℕ → ℕ → ℝ} (hg : ErrSmall g) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => LIDT.Simul.deltaSim q (4 * m) d 1 (g ε m d q)

The seeded soundness theorem's error at (q, 4m, d, 1), fed a small failure probability, is small.

theorem MIPRE.QLD.errSmall_deltaLD : ErrSmall fun (ε : ℝ) (m d q : ℕ) => deltaLD q m d ε

δ_ld, the seeded soundness theorem's error on the padded strategy (lem:qld-global-pvm).

theorem MIPRE.QLD.ErrSmall.deltaS_comp {g : ℝ → ℕ → ℕ → ℕ → ℝ} (hg : ErrSmall g) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => deltaS q (g ε m d q) ε

δ_S, the error of lem:qld-simultaneous, at any small GlobalPair error.

theorem MIPRE.QLD.errSmall_deltaS : ErrSmall fun (ε : ℝ) (m d q : ℕ) => deltaS q (deltaLD q m d ε) ε

δ_S of the chain: the error of the MirrorSimul that exists_mirrorSimul builds.

theorem MIPRE.QLD.ErrSmall.deltaSelfCons_comp {g : ℝ → ℕ → ℕ → ℕ → ℝ} (hg : ErrSmall g) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => deltaSelfCons (g ε m d q) ε m d q

The constant of lem:qld-pauli-selfcons, at any small MirrorSimul error.

theorem MIPRE.QLD.errSmall_deltaSelfCons : ErrSmall fun (ε : ℝ) (m d q : ℕ) => deltaSelfCons (deltaS q (deltaLD q m d ε) ε) ε m d q

The constant of lem:qld-pauli-selfcons along the chain.

Item 1 of lem:qld-swap

theorem MIPRE.QLD.two_sub_two_sqrt_one_sub {η : ℝ} (hη : 0 ≤ η) : 0 ≤ 2 - 2 * √(1 - η) ∧ 2 - 2 * √(1 - η) ≤ 2 * η

2 - 2 √(1 - η) ≤ 2 η for every η ≥ 0, and it is nonnegative. For η ≤ 1 because √t ≥ t on [0, 1]; for η > 1 because Real.sqrt of a negative number is 0.

theorem MIPRE.QLD.ErrSmall.itemOne_comp {g : ℝ → ℕ → ℕ → ℕ → ℝ} (hg : ErrSmall g) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => 2 - 2 * √(1 - (2 * √(g ε m d q) + 2 * g ε m d q))

Item 1's bound, at any small constant.

theorem MIPRE.QLD.errSmall_itemOneEta : ErrSmall fun (ε : ℝ) (m d q : ℕ) => 2 * √(deltaSelfCons (deltaS q (deltaLD q m d ε) ε) ε m d q) + 2 * deltaSelfCons (deltaS q (deltaLD q m d ε) ε) ε m d q

The quantity η = 2 √X + 2 X item 1 asks to be below one, at the chain's X.

theorem MIPRE.QLD.errSmall_swapItemOne : ErrSmall fun (ε : ℝ) (m d q : ℕ) => 2 - 2 * √(1 - (2 * √(deltaSelfCons (deltaS q (deltaLD q m d ε) ε) ε m d q) + 2 * deltaSelfCons (deltaS q (deltaLD q m d ε) ε) ε m d q))

Item 1 of lem:qld-swap has the error shape of thm:qld. The bound MirrorSimul.exists_aux_close gives on ‖endState - aux ⊗ EPR‖², at the MirrorSimul that exists_mirrorSimul builds, is at most a (md)^a (ε^b + q^{-b} + 2^{-bmd}) for universal constants a ≥ 1 and 0 < b < 1.

theorem MIPRE.QLD.errSmall_swapItemOne_sqrt : ErrSmall fun (ε : ℝ) (m d q : ℕ) => √(2 - 2 * √(1 - (2 * √(deltaSelfCons (deltaS q (deltaLD q m d ε) ε) ε m d q) + 2 * deltaSelfCons (deltaS q (deltaLD q m d ε) ε) ε m d q)))

The same for the distance itself, rather than its square.

Trivial bounds outside a regime

Two moves the proof of thm:qld makes on top of the chain: outside the regime where the chain applies it takes the trivial bound, and it reads a failure probability ε > 1 as ε = 1.

theorem MIPRE.QLD.ErrSmall.of_cases {f g h : ℝ → ℕ → ℕ → ℕ → ℝ} (hh : ErrSmall h) (hg : ErrSmall g) {C : ℝ} (hC : 0 ≤ C) (hf : ∀ (ε : ℝ) (m d q : ℕ), 0 ≤ ε → ε ≤ 1 → 1 ≤ m → 1 ≤ d → 2 ≤ q → 0 ≤ f ε m d q ∧ f ε m d q ≤ C ∧ (g ε m d q < 1 → f ε m d q ≤ h ε m d q)) : ErrSmall f

A bounded error that is small wherever a small quantity is below one is small. Where g ≥ 1 the trivial bound C ≤ C g is itself small.

theorem MIPRE.QLD.ErrSmall.of_regime {f h : ℝ → ℕ → ℕ → ℕ → ℝ} (hh : ErrSmall h) (k : ℕ) {C : ℝ} (hC : 0 ≤ C) (hf : ∀ (ε : ℝ) (m d q : ℕ), 0 ≤ ε → ε ≤ 1 → 1 ≤ m → 1 ≤ d → 2 ≤ q → 0 ≤ f ε m d q ∧ f ε m d q ≤ C ∧ (k * m * d ≤ q → f ε m d q ≤ h ε m d q)) : ErrSmall f

The regime k m d ≤ q. A bounded error that is small wherever k m d ≤ q is small: outside the regime 1 < k m d / q, which is small.

theorem MIPRE.QLD.errShape_mono_eps {a b ε ε' : ℝ} {m d q : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hε : 0 ≤ ε) (hεε : ε ≤ ε') : errShape a b ε m d q ≤ errShape a b ε' m d q

The shape is monotone in ε, so a bound at min ε 1 is a bound at ε.

theorem MIPRE.QLD.ErrSmall.exists_le_min_one {f : ℝ → ℕ → ℕ → ℕ → ℝ} (hf : ErrSmall f) : ∃ (a : ℝ) (b : ℝ), 1 ≤ a ∧ 0 < b ∧ b < 1 ∧ ∀ (ε : ℝ) (m d q : ℕ), 0 ≤ ε → 1 ≤ m → 1 ≤ d → 2 ≤ q → 0 ≤ f (min ε 1) m d q ∧ f (min ε 1) m d q ≤ errShape a b ε m d q

The bound at every ε ≥ 0: a small error, evaluated at min ε 1, is below the shape at ε. A strategy's failure probability is at most one, so min ε 1 is as good a failure bound as ε.