The block index

@[reducible, inline]

abbrev CommutingRepetition.EntropicArena.Idx (I J : Type) : Type

The block index: Alice's I, the source coordinate, Bob's J.

Equations

• CommutingRepetition.EntropicArena.Idx I J = (I ⊕ Unit ⊕ J)

def CommutingRepetition.EntropicArena.src (I J : Type) : Idx I J

The source coordinate.

Equations

• CommutingRepetition.EntropicArena.src I J = Sum.inr (Sum.inl ())

def CommutingRepetition.EntropicArena.ai {I J : Type} (i : I) : Idx I J

Alice's coordinates.

Equations

• CommutingRepetition.EntropicArena.ai i = Sum.inl i

def CommutingRepetition.EntropicArena.bj {I J : Type} (j : J) : Idx I J

Bob's coordinates.

Equations

• CommutingRepetition.EntropicArena.bj j = Sum.inr (Sum.inr j)

instance CommutingRepetition.EntropicArena.instNonemptyIdx {I J : Type} : Nonempty (Idx I J)

theorem CommutingRepetition.EntropicArena.ai_injective {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] : Function.Injective ai

theorem CommutingRepetition.EntropicArena.bj_injective {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] : Function.Injective bj

@[reducible, inline]

abbrev CommutingRepetition.EntropicArena.𝓑 (M : StdTracialAlgebra) (I J : Type) : Type

The block Hilbert space.

Equations

• CommutingRepetition.EntropicArena.𝓑 M I J = CommutingRepetition.Block.BH M (CommutingRepetition.EntropicArena.Idx I J)

@[reducible, inline]

noncomputable abbrev CommutingRepetition.EntropicArena.𝔑 (M : StdTracialAlgebra) (I J : Type) [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] : StarSubalgebra ℂ (𝓑 M I J →L[ℂ] 𝓑 M I J)

The block algebra.

Equations

• CommutingRepetition.EntropicArena.𝔑 M I J = CommutingRepetition.Block.blockAlg M (CommutingRepetition.EntropicArena.Idx I J)

@[reducible, inline]

noncomputable abbrev CommutingRepetition.EntropicArena.N (M : StdTracialAlgebra) (I J : Type) [Fintype I] [Fintype J] : StdTracialAlgebra

The arena algebra.

Equations

• CommutingRepetition.EntropicArena.N M I J = CommutingRepetition.Block.N M (CommutingRepetition.EntropicArena.Idx I J)

@[reducible, inline]

abbrev CommutingRepetition.EntropicArena.d (I J : Type) [Fintype I] [Fintype J] : ℕ

The amplification dimension.

Equations

• CommutingRepetition.EntropicArena.d I J = CommutingRepetition.Block.dim (CommutingRepetition.EntropicArena.Idx I J)

The left representation into vnAlg

noncomputable def CommutingRepetition.EntropicArena.Lv (M : StdTracialAlgebra) (a : M.A) : ↥M.vnAlg

L a as an element of vnAlg M.

Equations

• CommutingRepetition.EntropicArena.Lv M a = ⟨M.L a, ⋯⟩

theorem CommutingRepetition.EntropicArena.Lv_val (M : StdTracialAlgebra) (a : M.A) : ↑(Lv M a) = M.L a

theorem CommutingRepetition.EntropicArena.Lv_mul (M : StdTracialAlgebra) (a b : M.A) : Lv M (a * b) = Lv M a * Lv M b

theorem CommutingRepetition.EntropicArena.Lv_star (M : StdTracialAlgebra) (a : M.A) : Lv M (star a) = star (Lv M a)

theorem CommutingRepetition.EntropicArena.Lv_one (M : StdTracialAlgebra) : Lv M 1 = 1

theorem CommutingRepetition.EntropicArena.Lv_sum (M : StdTracialAlgebra) {ι : Type u_1} (s : Finset ι) (f : ι → M.A) : Lv M (∑ x ∈ s, f x) = ∑ x ∈ s, Lv M (f x)

theorem CommutingRepetition.EntropicArena.Lv_sub (M : StdTracialAlgebra) (a b : M.A) : Lv M (a - b) = Lv M a - Lv M b

