@[reducible, inline]

abbrev CommutingRepetition.BlockArena.RowA {I A : Type} (kA : I → A → ℕ) : Type

Alice's factor rows (i, a, k).

Equations

• CommutingRepetition.BlockArena.RowA kA = ((i : I) × (a : A) × Fin (kA i a))

@[reducible, inline]

abbrev CommutingRepetition.BlockArena.ColB {J B : Type} (kB : J → B → ℕ) : Type

Bob's factor columns (j, b, l).

Equations

• CommutingRepetition.BlockArena.ColB kB = ((j : J) × (b : B) × Fin (kB j b))

@[reducible, inline]

abbrev CommutingRepetition.BlockArena.Idx {I J A B : Type} (kA : I → A → ℕ) (kB : J → B → ℕ) : Type

The block index set: the source e₀, Alice's rows, Bob's columns.

Equations

• CommutingRepetition.BlockArena.Idx kA kB = (Unit ⊕ CommutingRepetition.BlockArena.RowA kA ⊕ CommutingRepetition.BlockArena.ColB kB)

def CommutingRepetition.BlockArena.colVec {M : StdTracialAlgebra} {I J A B : Type} [DecidableEq I] (kA : I → A → ℕ) (kB : J → B → ℕ) (xA : RowA kA → M.A) (i : I) : Idx kA kB → M.A

The Alice column of i as a vector: the factors of i, zero elsewhere.

Equations

• CommutingRepetition.BlockArena.colVec kA kB xA i (Sum.inr (Sum.inl r)) = if r.fst = i then xA r else 0
• CommutingRepetition.BlockArena.colVec kA kB xA i x✝ = 0

def CommutingRepetition.BlockArena.rowVec {M : StdTracialAlgebra} {I J A B : Type} [DecidableEq J] (kA : I → A → ℕ) (kB : J → B → ℕ) (yB : ColB kB → M.A) (j : J) : Idx kA kB → M.A

The Bob row of j as a vector: the adjoint factors of j, zero elsewhere.

Equations

• CommutingRepetition.BlockArena.rowVec kA kB yB j (Sum.inr (Sum.inr s)) = if s.fst = j then star (yB s) else 0
• CommutingRepetition.BlockArena.rowVec kA kB yB j x✝ = 0

def CommutingRepetition.BlockArena.labelA {I J A B : Type} [DecidableEq I] (kA : I → A → ℕ) (kB : J → B → ℕ) (a₀ : A) (i : I) : Idx kA kB → A

The answer label of an index for Alice's POVM at i: the factor's answer on the rows of i, the fallback a₀ everywhere else.

Equations

• CommutingRepetition.BlockArena.labelA kA kB a₀ i (Sum.inr (Sum.inl r)) = if r.fst = i then r.snd.fst else a₀
• CommutingRepetition.BlockArena.labelA kA kB a₀ i x✝ = a₀

def CommutingRepetition.BlockArena.labelB {I J A B : Type} [DecidableEq J] (kA : I → A → ℕ) (kB : J → B → ℕ) (b₀ : B) (j : J) : Idx kA kB → B

Equations

• CommutingRepetition.BlockArena.labelB kA kB b₀ j (Sum.inr (Sum.inr s)) = if s.fst = j then s.snd.fst else b₀
• CommutingRepetition.BlockArena.labelB kA kB b₀ j x✝ = b₀

def CommutingRepetition.BlockArena.rankOne {M : StdTracialAlgebra} {I J A B : Type} (kA : I → A → ℕ) (kB : J → B → ℕ) (a b : Idx kA kB → M.A) (σ : M.A) : Matrix (Idx kA kB) (Idx kA kB) M.A

A rank-one block a σ bᵀ.

Equations

• CommutingRepetition.BlockArena.rankOne kA kB a b σ = Matrix.of fun (p q : CommutingRepetition.BlockArena.Idx kA kB) => a p * σ * b q

def CommutingRepetition.BlockArena.branchMat {M : StdTracialAlgebra} {I J A B : Type} [DecidableEq I] [DecidableEq J] (kA : I → A → ℕ) (kB : J → B → ℕ) (xA : RowA kA → M.A) (yB : ColB kB → M.A) (σ : M.A) (i : I) (j : J) : Matrix (Idx kA kB) (Idx kA kB) M.A

The rank-one block c_i (σ e₀₀) d_j: entries x_r σ y_s*.

Equations

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

