noncomputable def CommutingRepetition.diagCLM {Seed H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : Seed → H →L[ℂ] H) : (PiLp 2 fun (x : Seed) => H) →L[ℂ] PiLp 2 fun (x : Seed) => H

Blockwise (diagonal) operator on the finite ℓ²-power ⊕_ω H.

Equations

• CommutingRepetition.diagCLM T = ↑(PiLp.continuousLinearEquiv 2 ℂ fun (x : Seed) => H).symm ∘SL ContinuousLinearMap.pi fun (ω : Seed) => T ω ∘SL PiLp.proj 2 (fun (x : Seed) => H) ω

@[simp]

theorem CommutingRepetition.diagCLM_apply {Seed : Type} [Fintype Seed] {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : Seed → H →L[ℂ] H) (v : PiLp 2 fun (x : Seed) => H) (ω : Seed) : ((diagCLM T) v).ofLp ω = (T ω) (v.ofLp ω)

theorem CommutingRepetition.diagCLM_sum {Seed : Type} [Fintype Seed] {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_1} (s : Finset κ) (T : κ → Seed → H →L[ℂ] H) : ∑ k ∈ s, diagCLM (T k) = diagCLM fun (ω : Seed) => ∑ k ∈ s, T k ω

theorem CommutingRepetition.diagCLM_one {Seed : Type} [Fintype Seed] {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : (diagCLM fun (x : Seed) => 1) = 1

theorem CommutingRepetition.diagCLM_mul {Seed : Type} [Fintype Seed] {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T S : Seed → H →L[ℂ] H) : diagCLM T * diagCLM S = diagCLM fun (ω : Seed) => T ω * S ω

theorem CommutingRepetition.diagCLM_commute {Seed : Type} [Fintype Seed] {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T S : Seed → H →L[ℂ] H} (h : ∀ (ω : Seed), Commute (T ω) (S ω)) : Commute (diagCLM T) (diagCLM S)

theorem CommutingRepetition.diagCLM_isPositive {Seed : Type} [Fintype Seed] {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : Seed → H →L[ℂ] H} (h : ∀ (ω : Seed), (T ω).IsPositive) : (diagCLM T).IsPositive

theorem CommutingRepetition.isPositive_sum {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_1} (s : Finset κ) (T : κ → H →L[ℂ] H) (h : ∀ k ∈ s, (T k).IsPositive) : (∑ k ∈ s, T k).IsPositive

A finite sum of positive operators is positive.

theorem CommutingRepetition.isPositive_ite {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : Prop) [Decidable c] {T : H →L[ℂ] H} (h : c → T.IsPositive) : (if c then T else 0).IsPositive

An if-then-else between a positive operator and zero is positive.

noncomputable def CommutingRepetition.mixState {Seed H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (ν : Seed → ℝ) (ψ : H) : PiLp 2 fun (x : Seed) => H

The mixed state ⊕_ω √(ν ω) • ψ.

Equations

• CommutingRepetition.mixState ν ψ = WithLp.toLp 2 fun (ω : Seed) => √(ν ω) • ψ

@[simp]

theorem CommutingRepetition.mixState_apply {Seed : Type} [Fintype Seed] {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ν : Seed → ℝ) (ψ : H) (ω : Seed) : (mixState ν ψ).ofLp ω = √(ν ω) • ψ

theorem CommutingRepetition.mixState_norm {Seed : Type} [Fintype Seed] {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ν : Seed → ℝ) (hν0 : ∀ (ω : Seed), 0 ≤ ν ω) (hν1 : ∑ ω : Seed, ν ω = 1) (ψ : H) (hψ : ‖ψ‖ = 1) : ‖mixState ν ψ‖ = 1

noncomputable def CommutingRepetition.CommutingStrategy.seedMixture {Seed : Type} [Fintype Seed] {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (ν : Seed → ℝ) (hν0 : ∀ (ω : Seed), 0 ≤ ν ω) (hν1 : ∑ ω : Seed, ν ω = 1) (ψ : H) (hψ : ‖ψ‖ = 1) (E : Seed → X → A → H →L[ℂ] H) (F : Seed → Y → B → H →L[ℂ] H) (hE_pos : ∀ (ω : Seed) (x : X) (a : A), (E ω x a).IsPositive) (hF_pos : ∀ (ω : Seed) (y : Y) (b : B), (F ω y b).IsPositive) (hE_sum : ∀ (ω : Seed) (x : X), ∑ a : A, E ω x a = 1) (hF_sum : ∀ (ω : Seed) (y : Y), ∑ b : B, F ω y b = 1) (hcomm : ∀ (ω : Seed) (x : X) (y : Y) (a : A) (b : B), Commute (E ω x a) (F ω y b)) : CommutingStrategy X Y A B

Seed mixture of commuting strategies (shared classical randomness): sampling ω ∼ ν and playing the ω-th effect families on a common unit state ψ is a legal commuting strategy on ⊕_ω H.

Equations

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

theorem CommutingRepetition.CommutingStrategy.seedMixture_correlation {Seed : Type} [Fintype Seed] {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (ν : Seed → ℝ) (hν0 : ∀ (ω : Seed), 0 ≤ ν ω) (hν1 : ∑ ω : Seed, ν ω = 1) (ψ : H) (hψ : ‖ψ‖ = 1) (E : Seed → X → A → H →L[ℂ] H) (F : Seed → Y → B → H →L[ℂ] H) (hE_pos : ∀ (ω : Seed) (x : X) (a : A), (E ω x a).IsPositive) (hF_pos : ∀ (ω : Seed) (y : Y) (b : B), (F ω y b).IsPositive) (hE_sum : ∀ (ω : Seed) (x : X), ∑ a : A, E ω x a = 1) (hF_sum : ∀ (ω : Seed) (y : Y), ∑ b : B, F ω y b = 1) (hcomm : ∀ (ω : Seed) (x : X) (y : Y) (a : A) (b : B), Commute (E ω x a) (F ω y b)) (x : X) (y : Y) (a : A) (b : B) : (seedMixture ν hν0 hν1 ψ hψ E F hE_pos hF_pos hE_sum hF_sum hcomm).correlation x y a b = ∑ ω : Seed, ν ω * (inner ℂ ψ ((E ω x a) ((F ω y b) ψ))).re

The mixture's correlation is the ν-average of the component correlations.