The value of a strategy for the seeded test, sample by sample

The seeded test's question distribution is the push-forward of the uniform distribution on Sample F m under the two typed question maps. A strategy's failure probability is therefore the average over samples of the conditional failure at the two questions the sample generates (one_sub_povmValue_clGame), and that average splits into the nine ordered type pairs (sum_sample_eq). The padded strategy of the Pauli basis test is analysed one type pair at a time, which is what these two identities are for.

The file also records two facts about a seeded line question that the analysis reads off the geometry: a point lies on its own line at the parameter lineParam computes, whether or not the direction vanishes (rep_add_lineParam_smul), and a degenerate diagonal direction is rare (sum_indicator_zeroBelow_eq_zero_le).

The sample space

def MIPRE.LIDT.CL.sampleEquiv (F : Type u_2) (m : ℕ) : Sample F m ≃ (Ty × Ty) × Point F m × F × Point F m

The verifier's random choices, split into the two types and the ambient triple.

Equations

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

theorem MIPRE.LIDT.CL.card_ty : Fintype.card Ty = 3

theorem MIPRE.LIDT.CL.card_sample {F : Type u_1} [Fintype F] {m : ℕ} : Fintype.card (Sample F m) = 9 * Fintype.card (Point F m × F × Point F m)

theorem MIPRE.LIDT.CL.sum_sample_eq {F : Type u_1} [Fintype F] {m : ℕ} {M : Type u_2} [AddCommMonoid M] (f : Sample F m → M) : ∑ sm : Sample F m, f sm = ∑ tA : Ty, ∑ tB : Ty, ∑ x : Point F m × F × Point F m, f { tyA := tA, tyB := tB, u := x.1, s := x.2.1, v := x.2.2 }

A sum over samples, as a sum over the two types and the ambient triple.

A point lies on its own line

theorem MIPRE.LIDT.CL.rep_add_lineParam_smul {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (w u : Point F m) : rep w u + lineParam (rep w u) w u • w = u

Every point lies on its own seeded line, at the parameter lineParam computes, whether or not the direction vanishes.

theorem MIPRE.LIDT.CL.lineParam_rep_add_smul {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} {w : Point F m} (hw : ∃ (j : Fin m), w j ≠ 0) (u : Point F m) (t : F) : lineParam (rep w (u + t • w)) w (u + t • w) = lineParam (rep w u) w u + t

Moving the point along a non-degenerate line by t moves its parameter by t, and keeps the base point.

Degenerate diagonal directions are rare

theorem MIPRE.LIDT.CL.sum_indicator_apply_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (i : Fin m) (c : F) : (∑ v : Point F m, if v i = c then 1 else 0) = ∑ v : Point F m, if v i = 0 then 1 else 0

The number of vectors with a prescribed value at one coordinate does not depend on the value.

theorem MIPRE.LIDT.CL.sum_indicator_apply_eq_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (i : Fin m) : (∑ v : Point F m, if v i = 0 then 1 else 0) = ↑(Fintype.card (Point F m)) / ↑(Fintype.card F)

theorem MIPRE.LIDT.CL.sum_indicator_zeroBelow_eq_zero_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (i : Fin m) : (∑ v : Point F m, if zeroBelow i v = 0 then 1 else 0) ≤ ↑(Fintype.card (Point F m)) / ↑(Fintype.card F)

A degenerate diagonal direction is rare: the truncation zeroBelow i vanishes on at most a 1/q fraction of the raw directions.

The failure probability, sample by sample

theorem MIPRE.LIDT.CL.one_sub_povmValue_clGame {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) {dA : Type u_2} {dB : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (MA : Question F m → POVM (Answer F m d ldc) dA) (MB : Question F m → POVM (Answer F m d ldc) dB) : 1 - povmValue (clGame hm) ψ MA MB = (↑(Fintype.card (Sample F m)))⁻¹ * ∑ sm : Sample F m, condFail (clGame hm) ψ MA MB (Sample.question hm sm sm.tyA) (Sample.question hm sm sm.tyB)

The failure probability of a POVM strategy in the seeded test is the average over the verifier's samples of the conditional failure at the two questions the sample generates.