def CommutingRepetition.BlockArena.proj {M : StdTracialAlgebra} {I J A B : Type} [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (P : Idx kA kB → Prop) [DecidablePred P] : Matrix (Idx kA kB) (Idx kA kB) M.A

A 0/1 diagonal projection.

Equations

• CommutingRepetition.BlockArena.proj kA kB P = Matrix.diagonal fun (p : CommutingRepetition.BlockArena.Idx kA kB) => if P p then 1 else 0

The trace computation

theorem CommutingRepetition.BlockArena.sum_diag_trace {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (σ : M.A) (a b : Idx kA kB → M.A) (PA PB : Idx kA kB → Prop) [DecidablePred PA] [DecidablePred PB] : ∑ q : Idx kA kB, M.τ ((star (rankOne kA kB a b σ) * (proj kA kB PA * rankOne kA kB a b σ * proj kA kB PB)) q q) = M.τ (star σ * ((∑ p : Idx kA kB, if PA p then star (a p) * a p else 0) * σ * ∑ q : Idx kA kB, if PB q then b q * star (b q) else 0))

The core computation (eqs branch-norm-computation, branch-weight-computation): the diagonal trace of X* (P X P') for the rank-one block X = a σ bᵀ.

The block sums

theorem CommutingRepetition.BlockArena.sum_colVec {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (xA : RowA kA → M.A) (F : I → A → M.A) (a₀ : A) (i : I) (P : A → Prop) [DecidablePred P] (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA ⟨i, ⟨a, k⟩⟩) * xA ⟨i, ⟨a, k⟩⟩) : (∑ p : Idx kA kB, if P (labelA kA kB a₀ i p) then star (colVec kA kB xA i p) * colVec kA kB xA i p else 0) = ∑ a : A, if P a then F i a else 0

The Alice column square, restricted to an answer predicate on the block labels.

theorem CommutingRepetition.BlockArena.sum_rowVec {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (yB : ColB kB → M.A) (G : J → B → M.A) (b₀ : B) (j : J) (P : B → Prop) [DecidablePred P] (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB ⟨j, ⟨b, l⟩⟩) * yB ⟨j, ⟨b, l⟩⟩) : (∑ q : Idx kA kB, if P (labelB kA kB b₀ j q) then rowVec kA kB yB j q * star (rowVec kA kB yB j q) else 0) = ∑ b : B, if P b then G j b else 0

The Bob row square, restricted to an answer predicate.

theorem CommutingRepetition.BlockArena.sum_proj_labelA {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (a₀ : A) (i : I) : (∑ a : A, proj kA kB fun (p : Idx kA kB) => labelA kA kB a₀ i p = a) = 1

The 0/1 projections onto the labels of i form a partition of unity.

theorem CommutingRepetition.BlockArena.sum_proj_labelB {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (b₀ : B) (j : J) : (∑ b : B, proj kA kB fun (q : Idx kA kB) => labelB kA kB b₀ j q = b) = 1

theorem CommutingRepetition.BlockArena.proj_star_mul_self {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (P : Idx kA kB → Prop) [DecidablePred P] : star (proj kA kB P) * proj kA kB P = proj kA kB P

A 0/1 projection is a hermitian square of itself.

theorem CommutingRepetition.BlockArena.proj_true {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) : (proj kA kB fun (x : Idx kA kB) => True) = 1

The arena

@[reducible, inline]

abbrev CommutingRepetition.BlockArena.dim {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] (kA : I → A → ℕ) (kB : J → B → ℕ) : ℕ

The amplification dimension.

Equations

• CommutingRepetition.BlockArena.dim kA kB = Fintype.card (CommutingRepetition.BlockArena.Idx kA kB)

instance CommutingRepetition.BlockArena.instNeZeroNatDim {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] (kA : I → A → ℕ) (kB : J → B → ℕ) : NeZero (dim kA kB)

@[reducible, inline]

noncomputable abbrev CommutingRepetition.BlockArena.N {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] (kA : I → A → ℕ) (kB : J → B → ℕ) : StdTracialAlgebra

The block algebra N = M_d(M).

Equations

• CommutingRepetition.BlockArena.N kA kB = M.amplify (CommutingRepetition.BlockArena.dim kA kB)

noncomputable def CommutingRepetition.BlockArena.emb {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] (kA : I → A → ℕ) (kB : J → B → ℕ) (X : Matrix (Idx kA kB) (Idx kA kB) M.A) : (N kA kB).A

The reindexing of block matrices into N.

Equations

• CommutingRepetition.BlockArena.emb kA kB X = (Matrix.reindex (Fintype.equivFin (CommutingRepetition.BlockArena.Idx kA kB)) (Fintype.equivFin (CommutingRepetition.BlockArena.Idx kA kB))) X

theorem CommutingRepetition.BlockArena.emb_mul {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (X Y : Matrix (Idx kA kB) (Idx kA kB) M.A) : emb kA kB (X * Y) = emb kA kB X * emb kA kB Y

theorem CommutingRepetition.BlockArena.emb_star {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (X : Matrix (Idx kA kB) (Idx kA kB) M.A) : emb kA kB (star X) = star (emb kA kB X)

theorem CommutingRepetition.BlockArena.emb_one {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) : emb kA kB 1 = 1

theorem CommutingRepetition.BlockArena.emb_sum {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) {ι : Type} (s : Finset ι) (f : ι → Matrix (Idx kA kB) (Idx kA kB) M.A) : emb kA kB (∑ x ∈ s, f x) = ∑ x ∈ s, emb kA kB (f x)

theorem CommutingRepetition.BlockArena.τ_emb {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (X : Matrix (Idx kA kB) (Idx kA kB) M.A) : (N kA kB).τ (emb kA kB X) = (↑(dim kA kB))⁻¹ * ∑ p : Idx kA kB, M.τ (X p p)

The trace of N on an embedded block matrix: d⁻¹ ∑_p τ(X p p).

noncomputable def CommutingRepetition.BlockArena.arena {M : StdTracialAlgebra} {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] (kA : I → A → ℕ) (kB : J → B → ℕ) (xA : RowA kA → M.A) (yB : ColB kB → M.A) (F : I → A → M.A) (G : J → B → M.A) (a₀ : A) (b₀ : B) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA ⟨i, ⟨a, k⟩⟩) * xA ⟨i, ⟨a, k⟩⟩) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB ⟨j, ⟨b, l⟩⟩) * yB ⟨j, ⟨b, l⟩⟩) : ResolverArena M F G

The block arena.

Equations

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