The error of thm:qld, named once

Blueprint lem:qld-error, with MIPRE/Background/QLD/ErrorShape.lean.

MirrorSimul.swap_isometry (MIPRE/Background/QLD/SwapItemTwo.lean) closes the swap isometry lemma lem:qld-swap for a legal projective strategy, at the MirrorSimul that exists_mirrorSimul builds. Its two bounds, and the hypothesis it needs, are explicit expressions in the chain's constants. What thm:qld asserts is one function of (ε, m, d, q), of the closed form a (md)^a (ε^b + q^{-b} + 2^{-bmd}) (errShape). This file names that function, qldErr, and proves it is of the closed form (exists_qldErr_le). The assembly of thm:qld then only has to show that each of the theorem's two items is at most qldErr, for which le_qldErr is the interface.

The constants

Along the chain, with q standing for Fintype.card F:

• qldDelta = δ_S(δ_ld), the error of the MirrorSimul that exists_mirrorSimul returns;
• qldHlt = 2 √X + 2 X at X = deltaSelfCons qldDelta, the quantity swap_isometry needs below one (its hypothesis hlt);
• qldEta = etaItemOne qldDelta, item 1's bound on the squared distance to the product state |aux> ⊗ |EPR_q>^M;
• qldBound = deltaItemTwo qldDelta … qldEta + √qldEta.

qldBound is chosen to dominate both items of the theorem at once. Item 1 of thm:qld bounds the distance itself, not its square, so it costs √qldEta (sqrt_qldEta_le_qldBound). Item 2 is item 2 of lem:qld-swap as it stands (itemTwo_le_qldBound): the swap isometry (MirrorSimul.swapPhi) is a local isometry of the strategy's own model, and the measurements item 2 is about are the strategy's own, so nothing follows it. The matrix statement this replaces was about an arbitrary POVM strategy, conjugated by an embedding of its space, and paid 8 √qldEta for the descent from its projective dilation to the POVM; a strategy in a model is projective, and that descent is gone.

Outside the regime