theorem CommutingRepetition.EntropicArena.L_nonneg (M : StdTracialAlgebra) {a : M.A} (ha : IsPosElem a) : 0 ≤ M.L a

theorem CommutingRepetition.EntropicArena.L_le_one (M : StdTracialAlgebra) {a : M.A} (ha : IsPosElem (1 - a)) : M.L a ≤ 1

The data

structure CommutingRepetition.EntropicArena.Hyp (M : StdTracialAlgebra) {I J A B : Type} [Fintype A] [Fintype B] (F : I → A → M.A) (G : J → B → M.A) : Prop

The hypotheses of resolver_arena_entropic.

• hF (i : I) (a : A) : IsPosElem (F i a)
• hG (j : J) (b : B) : IsPosElem (G j b)
• hF1 (i : I) : IsPosElem (1 - ∑ a : A, F i a)
• hG1 (j : J) : IsPosElem (1 - ∑ b : B, G j b)

@[reducible, inline]

abbrev CommutingRepetition.EntropicArena.FA (M : StdTracialAlgebra) {I A : Type} [Fintype A] (F : I → A → M.A) (i : I) : M.A

Alice's totals.

Equations

• CommutingRepetition.EntropicArena.FA M F i = ∑ a : A, F i a

@[reducible, inline]

abbrev CommutingRepetition.EntropicArena.GB (M : StdTracialAlgebra) {J B : Type} [Fintype B] (G : J → B → M.A) (j : J) : M.A

Bob's totals.

Equations

• CommutingRepetition.EntropicArena.GB M G j = ∑ b : B, G j b

@[reducible, inline]

noncomputable abbrev CommutingRepetition.EntropicArena.LF (M : StdTracialAlgebra) {I A : Type} [Fintype A] (F : I → A → M.A) (i : I) : M.H →L[ℂ] M.H

Alice's totals as operators.

Equations

• CommutingRepetition.EntropicArena.LF M F i = M.L (CommutingRepetition.EntropicArena.FA M F i)

@[reducible, inline]

noncomputable abbrev CommutingRepetition.EntropicArena.LG (M : StdTracialAlgebra) {J B : Type} [Fintype B] (G : J → B → M.A) (j : J) : M.H →L[ℂ] M.H

Bob's totals as operators.

Equations

• CommutingRepetition.EntropicArena.LG M G j = M.L (CommutingRepetition.EntropicArena.GB M G j)

