Tensor powers of permutation strategies

Paper II, Claim II:3043 and the completeness half of thm:repetition (II:11103), in the direct form of the plan (planning/aldous-lyons-track.md, Phase 2): a perfect Z-aligned permutation strategy commuting along edges for a tailored game G gives one for the product G.repeat k, its k-th tensor power.

• slot i : Matrix ι ι ℂ →ₐ[ℂ] Matrix (Fin k → ι) (Fin k → ι) ℂ, M ↦ 1 ⊗ ⋯ ⊗ M ⊗ ⋯ ⊗ 1 with M in the i-th factor, an algebra map; on ℂ^{m^k} after reindexing, slotE. It sends signed permutation matrices to signed permutation matrices (isSignedPerm_slot, the Kronecker closure of Claim II:3043 in the form needed here) and diagonal matrices to diagonal ones; the images of two different slots commute (commute_slot_slot); and the product of the slots of a family is its tensor product (prod_slot_finRange).
• PermStrategy.repeat S k: the observable of the variable (i, v) of x⃗ (varEquiv) is slotE i (S.U xᵢ v). Its measurement at x⃗ is the tensor product of the coordinates' measurements (proj_repeat), the factors of the Fourier transform commuting and being regrouped by coordinate.
• PermStrategy.proj_mul_eq_zero_of_value_eq_one: in a perfect permutation strategy, a rejected pair of answers to an edge is never produced, P^x_a P^y_b = 0.
• value_repeat_eq_one: the tensor power of a perfect strategy is perfect.
• PermStrategy.comap: a permutation strategy pulled back along a map of questions that preserves the lengths, the edges and the acceptance on the edges; at questions where the lengths differ, which carry no edge, the observables are the identity. With it, HasPerfectZPC.repeat_doubled: a perfect strategy for the doubled game gives one for the doubled product, which is the form TailoredVerifier.HasPerfectZPC reads.

Slot embeddings

theorem MIPRE.Tailored.tensorFamily_update_apply {k : ℕ} {ι : Type u_1} [DecidableEq ι] (i : Fin k) (M : Matrix ι ι ℂ) (v w : Fin k → ι) : tensorFamily (Function.update (fun (x : Fin k) => 1) i M) v w = M (v i) (w i) * ∏ j ∈ Finset.univ \ {i}, 1 (v j) (w j)

The entries of 1 ⊗ ⋯ ⊗ M ⊗ ⋯ ⊗ 1.

noncomputable def MIPRE.Tailored.slot {k : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : Fin k) : Matrix ι ι ℂ →ₐ[ℂ] Matrix (Fin k → ι) (Fin k → ι) ℂ

The slot embedding M ↦ 1 ⊗ ⋯ ⊗ M ⊗ ⋯ ⊗ 1, M in the factor i: an algebra map.

Equations

