Tensor powers of synchronous strategies

The completeness half of thm:parallel-repetition at the level of games: the k-fold tensor power of a PCC synchronous strategy of value 1 is a PCC synchronous strategy of value 1 for the k-fold direct repetition (blueprint def:direct-repetition).

• ProjectiveMeasurement.tensorPow P k: the family x⃗ ↦ a⃗ ↦ ⊗ᵢ M^{xᵢ}_{aᵢ} on ℂ^{Fin k → Fin d} (MIPRE.tensorFamily), a projective measurement family on the repeated alphabets; ProjectiveMeasurement.reindexMat carries it to ℂ^{d^k}, the shape SyncStrategy asks for.
• SyncStrategy.tensorPow S k : SyncStrategy (H.repeat k), with value = S.value ^ k (value_tensorPow) and PCC when S is (isPCC_tensorPow): the normalized trace on ℂ^{d^k} of a tensor product is the product of the normalized traces, and the direct repetition's distribution and predicate are products, so every summand of the value factorizes and the sum over k-tuples of questions and answers is the k-th power of the sum (sum_pi_prod).
• The doubled reading that Verifier.HasPerfectPCC uses: a strategy of G.doubled gives, by the tensor power read on the tag of the first coordinate, one of (G.repeat k).doubled (SyncStrategy.tensorPowDoubled), with the same value power and PCC, and exists_perfectPCC_repeat_doubled is the statement consumed downstream.

Reindexing a measurement family along an equivalence of the index set

theorem MIPRE.trace_submatrix_equiv {ι : Type u_3} {κ : Type u_4} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (M : Matrix ι ι ℂ) : (M.submatrix ⇑e.symm ⇑e.symm).trace = M.trace

The trace is invariant under reindexing along an equivalence.

def MIPRE.ProjectiveMeasurement.reindexMat {X : Type u_1} {A : Type u_2} [Fintype A] {ι : Type u_3} {κ : Type u_4} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (P : ProjectiveMeasurement X A (Matrix ι ι ℂ)) : ProjectiveMeasurement X A (Matrix κ κ ℂ)

Transport of a projective measurement family on ℂ^ι to ℂ^κ along ι ≃ κ.

Equations