Two hypotheses stand between a strategy and swap_isometry: the regime 48 m d ≤ q, which exists_mirrorSimul needs (the paper's appendix works under 16 m d ≤ q; the constant 48 is where lem:qld-global-separate is formalized, GlobalPair.one_sub_two_eta_ge), and qldHlt < 1. Where either fails, thm:qld takes a trivial bound: the distance between two unit vectors is at most 2, and the summed squared distance between two projective measurements on a unit vector is at most 4 (BipartiteModel.sum_stateSqNorm_sub_le_four). The cap is 4, the paper's bound on the state-dependent distance between any two POVMs. So qldErr is min qldBound 4 inside and 4 outside (qldErr_of_regime, qldErr_of_not).

That this costs nothing is ErrSmall.of_cases at the small quantity g = 48 md/q + qldHlt: where g < 1 both hypotheses hold, since each summand is nonnegative; and where g ≥ 1 the constant 4 is at most 4 g, which is itself of the shape. This is the paper's own move in the proof of thm:pauli-appendix --- enlarge a until the shape exceeds the trivial bound outside the regime --- written as a closure property rather than a choice of a. The min … 4 inside is what makes qldErr bounded everywhere, which of_cases needs.

Why every link is small

qldDelta is errSmall_deltaS, qldHlt is errSmall_itemOneEta and qldEta is errSmall_swapItemOne, all from MIPRE/Background/QLD/ErrorShape.lean. The two constants of item 2 join by the same combinators: deltaLegs δ is linear in δ, ε, √(688 ε) and md/q (ErrSmall.deltaLegs_comp), and deltaItemTwo is linear in deltaLegs, md/q and √η (ErrSmall.deltaItemTwo_comp). Nonnegativity, which the assembly needs at every ε ≥ 0 and not only on [0, 1], is proved directly (qldDelta_nonneg, qldHlt_nonneg, qldEta_nonneg, ...).

The constants

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

δ of the MirrorSimul the chain builds: δ_S at the GlobalPair error δ_ld, as exists_mirrorSimul returns it.

Equations

• MIPRE.QLD.qldDelta ε m d q = MIPRE.QLD.deltaS q (MIPRE.QLD.deltaLD q m d ε) ε

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

The quantity swap_isometry needs below one (its hypothesis hlt): 2 √X + 2 X at X = deltaSelfCons qldDelta.

Equations

• MIPRE.QLD.qldHlt ε m d q = 2 * √(MIPRE.QLD.deltaSelfCons (MIPRE.QLD.qldDelta ε m d q) ε m d q) + 2 * MIPRE.QLD.deltaSelfCons (MIPRE.QLD.qldDelta ε m d q) ε m d q

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

Item 1's bound on the squared distance to |aux> ⊗ |EPR_q>^M, along the chain.

Equations

• MIPRE.QLD.qldEta ε m d q = MIPRE.QLD.etaItemOne (MIPRE.QLD.qldDelta ε m d q) ε m d q

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

The bound on both items of thm:qld inside the regime: item 2 of lem:qld-swap plus √η, which dominates item 1's √η and item 2's deltaItemTwo.

Equations

• MIPRE.QLD.qldBound ε m d q = MIPRE.QLD.deltaItemTwo (MIPRE.QLD.qldDelta ε m d q) ε m d q (MIPRE.QLD.qldEta ε m d q) + √(MIPRE.QLD.qldEta ε m d q)

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

δ_qld, the error of thm:qld. Inside the regime 48 m d ≤ q where swap_isometry's hypothesis qldHlt < 1 also holds, the chain's bound, capped at the trivial bound 4; outside, the trivial bound.

Equations

• MIPRE.QLD.qldErr ε m d q = if 48 * m * d ≤ q ∧ MIPRE.QLD.qldHlt ε m d q < 1 then min (MIPRE.QLD.qldBound ε m d q) 4 else 4

theorem MIPRE.QLD.qldDelta_eq (ε : ℝ) (m d q : ℕ) : qldDelta ε m d q = deltaS q (deltaLD q m d ε) ε

theorem MIPRE.QLD.qldHlt_eq (ε : ℝ) (m d q : ℕ) : qldHlt ε m d q = 2 * √(deltaSelfCons (qldDelta ε m d q) ε m d q) + 2 * deltaSelfCons (qldDelta ε m d q) ε m d q

theorem MIPRE.QLD.qldEta_eq (ε : ℝ) (m d q : ℕ) : qldEta ε m d q = etaItemOne (qldDelta ε m d q) ε m d q

Nonnegativity, at every ε ≥ 0

theorem MIPRE.QLD.deltaLD_nonneg {ε : ℝ} {q m d : ℕ} (hε : 0 ≤ ε) : 0 ≤ deltaLD q m d ε

theorem MIPRE.QLD.deltaS_nonneg {ε : ℝ} {q : ℕ} {δ : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) : 0 ≤ deltaS q δ ε

theorem MIPRE.QLD.qldDelta_nonneg {ε : ℝ} (hε : 0 ≤ ε) (m d q : ℕ) : 0 ≤ qldDelta ε m d q

theorem MIPRE.QLD.qldHlt_nonneg {ε : ℝ} (hε : 0 ≤ ε) (m d q : ℕ) : 0 ≤ qldHlt ε m d q

theorem MIPRE.QLD.qldEta_nonneg {ε : ℝ} (hε : 0 ≤ ε) (m d q : ℕ) : 0 ≤ qldEta ε m d q

Item 1's bound is nonnegative, and at most twice qldHlt (two_sub_two_sqrt_one_sub).

theorem MIPRE.QLD.qldEta_le_two_mul_qldHlt {ε : ℝ} (hε : 0 ≤ ε) (m d q : ℕ) : qldEta ε m d q ≤ 2 * qldHlt ε m d q

theorem MIPRE.QLD.deltaLegs_nonneg {ε δ : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (m d q : ℕ) : 0 ≤ deltaLegs δ ε m d q

theorem MIPRE.QLD.deltaItemTwo_nonneg {ε δ : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (m d q : ℕ) (η : ℝ) : 0 ≤ deltaItemTwo δ ε m d q η

theorem MIPRE.QLD.qldItemTwo_nonneg {ε : ℝ} (hε : 0 ≤ ε) (m d q : ℕ) : 0 ≤ deltaItemTwo (qldDelta ε m d q) ε m d q (qldEta ε m d q)

Item 2's bound of lem:qld-swap, along the chain, is nonnegative.

theorem MIPRE.QLD.qldBound_nonneg {ε : ℝ} (hε : 0 ≤ ε) (m d q : ℕ) : 0 ≤ qldBound ε m d q

qldBound dominates both items

theorem MIPRE.QLD.sqrt_qldEta_le_qldBound {ε : ℝ} (hε : 0 ≤ ε) (m d q : ℕ) : √(qldEta ε m d q) ≤ qldBound ε m d q

Item 1 of thm:qld: the distance itself, the square root of item 1's bound, is at most qldBound.

theorem MIPRE.QLD.itemTwo_le_qldBound (ε : ℝ) (m d q : ℕ) : deltaItemTwo (qldDelta ε m d q) ε m d q (qldEta ε m d q) ≤ qldBound ε m d q

Item 2 of thm:qld: item 2 of lem:qld-swap is at most qldBound.

qldErr: the chain inside the regime, the trivial bound outside

theorem MIPRE.QLD.qldErr_of_not {ε : ℝ} {m d q : ℕ} (h : ¬(48 * m * d ≤ q ∧ qldHlt ε m d q < 1)) : qldErr ε m d q = 4

Outside the regime, the trivial bound.

theorem MIPRE.QLD.qldErr_of_regime {ε : ℝ} {m d q : ℕ} (hq : 48 * m * d ≤ q) (hlt : qldHlt ε m d q < 1) : qldErr ε m d q = min (qldBound ε m d q) 4

Inside the regime, the chain's bound, capped at the trivial one.

theorem MIPRE.QLD.qldErr_le_four {ε : ℝ} {m d q : ℕ} : qldErr ε m d q ≤ 4

theorem MIPRE.QLD.qldErr_le_qldBound {ε : ℝ} {m d q : ℕ} (hq : 48 * m * d ≤ q) (hlt : qldHlt ε m d q < 1) : qldErr ε m d q ≤ qldBound ε m d q

theorem MIPRE.QLD.qldErr_nonneg {ε : ℝ} {m d q : ℕ} (hε : 0 ≤ ε) : 0 ≤ qldErr ε m d q

theorem MIPRE.QLD.le_qldErr {ε : ℝ} {m d q : ℕ} {x : ℝ} (h4 : x ≤ 4) (hB : 48 * m * d ≤ q → qldHlt ε m d q < 1 → x ≤ qldBound ε m d q) : x ≤ qldErr ε m d q

The interface for the assembly of thm:qld. A quantity that is at most the trivial bound 4, and at most qldBound wherever the chain applies, is at most qldErr.

Every link is small

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

The legs of eq:qld-unitary-5, at any small MirrorSimul error: deltaLegs is linear in δ, ε, √(688 ε) and md/q.

theorem MIPRE.QLD.ErrSmall.deltaItemTwo_comp {g η : ℝ → ℕ → ℕ → ℕ → ℝ} (hg : ErrSmall g) (hη : ErrSmall η) : ErrSmall fun (ε : ℝ) (m d q : ℕ) => deltaItemTwo (g ε m d q) ε m d q (η ε m d q)

Item 2's bound of lem:qld-swap, at any small MirrorSimul error and item-1 bound.

theorem MIPRE.QLD.errSmall_qldDelta : ErrSmall qldDelta

theorem MIPRE.QLD.errSmall_qldHlt : ErrSmall qldHlt

theorem MIPRE.QLD.errSmall_qldEta : ErrSmall qldEta

Item 1's bound, along the chain, is of the shape of thm:qld.

theorem MIPRE.QLD.errSmall_deltaLegs : ErrSmall fun (ε : ℝ) (m d q : ℕ) => deltaLegs (qldDelta ε m d q) ε m d q

theorem MIPRE.QLD.errSmall_deltaItemTwo : ErrSmall fun (ε : ℝ) (m d q : ℕ) => deltaItemTwo (qldDelta ε m d q) ε m d q (qldEta ε m d q)

Item 2's bound, along the chain, is of the shape of thm:qld.

theorem MIPRE.QLD.errSmall_qldBound : ErrSmall qldBound

theorem MIPRE.QLD.errSmall_qldErr : ErrSmall qldErr

δ_qld is of the shape of thm:qld. ErrSmall.of_cases at g = 48 md/q + qldHlt: where g < 1 both summands are below one, so the chain applies and qldErr ≤ qldBound; and qldErr ≤ 4 everywhere.

theorem MIPRE.QLD.exists_qldErr_le : ∃ (a : ℝ) (b : ℝ), 1 ≤ a ∧ 0 < b ∧ b < 1 ∧ ∀ (ε : ℝ) (m d q : ℕ), 0 ≤ ε → 1 ≤ m → 1 ≤ d → 2 ≤ q → qldErr (min ε 1) m d q ≤ errShape a b ε m d q

thm:qld's error, in closed form. There are universal constants a ≥ 1 and 0 < b < 1 such that, for every ε ≥ 0, m, d ≥ 1 and q ≥ 2, the error qldErr at the failure probability min ε 1 is at most a (md)^a (ε^b + q^{-b} + 2^{-bmd}). A strategy's failure probability is at most one, so min ε 1 is as good a failure bound as ε.