Vector states

noncomputable def CommutingRepetition.EntropicArena.vecState (M : StdTracialAlgebra) (ξ : M.H) : (M.H →L[ℂ] M.H) →ₗ[ℝ] ℝ

The vector state C ↦ re ⟪ξ, C ξ⟫ as a real-linear functional.

Equations

• CommutingRepetition.EntropicArena.vecState M ξ = { toFun := fun (C : M.H →L[ℂ] M.H) => (inner ℂ ξ (C ξ)).re, map_add' := ⋯, map_smul' := ⋯ }

theorem CommutingRepetition.EntropicArena.vecState_apply (M : StdTracialAlgebra) (ξ : M.H) (C : M.H →L[ℂ] M.H) : (vecState M ξ) C = (inner ℂ ξ (C ξ)).re

theorem CommutingRepetition.EntropicArena.vecState_mono (M : StdTracialAlgebra) (ξ : M.H) {C C' : M.H →L[ℂ] M.H} (hCC : C ≤ C') : (vecState M ξ) C ≤ (vecState M ξ) C'

theorem CommutingRepetition.EntropicArena.sqrt_mem_vnAlg (M : StdTracialAlgebra) {P : M.H →L[ℂ] M.H} (hP0 : 0 ≤ P) (hP : P ∈ M.vnAlg) : CFC.sqrt P ∈ M.vnAlg

theorem CommutingRepetition.EntropicArena.sqrt_sa (M : StdTracialAlgebra) {P : M.H →L[ℂ] M.H} : IsSelfAdjoint (CFC.sqrt P)

theorem CommutingRepetition.EntropicArena.traceState_conj_eq_inner (M : StdTracialAlgebra) (σ : M.A) {C P : M.H →L[ℂ] M.H} (hC : C ∈ M.vnAlg) (hP : P ∈ M.vnAlg) (hP0 : 0 ≤ P) : M.traceState (M.L (star σ) * C * M.L σ * P) = inner ℂ ((M.L σ) ((CFC.sqrt P) M.traceVector)) (C ((M.L σ) ((CFC.sqrt P) M.traceVector)))

Alice's vector-state form of the positive functional: φ(L(σ*) C L(σ) P) = ⟪ξ, C ξ⟫ with ξ = L(σ) √P Ω.

theorem CommutingRepetition.EntropicArena.traceState_conj_eq_inner' (M : StdTracialAlgebra) (σ : M.A) {C P : M.H →L[ℂ] M.H} (hC : C ∈ M.vnAlg) (hP : P ∈ M.vnAlg) (hP0 : 0 ≤ P) : M.traceState (M.L (star σ) * P * M.L σ * C) = inner ℂ ((M.L (star σ)) ((CFC.sqrt P) M.traceVector)) (C ((M.L (star σ)) ((CFC.sqrt P) M.traceVector)))

Bob's vector-state form: φ(L(σ*) P L(σ) C) = ⟪ζ, C ζ⟫ with ζ = L(σ*) √P Ω.

The increments

theorem CommutingRepetition.EntropicArena.sq_norm_smul_ι (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (W : ↥(𝔑 M I J)) : ‖↑√↑(d I J) • (N M I J).ι ((lft M) W)‖ ^ 2 = ↑(d I J) * ((N M I J).τ ((lft M) (star W * W))).re

theorem CommutingRepetition.EntropicArena.d_mul_re_τ_Ecor (M : StdTracialAlgebra) {I J : Type} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (T : ↥M.vnAlg) : ↑(d I J) * ((N M I J).τ ((lft M) (Ecor M T))).re = (M.traceState ↑T).re

noncomputable def CommutingRepetition.EntropicArena.Δ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) : ↥M.vnAlg

Alice's polarized kernel K_ii − K_ii' − (K_i'i − K_i'i').

Equations

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

noncomputable def CommutingRepetition.EntropicArena.Δ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) : ↥M.vnAlg

Bob's polarized kernel.

Equations

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

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

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