• MIPRE.Tailored.slot i = AlgHom.ofLinearMap { toFun := fun (M : Matrix ι ι ℂ) => MIPRE.tensorFamily (Function.update (fun (x : Fin k) => 1) i M), map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯

theorem MIPRE.Tailored.slot_apply {k : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : Fin k) (M : Matrix ι ι ℂ) : (slot i) M = tensorFamily (Function.update (fun (x : Fin k) => 1) i M)

theorem MIPRE.Tailored.commute_slot_slot {k : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {i j : Fin k} (hij : i ≠ j) (A B : Matrix ι ι ℂ) : Commute ((slot i) A) ((slot j) B)

The images of two different slots commute.

theorem MIPRE.Tailored.prod_slot_of_nodup {k : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : Fin k → Matrix ι ι ℂ) (l : List (Fin k)) : l.Nodup → (List.map (fun (i : Fin k) => (slot i) (P i)) l).prod = tensorFamily fun (j : Fin k) => if j ∈ l then P j else 1

A product of slots, one per coordinate of a duplicate-free list.

theorem MIPRE.Tailored.prod_slot_finRange {k : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : Fin k → Matrix ι ι ℂ) : (List.map (fun (i : Fin k) => (slot i) (P i)) (List.finRange k)).prod = tensorFamily P

The product of the slots of a family, in order, is its tensor product.

theorem MIPRE.Tailored.tensorFamily_eq_zero {k : ℕ} {ι : Type u_1} {P : Fin k → Matrix ι ι ℂ} {i : Fin k} (h : P i = 0) : tensorFamily P = 0

A tensor product with a zero factor is zero.

theorem MIPRE.Tailored.isSignedPerm_slot {k : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : Fin k) {M : Matrix ι ι ℂ} (hM : IsSignedPerm M) : IsSignedPerm ((slot i) M)

A slot of a signed permutation matrix is a signed permutation matrix.

theorem MIPRE.Tailored.isDiag_slot {k : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : Fin k) {M : Matrix ι ι ℂ} (hM : M.IsDiag) : ((slot i) M).IsDiag

A slot of a diagonal matrix is diagonal.

noncomputable def MIPRE.Tailored.powEquiv (m k : ℕ) : (Fin k → Fin m) ≃ Fin (m ^ k)

The reindexing of ℂ^{Fin k → Fin m} as ℂ^{m^k}.

Equations

• MIPRE.Tailored.powEquiv m k = Fintype.equivFinOfCardEq ⋯

theorem MIPRE.Tailored.reindex_eq_reindexAlgEquiv {κ : Type u_2} {κ' : Type u_3} [Fintype κ] [Fintype κ'] [DecidableEq κ] [DecidableEq κ'] (e : κ ≃ κ') (M : Matrix κ κ ℂ) : (Matrix.reindex e e) M = (Matrix.reindexAlgEquiv ℂ ℂ e) M

Reindexing a square matrix is the algebra equivalence reindexAlgEquiv.

noncomputable def MIPRE.Tailored.slotE {k : ℕ} (m : ℕ) (i : Fin k) : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix (Fin (m ^ k)) (Fin (m ^ k)) ℂ

The slot embedding into the matrices on ℂ^{m^k}.

Equations

• MIPRE.Tailored.slotE m i = (↑(Matrix.reindexAlgEquiv ℂ ℂ (MIPRE.Tailored.powEquiv m k))).comp (MIPRE.Tailored.slot i)

theorem MIPRE.Tailored.slotE_apply {k : ℕ} (m : ℕ) (i : Fin k) (M : Matrix (Fin m) (Fin m) ℂ) : (slotE m i) M = (Matrix.reindex (powEquiv m k) (powEquiv m k)) ((slot i) M)

theorem MIPRE.Tailored.isSignedPerm_slotE {k m : ℕ} (i : Fin k) {M : Matrix (Fin m) (Fin m) ℂ} (hM : IsSignedPerm M) : IsSignedPerm ((slotE m i) M)

theorem MIPRE.Tailored.isDiag_slotE {k m : ℕ} (i : Fin k) {M : Matrix (Fin m) (Fin m) ℂ} (hM : M.IsDiag) : ((slotE m i) M).IsDiag

theorem MIPRE.Tailored.commute_slotE_slotE {k m : ℕ} {i j : Fin k} (hij : i ≠ j) (A B : Matrix (Fin m) (Fin m) ℂ) : Commute ((slotE m i) A) ((slotE m j) B)

theorem MIPRE.Tailored.commute_slotE {k m : ℕ} (i : Fin k) {A B : Matrix (Fin m) (Fin m) ℂ} (h : Commute A B) : Commute ((slotE m i) A) ((slotE m i) B)

theorem MIPRE.Tailored.commute_slotE_of {k m : ℕ} {i j : Fin k} {A B : Matrix (Fin m) (Fin m) ℂ} (h : i = j → Commute A B) : Commute ((slotE m i) A) ((slotE m j) B)

Slots in two coordinates of commuting matrices commute, whether the coordinates agree or not.

theorem MIPRE.Tailored.fourierFactor_map {R : Type u_2} {S : Type u_3} [Ring R] [Algebra ℂ R] [Ring S] [Algebra ℂ S] (φ : R →ₐ[ℂ] S) (u : R) (b : Bool) : fourierFactor (φ u) b = φ (fourierFactor u b)

The factors of a Fourier transform pass through an algebra map.

Perfect permutation strategies produce only accepted answers

theorem MIPRE.Tailored.PermStrategy.proj_mul_eq_conjTranspose_mul {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) {x y : X} (hxy : 0 < G.μ x y) (a : Fin (G.len x) → Bool) (b : Fin (G.len y) → Bool) : S.proj x a * S.proj y b = (S.proj x a * S.proj y b).conjTranspose * (S.proj x a * S.proj y b)

On an edge, P^x_a P^y_b is its own Xᴴ X: the two projections commute.

theorem MIPRE.Tailored.PermStrategy.trace_proj_mul_nonneg {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) {x y : X} (hxy : 0 < G.μ x y) (a : Fin (G.len x) → Bool) (b : Fin (G.len y) → Bool) : 0 ≤ (S.proj x a * S.proj y b).trace.re

On an edge, the probability of a pair of answers is nonnegative.

theorem MIPRE.Tailored.PermStrategy.proj_mul_eq_zero_of_value_eq_one {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (hS : S.value = 1) {x y : X} (hxy : 0 < G.μ x y) {a : Fin (G.len x) → Bool} {b : Fin (G.len y) → Bool} (hrej : ¬G.Accepts x y (List.ofFn a) (List.ofFn b)) : S.proj x a * S.proj y b = 0

A perfect permutation strategy never produces a rejected pair of answers on an edge.

The tensor power of a permutation strategy

theorem MIPRE.Tailored.TailoredGame.pos_of_repeat_pos {X : Type u_1} [Fintype X] (G : TailoredGame X) {k : ℕ} {x y : Fin k → X} (h : 0 < (G.repeat k).μ x y) (i : Fin k) : 0 < G.μ (x i) (y i)

An edge of the product is an edge in every coordinate.

noncomputable def MIPRE.Tailored.PermStrategy.repeat {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (k : ℕ) : PermStrategy (G.repeat k)

The k-th tensor power of a permutation strategy, for the product game: the observable of the variable (i, v) of x⃗ is S.U xᵢ v in the i-th tensor factor.

Equations

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

noncomputable def MIPRE.Tailored.PermStrategy.tensorProj {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (k : ℕ) (x : Fin k → X) (a : (i : Fin k) → Fin (G.len (x i)) → Bool) : Matrix (Fin (S.m ^ k)) (Fin (S.m ^ k)) ℂ

The tensor product of the coordinates' measurements, on ℂ^{m^k}.

Equations

• S.tensorProj k x a = (Matrix.reindex (MIPRE.Tailored.powEquiv S.m k) (MIPRE.Tailored.powEquiv S.m k)) (MIPRE.tensorFamily fun (i : Fin k) => S.proj (x i) (a i))

theorem MIPRE.Tailored.PermStrategy.finRange_perm_flatMap {X : Type u_1} [Fintype X] {G : TailoredGame X} (k : ℕ) (x : Fin k → X) : (List.finRange (G.lenRSum x + G.lenLSum x)).Perm (List.flatMap (fun (i : Fin k) => List.map (fun (v : Fin (G.len (x i))) => (G.varEquiv x).symm ⟨i, v⟩) (List.finRange (G.len (x i)))) (List.finRange k))

The variables of x⃗ regrouped by coordinate: a permutation of all of them.

theorem MIPRE.Tailored.PermStrategy.proj_repeat {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (k : ℕ) (x : Fin k → X) (a : Fin (G.lenRSum x + G.lenLSum x) → Bool) : (S.repeat k).proj x a = S.tensorProj k x fun (i : Fin k) (v : Fin (G.len (x i))) => a ((G.varEquiv x).symm ⟨i, v⟩)

The measurement of the tensor power is the tensor product of the coordinates' measurements.

theorem MIPRE.Tailored.PermStrategy.reindex_tensorFamily_mul_eq_zero (k : ℕ) {m : ℕ} (P Q : Fin k → Matrix (Fin m) (Fin m) ℂ) (i : Fin k) (h : P i * Q i = 0) : (Matrix.reindex (powEquiv m k) (powEquiv m k)) (tensorFamily P) * (Matrix.reindex (powEquiv m k) (powEquiv m k)) (tensorFamily Q) = 0

A product of two tensor products is zero when one coordinate's product is.

theorem MIPRE.Tailored.PermStrategy.value_repeat_eq_one {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (k : ℕ) (hS : S.value = 1) : (S.repeat k).value = 1

The tensor power of a perfect permutation strategy is perfect.

Pulling a permutation strategy back along a map of questions

def MIPRE.Tailored.SameLens {X : Type u_1} [Fintype X] {Y : Type u_2} [Fintype Y] (G : TailoredGame X) (G' : TailoredGame Y) (φ : Y → X) (y : Y) : Prop

The lengths at y are those at φ y.

Equations

• MIPRE.Tailored.SameLens G G' φ y = (G'.lenR y = G.lenR (φ y) ∧ G'.lenL y = G.lenL (φ y))

theorem MIPRE.Tailored.SameLens.len_eq {X : Type u_1} [Fintype X] {Y : Type u_2} [Fintype Y] {G : TailoredGame X} {G' : TailoredGame Y} {φ : Y → X} {y : Y} (h : SameLens G G' φ y) : G'.len y = G.len (φ y)

theorem MIPRE.Tailored.fourierProj_cast {R : Type u_3} [Ring R] [Algebra ℂ R] {n n' : ℕ} (hn : n = n') (U : Fin n' → R) (a : Fin n → Bool) : fourierProj (fun (j : Fin n) => U (Fin.cast hn j)) a = fourierProj U fun (j : Fin n') => a (Fin.cast ⋯ j)

The Fourier transform reindexed along Fin.cast.

noncomputable def MIPRE.Tailored.PermStrategy.comap {X : Type u_1} [Fintype X] {Y : Type u_2} [Fintype Y] {G : TailoredGame X} (S : PermStrategy G) (G' : TailoredGame Y) (φ : Y → X) (hedge : ∀ (y₁ y₂ : Y), 0 < G'.μ y₁ y₂ → SameLens G G' φ y₁ ∧ SameLens G G' φ y₂ ∧ 0 < G.μ (φ y₁) (φ y₂)) : PermStrategy G'

A permutation strategy pulled back along φ: at a question with the lengths of its image, the observables of the image; elsewhere the identity. The hypothesis is that the edges of G' join such questions and are sent to edges of G.

Equations

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

theorem MIPRE.Tailored.PermStrategy.proj_comap {X : Type u_1} [Fintype X] {Y : Type u_2} [Fintype Y] {G : TailoredGame X} {G' : TailoredGame Y} (S : PermStrategy G) (φ : Y → X) (hedge : ∀ (y₁ y₂ : Y), 0 < G'.μ y₁ y₂ → SameLens G G' φ y₁ ∧ SameLens G G' φ y₂ ∧ 0 < G.μ (φ y₁) (φ y₂)) {y : Y} (h : SameLens G G' φ y) (a : Fin (G'.len y) → Bool) : (S.comap G' φ hedge).proj y a = S.proj (φ y) fun (j : Fin (G.len (φ y))) => a (Fin.cast ⋯ j)

theorem MIPRE.Tailored.PermStrategy.value_comap_eq_one {X : Type u_1} [Fintype X] {Y : Type u_2} [Fintype Y] {G : TailoredGame X} {G' : TailoredGame Y} (S : PermStrategy G) (hS : S.value = 1) (φ : Y → X) (hedge : ∀ (y₁ y₂ : Y), 0 < G'.μ y₁ y₂ → SameLens G G' φ y₁ ∧ SameLens G G' φ y₂ ∧ 0 < G.μ (φ y₁) (φ y₂)) (hacc : ∀ (y₁ y₂ : Y), 0 < G'.μ y₁ y₂ → ∀ (a b : Cost.BitStr), G.Accepts (φ y₁) (φ y₂) a b → G'.Accepts y₁ y₂ a b) : (S.comap G' φ hedge).value = 1

A perfect strategy pulls back to a perfect strategy, when the acceptance on the edges of G' is implied by that on their images.

The doubled product

theorem MIPRE.Tailored.TailoredGame.HasPerfectZPC.repeat_doubled {X : Type u_1} [Fintype X] {G : TailoredGame X} {k : ℕ} (h : G.doubled.HasPerfectZPC) : (G.repeat k).doubled.HasPerfectZPC

A perfect ZPC strategy for the doubled game gives one for the doubled product: the tensor power of the strategy for G.doubled, read at (p, x⃗) on the questions (p, x₁), …, (p, x_k).