noncomputable def CommutingRepetition.Density.letterOp {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : X × A ⊕ Y × B → S.H →L[ℂ] S.H

The letters: Alice's and Bob's effects.

Equations

• CommutingRepetition.Density.letterOp S (Sum.inl (x_1, a)) = S.E x_1 a
• CommutingRepetition.Density.letterOp S (Sum.inr (y, b)) = S.F y b

noncomputable def CommutingRepetition.Density.wordOp {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (l : List (X × A ⊕ Y × B)) : S.H →L[ℂ] S.H

A word in the effects, as an operator.

Equations

• CommutingRepetition.Density.wordOp S l = (List.map (CommutingRepetition.Density.letterOp S) l).prod

theorem CommutingRepetition.Density.wordOp_nil {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : wordOp S [] = 1

theorem CommutingRepetition.Density.wordOp_cons {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (i : X × A ⊕ Y × B) (l : List (X × A ⊕ Y × B)) : wordOp S (i :: l) = letterOp S i * wordOp S l

noncomputable def CommutingRepetition.Density.wordVec {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (l : List (X × A ⊕ Y × B)) : S.H

The vectors w ψ.

Equations

• CommutingRepetition.Density.wordVec S l = (CommutingRepetition.Density.wordOp S l) S.ψ

theorem CommutingRepetition.Density.countable_range_wordVec {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : (Set.range (wordVec S)).Countable

noncomputable def CommutingRepetition.Density.cyclic {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : Submodule ℂ S.H

The cyclic subspace: the closed span of the w ψ.

Equations

• CommutingRepetition.Density.cyclic S = (Submodule.span ℂ (Set.range (CommutingRepetition.Density.wordVec S))).topologicalClosure

theorem CommutingRepetition.Density.isClosed_cyclic {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : IsClosed ↑(cyclic S)

theorem CommutingRepetition.Density.ψ_mem_cyclic {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : S.ψ ∈ cyclic S

theorem CommutingRepetition.Density.letterOp_wordVec {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (i : X × A ⊕ Y × B) (l : List (X × A ⊕ Y × B)) : (letterOp S i) (wordVec S l) = wordVec S (i :: l)

theorem CommutingRepetition.Density.letterOp_mem_cyclic {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (i : X × A ⊕ Y × B) {v : S.H} (hv : v ∈ cyclic S) : (letterOp S i) v ∈ cyclic S

theorem CommutingRepetition.Density.E_mem_cyclic {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (x : X) (a : A) {v : S.H} (hv : v ∈ cyclic S) : (S.E x a) v ∈ cyclic S

theorem CommutingRepetition.Density.F_mem_cyclic {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (y : Y) (b : B) {v : S.H} (hv : v ∈ cyclic S) : (S.F y b) v ∈ cyclic S

theorem CommutingRepetition.Density.isSeparable_cyclic {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : TopologicalSpace.IsSeparable ↑(cyclic S)

instance CommutingRepetition.Density.separableSpace_cyclic {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : TopologicalSpace.SeparableSpace ↥(cyclic S)

instance CommutingRepetition.Density.completeSpace_cyclic {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : CompleteSpace ↥(cyclic S)

Compression

noncomputable def CommutingRepetition.Density.compressOp {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (T : S.H →L[ℂ] S.H) (hT : ∀ v ∈ cyclic S, T v ∈ cyclic S) : ↥(cyclic S) →L[ℂ] ↥(cyclic S)

Compression of an operator leaving cyclic S invariant.

Equations

• CommutingRepetition.Density.compressOp S T hT = (T ∘SL (CommutingRepetition.Density.cyclic S).subtypeL).codRestrict (CommutingRepetition.Density.cyclic S) ⋯

theorem CommutingRepetition.Density.compressOp_apply {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (T : S.H →L[ℂ] S.H) (hT : ∀ v ∈ cyclic S, T v ∈ cyclic S) (v : ↥(cyclic S)) : ↑((compressOp S T hT) v) = T ↑v

theorem CommutingRepetition.Density.compressOp_isPositive {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) {T : S.H →L[ℂ] S.H} (hT : ∀ v ∈ cyclic S, T v ∈ cyclic S) (hpos : T.IsPositive) : (compressOp S T hT).IsPositive

theorem CommutingRepetition.Density.compressOp_mul {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) {T U : S.H →L[ℂ] S.H} (hT : ∀ v ∈ cyclic S, T v ∈ cyclic S) (hU : ∀ v ∈ cyclic S, U v ∈ cyclic S) : compressOp S (T * U) ⋯ = compressOp S T hT * compressOp S U hU

theorem CommutingRepetition.Density.compressOp_one {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : compressOp S 1 ⋯ = 1

theorem CommutingRepetition.Density.compressOp_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) {ι : Type u_1} (s : Finset ι) (T : ι → S.H →L[ℂ] S.H) (hT : ∀ (i : ι), ∀ v ∈ cyclic S, (T i) v ∈ cyclic S) : compressOp S (∑ i ∈ s, T i) ⋯ = ∑ i ∈ s, compressOp S (T i) ⋯

noncomputable def CommutingRepetition.Density.compress {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : CommutingStrategy X Y A B

The compressed strategy on the separable cyclic subspace.

Equations

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

theorem CommutingRepetition.Density.compress_correlation {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : (compress S).correlation = S.correlation

instance CommutingRepetition.Density.separableSpace_compress {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : TopologicalSpace.SeparableSpace (compress S).H