theorem CommutingRepetition.EntropicArena.star_diffA_mul_diffA (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty 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') * (cA M h i - cA M h i') = Ecor M (ΔA M h i i')

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

theorem CommutingRepetition.EntropicArena.sq_norm_branch_sub_A (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (i i' : I) (j : J) : ‖branch M h σ i j - branch M h σ i' j‖ ^ 2 = (M.traceState (M.L (star σ) * ↑(ΔA M h i i') * M.L σ * LG M G j)).re

Alice's increment: ‖Φ(σ,i,j) − Φ(σ,i',j)‖² = re φ(L(σ*) Δ_A L(σ) L(Gⱼ)).

theorem CommutingRepetition.EntropicArena.sq_norm_branch_sub_B (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (i : I) (j j' : J) : ‖branch M h σ i j - branch M h σ i j'‖ ^ 2 = (M.traceState (M.L (star σ) * LF M F i * M.L σ * ↑(ΔB M h j j'))).re

Bob's increment: ‖Φ(σ,i,j) − Φ(σ,i,j')‖² = re φ(L(σ*) L(Fᵢ) L(σ) Δ_B).

The functionals

noncomputable def CommutingRepetition.EntropicArena.ωA (M : StdTracialAlgebra) {J B : Type} [Fintype B] (G : J → B → M.A) (σ : M.A) (j : J) : (M.H →L[ℂ] M.H) →ₗ[ℝ] ℝ

Alice's functional ω_j(C) = re ⟪ξ, C ξ⟫, ξ = L(σ) √(L Gⱼ) Ω.

Equations

• CommutingRepetition.EntropicArena.ωA M G σ j = CommutingRepetition.EntropicArena.vecState M ((M.L σ) ((CFC.sqrt (CommutingRepetition.EntropicArena.LG M G j)) M.traceVector))

noncomputable def CommutingRepetition.EntropicArena.ωB (M : StdTracialAlgebra) {I A : Type} [Fintype A] (F : I → A → M.A) (σ : M.A) (i : I) : (M.H →L[ℂ] M.H) →ₗ[ℝ] ℝ

Bob's functional ω_i(C) = re ⟪ζ, C ζ⟫, ζ = L(σ*) √(L Fᵢ) Ω.

Equations

• CommutingRepetition.EntropicArena.ωB M F σ i = CommutingRepetition.EntropicArena.vecState M ((M.L (star σ)) ((CFC.sqrt (CommutingRepetition.EntropicArena.LF M F i)) M.traceVector))

theorem CommutingRepetition.EntropicArena.ωA_eq (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (j : J) {C : M.H →L[ℂ] M.H} (hC : C ∈ M.vnAlg) : (ωA M G σ j) C = (M.traceState (M.L (star σ) * C * M.L σ * LG M G j)).re

theorem CommutingRepetition.EntropicArena.ωB_eq (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (i : I) {C : M.H →L[ℂ] M.H} (hC : C ∈ M.vnAlg) : (ωB M F σ i) C = (M.traceState (M.L (star σ) * LF M F i * M.L σ * C)).re

theorem CommutingRepetition.EntropicArena.ωA_mono (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (j : J) {C C' : M.H →L[ℂ] M.H} (hCC : C ≤ C') : (ωA M G σ j) C ≤ (ωA M G σ j) C'

theorem CommutingRepetition.EntropicArena.ωB_mono (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (i : I) {C C' : M.H →L[ℂ] M.H} (hCC : C ≤ C') : (ωB M F σ i) C ≤ (ωB M F σ i) C'

theorem CommutingRepetition.EntropicArena.ωA_LF (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (j : J) (i : I) : (ωA M G σ j) (LF M F i) = (M.τ (star σ * (FA M F i * σ * GB M G j))).re

theorem CommutingRepetition.EntropicArena.ωB_LG (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (i : I) (j : J) : (ωB M F σ i) (LG M G j) = (M.τ (star σ * (FA M F i * σ * GB M G j))).re

theorem CommutingRepetition.EntropicArena.ωA_mass (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (hσ : M.τ (star σ * σ) = 1) (j : J) : (ωA M G σ j) 1 ≤ 1

theorem CommutingRepetition.EntropicArena.ωB_mass (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (hσ : M.τ (star σ * σ) = 1) (i : I) : (ωB M F σ i) 1 ≤ 1

theorem CommutingRepetition.EntropicArena.hinc_A (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (j : J) (i i' : I) : ‖branch M h σ i j - branch M h σ i' j‖ ^ 2 = (ωA M G σ j) (Resolver.kern (LF M F i) (LF M F i) - Resolver.kern (LF M F i) (LF M F i') - Resolver.kern (LF M F i') (LF M F i) + Resolver.kern (LF M F i') (LF M F i'))

theorem CommutingRepetition.EntropicArena.hinc_B (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (σ : M.A) (i : I) (j j' : J) : ‖branch M h σ i j - branch M h σ i j'‖ ^ 2 = (ωB M F σ i) (Resolver.kern (LG M G j) (LG M G j) - Resolver.kern (LG M G j) (LG M G j') - Resolver.kern (LG M G j') (LG M G j) + Resolver.kern (LG M G j') (LG M G j'))

The tower condition along L

theorem CommutingRepetition.EntropicArena.tower_L (M : StdTracialAlgebra) {steps : ℕ} {Ω : Type} [Fintype Ω] (law : Ω → ℝ) {K : Type} [DecidableEq K] (idx : Fin (steps + 1) → Ω → K) (E : K → M.A) (hX : ∀ (s : Fin steps) (i : K), ↑(∑ ω : Ω with idx s.castSucc ω = i, law ω) • E i = ∑ ω : Ω with idx s.castSucc ω = i, ↑(law ω) • E (idx s.succ ω)) (s : Fin steps) (i : K) : ∑ ω : Ω, (if idx s.castSucc ω = i then law ω else 0) • M.L (E (idx s.succ ω)) = (∑ ω : Ω, if idx s.castSucc ω = i then law ω else 0) • M.L (E i)

The budgets

theorem CommutingRepetition.EntropicArena.col_budget (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (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) (steps : ℕ) {Ω : Type} [Fintype Ω] (law : Ω → ℝ) (hlaw : ∀ (ω : Ω), 0 ≤ law ω) (hsum : ∑ ω : Ω, law ω = 1) (idx : Fin (steps + 1) → Ω → I) (hidx0 : ∀ (ω ω' : Ω), idx 0 ω = idx 0 ω') (hX : ∀ (s : Fin steps) (i : I), ↑(∑ ω : Ω with idx s.castSucc ω = i, law ω) • FA M F i = ∑ ω : Ω with idx s.castSucc ω = i, ↑(law ω) • FA M F (idx s.succ ω)) (σ : M.A) (hσ : M.τ (star σ * σ) = 1) (j : J) (ω₀ : Ω) : ∑ s : Fin steps, ∑ ω : Ω, law ω * ‖(arena M h kA xA hxA kB yB hyB).branch σ (idx s.succ ω) j - (arena M h kA xA hxA kB yB hyB).branch σ (idx s.castSucc ω) j‖ ^ 2 ≤ (M.τ (star σ * (FA M F (idx 0 ω₀) * σ * GB M G j))).re.negMulLog

The Alice-column budget for the entropic arena (unbundled form of ResolverArena.ColEntropyBudget).

theorem CommutingRepetition.EntropicArena.row_budget (M : StdTracialAlgebra) {I J A B : Type} [Fintype I] [Fintype J] [Fintype A] [Fintype B] [DecidableEq I] [DecidableEq J] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] {F : I → A → M.A} {G : J → B → M.A} (h : Hyp M F G) (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) (steps : ℕ) {Ω : Type} [Fintype Ω] (law : Ω → ℝ) (hlaw : ∀ (ω : Ω), 0 ≤ law ω) (hsum : ∑ ω : Ω, law ω = 1) (idx : Fin (steps + 1) → Ω → J) (hidx0 : ∀ (ω ω' : Ω), idx 0 ω = idx 0 ω') (hX : ∀ (s : Fin steps) (j : J), ↑(∑ ω : Ω with idx s.castSucc ω = j, law ω) • GB M G j = ∑ ω : Ω with idx s.castSucc ω = j, ↑(law ω) • GB M G (idx s.succ ω)) (σ : M.A) (hσ : M.τ (star σ * σ) = 1) (i : I) (ω₀ : Ω) : ∑ s : Fin steps, ∑ ω : Ω, law ω * ‖(arena M h kA xA hxA kB yB hyB).branch σ i (idx s.succ ω) - (arena M h kA xA hxA kB yB hyB).branch σ i (idx s.castSucc ω)‖ ^ 2 ≤ (M.τ (star σ * (FA M F i * σ * GB M G (idx 0 ω₀)))).re.negMulLog

The Bob-row budget for the entropic arena (unbundled form of ResolverArena.RowEntropyBudget).