• MIPRE.ProjectiveMeasurement.reindexMat e P = { M := fun (x : X) (a : A) => (P.M x a).submatrix ⇑e.symm ⇑e.symm, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.ProjectiveMeasurement.reindexMat_M {X : Type u_1} {A : Type u_2} [Fintype A] {ι : Type u_3} {κ : Type u_4} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (P : ProjectiveMeasurement X A (Matrix ι ι ℂ)) (x : X) (a : A) : (reindexMat e P).M x a = (P.M x a).submatrix ⇑e.symm ⇑e.symm

theorem MIPRE.ProjectiveMeasurement.reindexMat_trace_mul {X : Type u_1} {A : Type u_2} [Fintype A] {ι : Type u_3} {κ : Type u_4} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (P : ProjectiveMeasurement X A (Matrix ι ι ℂ)) (x y : X) (a b : A) : ((reindexMat e P).M x a * (reindexMat e P).M y b).trace = (P.M x a * P.M y b).trace

def MIPRE.ProjectiveMeasurement.tensorPow {X : Type u_1} {A : Type u_2} [Fintype A] {d : ℕ} (P : ProjectiveMeasurement X A (Matrix (Fin d) (Fin d) ℂ)) (k : ℕ) : ProjectiveMeasurement (Fin k → X) (Fin k → A) (Matrix (Fin k → Fin d) (Fin k → Fin d) ℂ)

The k-fold tensor power of a measurement family: x⃗ ↦ a⃗ ↦ ⊗ᵢ M^{xᵢ}_{aᵢ}.

Equations

• P.tensorPow k = { M := fun (x : Fin k → X) (a : Fin k → A) => MIPRE.tensorFamily fun (i : Fin k) => P.M (x i) (a i), selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.ProjectiveMeasurement.tensorPow_M {X : Type u_1} {A : Type u_2} [Fintype A] {d : ℕ} (P : ProjectiveMeasurement X A (Matrix (Fin d) (Fin d) ℂ)) (k : ℕ) (x : Fin k → X) (a : Fin k → A) : (P.tensorPow k).M x a = tensorFamily fun (i : Fin k) => P.M (x i) (a i)

noncomputable def MIPRE.equivFinPow (d k : ℕ) : (Fin k → Fin d) ≃ Fin (d ^ k)

(Fin k → Fin d) ≃ Fin (d ^ k).

Equations

• MIPRE.equivFinPow d k = Fintype.equivFinOfCardEq ⋯

The trace of a product of two projections is real

theorem MIPRE.trace_mul_im_eq_zero {d : ℕ} (hd : 0 < d) {P Q : Matrix (Fin d) (Fin d) ℂ} (hP : star P = P) (hPP : P * P = P) (hQ : star Q = Q) (hQQ : Q * Q = Q) : (P * Q).trace.im = 0

For self-adjoint idempotents P, Q on ℂ^d (d > 0), Tr(PQ) is real.

theorem MIPRE.re_trace_tensorFamily_div {d k : ℕ} (hd : 0 < d) (P Q : Fin k → Matrix (Fin d) (Fin d) ℂ) (hP : ∀ (i : Fin k), star (P i) = P i) (hPP : ∀ (i : Fin k), P i * P i = P i) (hQ : ∀ (i : Fin k), star (Q i) = Q i) (hQQ : ∀ (i : Fin k), Q i * Q i = Q i) : (tensorFamily P * tensorFamily Q).trace.re / ↑(d ^ k) = ∏ i : Fin k, (P i * Q i).trace.re / ↑d

The normalized trace of a tensor product of pairs of projections is the product of the normalized traces, in real parts.

Sums over tuples

theorem MIPRE.sum_pi_prod {X : Type u_3} {Y : Type u_4} {A : Type u_5} {B : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (f : X → Y → A → B → ℝ) (k : ℕ) : ∑ x : Fin k → X, ∑ y : Fin k → Y, ∑ a : Fin k → A, ∑ b : Fin k → B, ∏ i : Fin k, f (x i) (y i) (a i) (b i) = (∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, f x y a b) ^ k

A sum over k-tuples of a product of per-coordinate terms is the k-th power of the single-coordinate sum.

The tensor power of a synchronous strategy

noncomputable def MIPRE.SyncStrategy.tensorPow {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {H : SynchronousGame X A} (S : SyncStrategy H) (k : ℕ) : SyncStrategy (H.repeat k)

The k-fold tensor power of a synchronous strategy, a strategy for the k-fold direct repetition: dimension d ^ k, measurements ⊗ᵢ M^{xᵢ}_{aᵢ}.

Equations

• S.tensorPow k = { d := S.d ^ k, d_pos := ⋯, P := MIPRE.ProjectiveMeasurement.reindexMat (MIPRE.equivFinPow S.d k) (S.P.tensorPow k) }

noncomputable def MIPRE.SyncStrategy.weight {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {H : SynchronousGame X A} (S : SyncStrategy H) (x y : X) (a b : A) : ℝ

The per-coordinate weight of a strategy: μ(x, y) · [D(x, y, a, b)] · Tr(M^x_a M^y_b)/d.

Equations

• S.weight x y a b = (H.μ x y * if H.D x y a b = true then 1 else 0) * ((S.P.M x a * S.P.M y b).trace.re / ↑S.d)

theorem MIPRE.SyncStrategy.value_eq_sum_weight {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {H : SynchronousGame X A} (S : SyncStrategy H) : S.value = ∑ x : X, ∑ y : X, ∑ a : A, ∑ b : A, S.weight x y a b

theorem MIPRE.SyncStrategy.weight_tensorPow {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {H : SynchronousGame X A} (S : SyncStrategy H) (k : ℕ) (x y : Fin k → X) (a b : Fin k → A) : (S.tensorPow k).weight x y a b = ∏ i : Fin k, S.weight (x i) (y i) (a i) (b i)

The summand of the tensor power's value factorizes over the coordinates.

theorem MIPRE.SyncStrategy.value_tensorPow {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {H : SynchronousGame X A} (S : SyncStrategy H) (k : ℕ) : (S.tensorPow k).value = S.value ^ k

The value of the tensor power is the power of the value.

theorem MIPRE.SyncStrategy.μ_pos_of_repeat_pos {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {H : SynchronousGame X A} {k : ℕ} {x y : Fin k → X} (h : 0 < (H.repeat k).μ x y) (i : Fin k) : 0 < H.μ (x i) (y i)

A positive product weight has positive factors.

theorem MIPRE.SyncStrategy.isPCC_tensorPow {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {H : SynchronousGame X A} {S : SyncStrategy H} (hS : S.IsPCC) (k : ℕ) : (S.tensorPow k).IsPCC

The tensor power of a PCC strategy is PCC.

The doubled reading

noncomputable def MIPRE.SyncStrategy.tensorPowDoubled {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : Game X X A A} (S : SyncStrategy G.doubled) (k : ℕ) : SyncStrategy (G.repeat k).doubled

The tensor power of a strategy of the doubled game, read on the doubled repeated game: the tag is that of every coordinate.

Equations

• S.tensorPowDoubled k = (S.tensorPow k).relabel (G.repeat k).doubled (fun (p : Bool × (Fin k → X)) (i : Fin k) => (p.1, p.2 i)) (Equiv.refl (Fin k → A))

theorem MIPRE.SyncStrategy.value_tensorPowDoubled {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : Game X X A A} (S : SyncStrategy G.doubled) (k : ℕ) : (S.tensorPowDoubled k).value = S.value ^ k

theorem MIPRE.SyncStrategy.isPCC_tensorPowDoubled {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : Game X X A A} {S : SyncStrategy G.doubled} (hS : S.IsPCC) (k : ℕ) : (S.tensorPowDoubled k).IsPCC

theorem MIPRE.exists_perfectPCC_repeat_doubled {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : Game X X A A} (k : ℕ) (h : ∃ (S : SyncStrategy G.doubled), S.IsPCC ∧ S.value = 1) : ∃ (S' : SyncStrategy (G.repeat k).doubled), S'.IsPCC ∧ S'.value = 1

Game-level completeness of direct repetition: a value-1 PCC strategy of the doubled game gives one of the doubled k-fold repetition, for every k.