theorem CommutingRepetition.EntropicArena.LF_nonneg (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (i : I) : 0 ≤ LF M F i

theorem CommutingRepetition.EntropicArena.LF_le_one (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (i : I) : LF M F i ≤ 1

theorem CommutingRepetition.EntropicArena.LG_nonneg (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (j : J) : 0 ≤ LG M G j

theorem CommutingRepetition.EntropicArena.LG_le_one (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (j : J) : LG M G j ≤ 1

The kernels

noncomputable def CommutingRepetition.EntropicArena.KA (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (i i' : I) : ↥M.vnAlg

Alice's kernel entries K(L Fᵢ, L Fᵢ') in vnAlg M.

Equations

• CommutingRepetition.EntropicArena.KA M h i i' = ⟨CommutingRepetition.Resolver.kern (CommutingRepetition.EntropicArena.LF M F i) (CommutingRepetition.EntropicArena.LF M F i'), ⋯⟩

noncomputable def CommutingRepetition.EntropicArena.KB (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (j j' : J) : ↥M.vnAlg

Bob's kernel entries K(L Gⱼ, L Gⱼ').

Equations

• CommutingRepetition.EntropicArena.KB M h j j' = ⟨CommutingRepetition.Resolver.kern (CommutingRepetition.EntropicArena.LG M G j) (CommutingRepetition.EntropicArena.LG M G j'), ⋯⟩

theorem CommutingRepetition.EntropicArena.KA_val (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (i i' : I) : ↑(KA M h i i') = Resolver.kern (LF M F i) (LF M F i')

theorem CommutingRepetition.EntropicArena.KB_val (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (j j' : J) : ↑(KB M h j j') = Resolver.kern (LG M G j) (LG M G j')

theorem CommutingRepetition.EntropicArena.KA_self (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (i : I) : KA M h i i = Lv M (FA M F i)

theorem CommutingRepetition.EntropicArena.KB_self (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (j : J) : KB M h j j = Lv M (GB M G j)

Block kernels and their positivity

noncomputable def CommutingRepetition.EntropicArena.blockKern (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {ι : Type} [Fintype ι] (c : ι → Idx I J) (Fs : ι → M.H →L[ℂ] M.H) : 𝓑 M I J →L[ℂ] 𝓑 M I J

The block kernel of a positive family placed at coordinates c.

Equations

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

theorem CommutingRepetition.EntropicArena.blockKern_mem (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {ι : Type} [Fintype ι] (c : ι → Idx I J) (Fs : ι → M.H →L[ℂ] M.H) (hFs0 : ∀ (i : ι), 0 ≤ Fs i) (hmem : ∀ (i : ι), Fs i ∈ M.vnAlg) : blockKern M c Fs ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.entry_blockKern (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {ι : Type} [Fintype ι] {c : ι → Idx I J} (hc : Function.Injective c) (Fs : ι → M.H →L[ℂ] M.H) (i i' : ι) : Block.entry M (Idx I J) (blockKern M c Fs) (c i) (c i') = Resolver.kern (Fs i) (Fs i')

theorem CommutingRepetition.EntropicArena.blockKern_nonneg (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {ι : Type} [Fintype ι] (c : ι → Idx I J) (Fs : ι → M.H →L[ℂ] M.H) (hFs0 : ∀ (i : ι), 0 ≤ Fs i) : 0 ≤ blockKern M c Fs

Positivity of the block kernel: it is the limit of the integrals ∫ ρ(u)* ρ(u) du over the cutoffs.

The block kernels and their square roots

noncomputable def CommutingRepetition.EntropicArena.𝒦A (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] {F : I → A → M.A} {G : J → B → M.A} (_h : Hyp M F G) : 𝓑 M I J →L[ℂ] 𝓑 M I J

Alice's block kernel [K(L Fᵢ, L Fᵢ')] on the I-block.

Equations

• CommutingRepetition.EntropicArena.𝒦A M _h = CommutingRepetition.EntropicArena.blockKern M CommutingRepetition.EntropicArena.ai (CommutingRepetition.EntropicArena.LF M F)

noncomputable def CommutingRepetition.EntropicArena.𝒦B (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] {F : I → A → M.A} {G : J → B → M.A} (_h : Hyp M F G) : 𝓑 M I J →L[ℂ] 𝓑 M I J

Bob's block kernel [K(L Gⱼ, L Gⱼ')] on the J-block.

Equations

• CommutingRepetition.EntropicArena.𝒦B M _h = CommutingRepetition.EntropicArena.blockKern M CommutingRepetition.EntropicArena.bj (CommutingRepetition.EntropicArena.LG M G)

theorem CommutingRepetition.EntropicArena.𝒦A_mem (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : 𝒦A M h ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.𝒦B_mem (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : 𝒦B M h ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.𝒦A_nonneg (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : 0 ≤ 𝒦A M h

theorem CommutingRepetition.EntropicArena.𝒦B_nonneg (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : 0 ≤ 𝒦B M h

theorem CommutingRepetition.EntropicArena.entry_𝒦A (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (i i' : I) : Block.entry M (Idx I J) (𝒦A M h) (ai i) (ai i') = ↑(KA M h i i')

theorem CommutingRepetition.EntropicArena.entry_𝒦B (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (j j' : J) : Block.entry M (Idx I J) (𝒦B M h) (bj j) (bj j') = ↑(KB M h j j')

noncomputable def CommutingRepetition.EntropicArena.𝒞A (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : 𝓑 M I J →L[ℂ] 𝓑 M I J

𝒞_A = √𝒦_A.

Equations

• CommutingRepetition.EntropicArena.𝒞A M h = CFC.sqrt (CommutingRepetition.EntropicArena.𝒦A M h)

noncomputable def CommutingRepetition.EntropicArena.𝒞B (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : 𝓑 M I J →L[ℂ] 𝓑 M I J

𝒞_B = √𝒦_B.

Equations

• CommutingRepetition.EntropicArena.𝒞B M h = CFC.sqrt (CommutingRepetition.EntropicArena.𝒦B M h)

theorem CommutingRepetition.EntropicArena.𝒞A_sq (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : 𝒞A M h * 𝒞A M h = 𝒦A M h

theorem CommutingRepetition.EntropicArena.𝒞B_sq (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : 𝒞B M h * 𝒞B M h = 𝒦B M h

theorem CommutingRepetition.EntropicArena.𝒞A_sa (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : IsSelfAdjoint (𝒞A M h)

theorem CommutingRepetition.EntropicArena.𝒞B_sa (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : IsSelfAdjoint (𝒞B M h)

theorem CommutingRepetition.EntropicArena.sqrt_mem (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {T : 𝓑 M I J →L[ℂ] 𝓑 M I J} (hT0 : 0 ≤ T) (hT : T ∈ 𝔑 M I J) : CFC.sqrt T ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.𝒞A_mem (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : 𝒞A M h ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.𝒞B_mem (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : 𝒞B M h ∈ 𝔑 M I J

Matrix units, columns and rows

noncomputable def CommutingRepetition.EntropicArena.U (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (r r' : Idx I J) : ↥(𝔑 M I J)

The matrix unit e_{r r'}.

Equations

• CommutingRepetition.EntropicArena.U M r r' = ⟨(CommutingRepetition.Block.place M (CommutingRepetition.EntropicArena.Idx I J) r r') 1, ⋯⟩

theorem CommutingRepetition.EntropicArena.U_val (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (r r' : Idx I J) : ↑(U M r r') = (Block.place M (Idx I J) r r') 1

theorem CommutingRepetition.EntropicArena.star_U (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (r r' : Idx I J) : star (U M r r') = U M r' r

noncomputable def CommutingRepetition.EntropicArena.CA (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : ↥(𝔑 M I J)

𝒞_A as an element of the block algebra.

Equations

• CommutingRepetition.EntropicArena.CA M h = ⟨CommutingRepetition.EntropicArena.𝒞A M h, ⋯⟩

noncomputable def CommutingRepetition.EntropicArena.CB (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) : ↥(𝔑 M I J)

𝒞_B as an element of the block algebra.

Equations

• CommutingRepetition.EntropicArena.CB M h = ⟨CommutingRepetition.EntropicArena.𝒞B M h, ⋯⟩

noncomputable def CommutingRepetition.EntropicArena.cA (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (i : I) : ↥(𝔑 M I J)

Alice's column cᵢ = 𝒞_A e_{i, src}.

Equations

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

noncomputable def CommutingRepetition.EntropicArena.dB (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (j : J) : ↥(𝔑 M I J)

Bob's row dⱼ = e_{src, j} 𝒞_B.

Equations

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

@[reducible, inline]

noncomputable abbrev CommutingRepetition.EntropicArena.Ecor (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (T : ↥M.vnAlg) : ↥(𝔑 M I J)

The corner copy at the source coordinate.

Equations

• CommutingRepetition.EntropicArena.Ecor M T = CommutingRepetition.Block.E M (CommutingRepetition.EntropicArena.Idx I J) (CommutingRepetition.EntropicArena.src I J) T

theorem CommutingRepetition.EntropicArena.Ecor_val (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (T : ↥M.vnAlg) : ↑(Ecor M T) = (Block.place M (Idx I J) (src I J) (src I J)) ↑T

theorem CommutingRepetition.EntropicArena.star_cA_mul_cA (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (i i' : I) : star (cA M h i') * cA M h i = Ecor M (KA M h i' i)

cᵢ'* cᵢ = E(K(Fᵢ', Fᵢ)) (eq resolver-square-identities, polarized).

theorem CommutingRepetition.EntropicArena.dB_mul_star_dB (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (j j' : J) : dB M h j * star (dB M h j') = Ecor M (KB M h j j')

dⱼ dⱼ'* = E(K(Gⱼ, Gⱼ')).

theorem CommutingRepetition.EntropicArena.star_cA_mul_cA_self (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (i : I) : star (cA M h i) * cA M h i = Ecor M (Lv M (FA M F i))

theorem CommutingRepetition.EntropicArena.dB_mul_star_dB_self (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (j : J) : dB M h j * star (dB M h j) = Ecor M (Lv M (GB M G j))

Algebra of the corner copy

theorem CommutingRepetition.EntropicArena.Ecor_Lv_mul (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (a b : M.A) : Ecor M (Lv M a) * Ecor M (Lv M b) = Ecor M (Lv M (a * b))

theorem CommutingRepetition.EntropicArena.star_Ecor_Lv (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (a : M.A) : star (Ecor M (Lv M a)) = Ecor M (Lv M (star a))

theorem CommutingRepetition.EntropicArena.coe_sum_𝔑 (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {ι : Type u_1} (t : Finset ι) (f : ι → ↥(𝔑 M I J)) : ↑(∑ x ∈ t, f x) = ∑ x ∈ t, ↑(f x)

Coercion of a sum in the block algebra.

The Douglas POVMs

@[reducible, inline]

abbrev CommutingRepetition.EntropicArena.IdxA {I A : Type} (kA : I → A → ℕ) (i : I) : Type

Alice's factor index at i.

Equations

• CommutingRepetition.EntropicArena.IdxA kA i = ((a : A) × Fin (kA i a))

@[reducible, inline]

abbrev CommutingRepetition.EntropicArena.IdxB {J B : Type} (kB : J → B → ℕ) (j : J) : Type

Bob's factor index at j.

Equations

• CommutingRepetition.EntropicArena.IdxB kB j = ((b : B) × Fin (kB j b))

noncomputable def CommutingRepetition.EntropicArena.xopA (M : StdTracialAlgebra) {I J A : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (i : I) (p : IdxA kA i) : 𝓑 M I J →L[ℂ] 𝓑 M I J

The factors of Alice's refinements, as corner operators.

Equations

• CommutingRepetition.EntropicArena.xopA M kA xA i p = ↑(CommutingRepetition.EntropicArena.Ecor M (CommutingRepetition.EntropicArena.Lv M (xA i p.fst p.snd)))

noncomputable def CommutingRepetition.EntropicArena.yopB (M : StdTracialAlgebra) {I J B : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (j : J) (p : IdxB kB j) : 𝓑 M I J →L[ℂ] 𝓑 M I J

The factors of Bob's refinements, as corner operators.

Equations

• CommutingRepetition.EntropicArena.yopB M kB yB j p = ↑(CommutingRepetition.EntropicArena.Ecor M (CommutingRepetition.EntropicArena.Lv M (yB j p.fst p.snd)))

theorem CommutingRepetition.EntropicArena.xopA_mem (M : StdTracialAlgebra) {I J A : Type} [Fintype I] [Fintype J] [Fintype A] [DecidableEq I] [DecidableEq J] [DecidableEq A] [Nonempty A] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (i : I) (p : IdxA kA i) : xopA M kA xA i p ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.yopB_mem (M : StdTracialAlgebra) {I J B : Type} [Fintype I] [Fintype J] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq B] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (j : J) (p : IdxB kB j) : yopB M kB yB j p ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.hxeA (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (i : I) : ∑ p : IdxA kA i, star (xopA M kA xA i p) * xopA M kA xA i p = star ↑(cA M h i) * ↑(cA M h i)

∑ x* x = cᵢ* cᵢ for Alice.

theorem CommutingRepetition.EntropicArena.hyeB (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (j : J) : ∑ p : IdxB kB j, star (yopB M kB yB j p) * yopB M kB yB j p = star ↑(star (dB M h j)) * ↑(star (dB M h j))

∑ y* y = dⱼ dⱼ* for Bob (with c := dⱼ*).

noncomputable def CommutingRepetition.EntropicArena.zA (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (i : I) (p : IdxA kA i) : 𝓑 M I J →L[ℂ] 𝓑 M I J

Alice's Douglas factors.

Equations

• CommutingRepetition.EntropicArena.zA M h kA xA hxA i p = CommutingRepetition.Resolver.Douglas.z ⋯ p

noncomputable def CommutingRepetition.EntropicArena.zB (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (j : J) (p : IdxB kB j) : 𝓑 M I J →L[ℂ] 𝓑 M I J

Bob's Douglas factors.

Equations

• CommutingRepetition.EntropicArena.zB M h kB yB hyB j p = CommutingRepetition.Resolver.Douglas.z ⋯ p

theorem CommutingRepetition.EntropicArena.zA_mem (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (i : I) (p : IdxA kA i) : zA M h kA xA hxA i p ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.zB_mem (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (j : J) (p : IdxB kB j) : zB M h kB yB hyB j p ∈ 𝔑 M I J

noncomputable def CommutingRepetition.EntropicArena.a₀ {A : Type} [Nonempty A] : A

The fallback answers.

Equations

• CommutingRepetition.EntropicArena.a₀ = Classical.arbitrary A

noncomputable def CommutingRepetition.EntropicArena.b₀ {B : Type} [Nonempty B] : B

Equations

• CommutingRepetition.EntropicArena.b₀ = Classical.arbitrary B

noncomputable def CommutingRepetition.EntropicArena.Aop (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (i : I) (a : A) : 𝓑 M I J →L[ℂ] 𝓑 M I J

Alice's POVM element at (i, a), as an operator.

Equations

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

noncomputable def CommutingRepetition.EntropicArena.Bop (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (j : J) (b : B) : 𝓑 M I J →L[ℂ] 𝓑 M I J

Bob's POVM element at (j, b), as an operator.

Equations

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

theorem CommutingRepetition.EntropicArena.ZA_mem (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (i : I) : Resolver.Douglas.Z ⋯ ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.ZB_mem (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (j : J) : Resolver.Douglas.Z ⋯ ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.Aop_mem (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (i : I) (a : A) : Aop M h kA xA hxA i a ∈ 𝔑 M I J

theorem CommutingRepetition.EntropicArena.Bop_mem (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (j : J) (b : B) : Bop M h kB yB hyB j b ∈ 𝔑 M I J

noncomputable def CommutingRepetition.EntropicArena.Ame (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (i : I) (a : A) : ↥(𝔑 M I J)

Alice's POVM element in the block algebra.

Equations

• CommutingRepetition.EntropicArena.Ame M h kA xA hxA i a = ⟨CommutingRepetition.EntropicArena.Aop M h kA xA hxA i a, ⋯⟩

noncomputable def CommutingRepetition.EntropicArena.Bme (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (j : J) (b : B) : ↥(𝔑 M I J)

Bob's POVM element in the block algebra.

Equations

• CommutingRepetition.EntropicArena.Bme M h kB yB hyB j b = ⟨CommutingRepetition.EntropicArena.Bop M h kB yB hyB j b, ⋯⟩

theorem CommutingRepetition.EntropicArena.Ame_sum (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (i : I) : ∑ a : A, Ame M h kA xA hxA i a = 1

theorem CommutingRepetition.EntropicArena.Bme_sum (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (j : J) : ∑ b : B, Bme M h kB yB hyB j b = 1

theorem CommutingRepetition.EntropicArena.sum_sigma_label (M : StdTracialAlgebra) {I J A : Type} [Fintype I] [Fintype J] [Fintype A] [DecidableEq I] [DecidableEq J] [DecidableEq A] [Nonempty A] {k : A → ℕ} (f : (a : A) → Fin (k a) → 𝓑 M I J →L[ℂ] 𝓑 M I J) (a : A) : (∑ p : (a : A) × Fin (k a), if p.fst = a then f p.fst p.snd else 0) = ∑ x : Fin (k a), f a x

Regrouping a labelled sigma sum.

theorem CommutingRepetition.EntropicArena.star_cA_mul_Ame_mul_cA (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (i : I) (a : A) : star (cA M h i) * Ame M h kA xA hxA i a * cA M h i = Ecor M (Lv M (F i a))

cᵢ* 𝖠ᵢᵃ cᵢ = E(Fᵢᵃ) (eq resolver-refinement-identities).

theorem CommutingRepetition.EntropicArena.dB_mul_Bme_mul_star_dB (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (j : J) (b : B) : dB M h j * Bme M h kB yB hyB j b * star (dB M h j) = Ecor M (Lv M (G j b))

dⱼ 𝖡ⱼᵇ dⱼ* = E(Gⱼᵇ).

Positivity of the lifted POVMs

@[reducible, inline]

noncomputable abbrev CommutingRepetition.EntropicArena.lft (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] : ↥(𝔑 M I J) →⋆ₐ[ℂ] (N M I J).A

The lift into the arena algebra.

Equations

• CommutingRepetition.EntropicArena.lft M = CommutingRepetition.Block.lift M (CommutingRepetition.EntropicArena.Idx I J)

theorem CommutingRepetition.EntropicArena.isPosElem_lft_star_mul_self (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (x : ↥(𝔑 M I J)) : IsPosElem ((lft M) (star x * x))

theorem CommutingRepetition.EntropicArena.isPosElem_lft_zero (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] : IsPosElem ((lft M) 0)

theorem CommutingRepetition.EntropicArena.isPosElem_lft_ite (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {P : Prop} [Decidable P] (x : ↥(𝔑 M I J)) : IsPosElem ((lft M) (if P then star x * x else 0))

theorem CommutingRepetition.EntropicArena.Ame_isPos (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (i : I) (a : A) : IsPosElem ((lft M) (Ame M h kA xA hxA i a))

theorem CommutingRepetition.EntropicArena.Bme_isPos (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (j : J) (b : B) : IsPosElem ((lft M) (Bme M h kB yB hyB j b))

The branch and the trace bookkeeping

noncomputable def CommutingRepetition.EntropicArena.Xb (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (i : I) (j : J) : ↥(𝔑 M I J)

The branch block cᵢ E(σ) dⱼ.

Equations

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

noncomputable def CommutingRepetition.EntropicArena.branch (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (i : I) (j : J) : (N M I J).H

The branch vector √d • ι(cᵢ E(σ) dⱼ).

Equations

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

theorem CommutingRepetition.EntropicArena.d_pos {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] : 0 < ↑(d I J)

theorem CommutingRepetition.EntropicArena.sqrt_d_sq {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] : ↑√↑(d I J) * ↑√↑(d I J) * (↑(d I J))⁻¹ = 1

theorem CommutingRepetition.EntropicArena.τ_conj (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (D W : ↥(𝔑 M I J)) : (N M I J).τ ((lft M) (star D * W * D)) = (N M I J).τ ((lft M) (W * (D * star D)))

Traciality of the arena trace, conjugation form.

theorem CommutingRepetition.EntropicArena.τ_conj' (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (D W V : ↥(𝔑 M I J)) : (N M I J).τ ((lft M) (star D * W * D * V)) = (N M I J).τ ((lft M) (W * (D * V * star D)))

theorem CommutingRepetition.EntropicArena.τ_lft_Ecor_Lv (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (a : M.A) : (N M I J).τ ((lft M) (Ecor M (Lv M a))) = (↑(d I J))⁻¹ * M.τ a

theorem CommutingRepetition.EntropicArena.star_Xb_mul_Xb (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (σ : M.A) (i : I) (j : J) : star (Xb M h σ i j) * Xb M h σ i j = star (dB M h j) * Ecor M (Lv M (star σ * FA M F i * σ)) * dB M h j

theorem CommutingRepetition.EntropicArena.star_Xb_mul_Ame_Xb_Bme (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (hyB : ∀ (j : J) (b : B), G j b = ∑ l : Fin (kB j b), star (yB j b l) * yB j b l) (σ : M.A) (i : I) (j : J) (a : A) (b : B) : star (Xb M h σ i j) * (Ame M h kA xA hxA i a * Xb M h σ i j * Bme M h kB yB hyB j b) = star (dB M h j) * Ecor M (Lv M (star σ * F i a * σ)) * dB M h j * Bme M h kB yB hyB j b

The arena

noncomputable def CommutingRepetition.EntropicArena.arena (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) [Nonempty A] [Nonempty B] (kA : I → A → ℕ) (xA : (i : I) → (a : A) → Fin (kA i a) → M.A) (hxA : ∀ (i : I) (a : A), F i a = ∑ k : Fin (kA i a), star (xA i a k) * xA i a k) (kB : J → B → ℕ) (yB : (j : J) → (b : B) → Fin (kB j b) → M.A) (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 entropic resolver arena.

Equations

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