The vector state and Bob's functionals of a commuting strategy

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

The vector state T ↦ ⟪ψ, T ψ⟫.

Equations

• CommutingRepetition.Density.vecState S = { toFun := fun (T : S.H →L[ℂ] S.H) => inner ℂ S.ψ (T S.ψ), map_add' := ⋯, map_smul' := ⋯ }

theorem CommutingRepetition.Density.vecState_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) : (vecState S) T = inner ℂ S.ψ (T S.ψ)

noncomputable def CommutingRepetition.Density.bobFun {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (y : Y) (b : B) : (S.H →L[ℂ] S.H) →ₗ[ℂ] ℂ

Bob's functional T ↦ ⟪ψ, T F_b^y ψ⟫ on B(H).

Equations

• CommutingRepetition.Density.bobFun S y b = { toFun := fun (T : S.H →L[ℂ] S.H) => inner ℂ S.ψ (T ((S.F y b) S.ψ)), map_add' := ⋯, map_smul' := ⋯ }

theorem CommutingRepetition.Density.bobFun_apply {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (y : Y) (b : B) (T : S.H →L[ℂ] S.H) : (bobFun S y b) T = inner ℂ S.ψ (T ((S.F y b) S.ψ))

theorem CommutingRepetition.Density.bobFun_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (y : Y) : ∑ b : B, bobFun S y b = vecState S

theorem CommutingRepetition.Density.bobFun_correlation {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : ((bobFun S y b) (S.E x a)).re = S.correlation x y a b

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

theorem CommutingRepetition.Density.vecState_nonneg {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) : 0 ≤ (vecState S) (star T * T)

theorem CommutingRepetition.Density.bobFun_nonneg_of_commute {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (y : Y) (b : B) {T : S.H →L[ℂ] S.H} (hT : Commute T (S.F y b)) : 0 ≤ (bobFun S y b) (star T * T)

Bob's functionals are positive on operators commuting with Bob's effect.

theorem CommutingRepetition.Density.vecState_traceClass {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : IsTraceClassFunctional (vecState S)

theorem CommutingRepetition.Density.bobFun_traceClass {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (y : Y) (b : B) : IsTraceClassFunctional (bobFun S y b)

Sums of trace-class functionals

noncomputable def CommutingRepetition.Density.interleave {K : Type u_1} (v v' : ℕ → K) (k : ℕ) : K

Interleaving two sequences.

Equations

• CommutingRepetition.Density.interleave v v' k = if Even k then v (k / 2) else v' (k / 2)

theorem CommutingRepetition.Density.interleave_even {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (v v' : ℕ → K) (k : ℕ) : interleave v v' (2 * k) = v k

theorem CommutingRepetition.Density.interleave_odd {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (v v' : ℕ → K) (k : ℕ) : interleave v v' (2 * k + 1) = v' k

theorem CommutingRepetition.Density.summable_inner_of_summable_norm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {v w : ℕ → K} (hs : Summable fun (k : ℕ) => ‖v k‖ * ‖w k‖) (T : K →L[ℂ] K) : Summable fun (k : ℕ) => inner ℂ (v k) (T (w k))

theorem CommutingRepetition.Density.IsTraceClassFunctional.add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {φ ψ : (K →L[ℂ] K) →ₗ[ℂ] ℂ} (hφ : IsTraceClassFunctional φ) (hψ : IsTraceClassFunctional ψ) : IsTraceClassFunctional (φ + ψ)

The faithful perturbation

theorem CommutingRepetition.Density.vecState_star_mul_self {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) : (vecState S) (star T * T) = ↑(‖T S.ψ‖ ^ 2)

structure CommutingRepetition.Density.Perturbed (X Y A B : Type) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Type 1

The data of a faithful perturbation: a strategy, a dense sequence in its Hilbert space and ε ∈ (0, 1].

• S : CommutingStrategy X Y A B
• u : ℕ → self.S.H
• u_dense : DenseRange self.u
• ε : ℝ
• ε_pos : 0 < self.ε
• ε_le : self.ε ≤ 1

theorem CommutingRepetition.Density.Perturbed.u_ne {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) : ∃ (k : ℕ), P.u k ≠ 0

noncomputable def CommutingRepetition.Density.Perturbed.φ {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) : (P.S.H →L[ℂ] P.S.H) →ₗ[ℂ] ℂ

The perturbed (faithful) state (1−ε) ω_ψ + ε φ₀.

Equations

• P.φ = ↑(1 - P.ε) • CommutingRepetition.Density.vecState P.S + ↑P.ε • CommutingRepetition.Density.faithfulState P.u

noncomputable def CommutingRepetition.Density.Perturbed.ω {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) (y : Y) (b : B) : (P.S.H →L[ℂ] P.S.H) →ₗ[ℂ] ℂ

Bob's perturbed functionals (1−ε)⟪ψ, · F_b^y ψ⟫ + (ε/|B|) φ₀.

Equations

• P.ω y b = ↑(1 - P.ε) • CommutingRepetition.Density.bobFun P.S y b + ↑(P.ε / ↑(Fintype.card B)) • CommutingRepetition.Density.faithfulState P.u

noncomputable def CommutingRepetition.Density.Perturbed.corr {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) : Correlation X Y A B

The perturbed correlation re ω_b^y(E_a^x).

Equations

• P.corr x y a b = ((P.ω y b) (P.S.E x a)).re

theorem CommutingRepetition.Density.Perturbed.φ_apply {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) (T : P.S.H →L[ℂ] P.S.H) : P.φ T = ↑(1 - P.ε) * (vecState P.S) T + ↑P.ε * (faithfulState P.u) T

theorem CommutingRepetition.Density.Perturbed.ω_apply {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) (y : Y) (b : B) (T : P.S.H →L[ℂ] P.S.H) : (P.ω y b) T = ↑(1 - P.ε) * (bobFun P.S y b) T + ↑(P.ε / ↑(Fintype.card B)) * (faithfulState P.u) T

theorem CommutingRepetition.Density.Perturbed.φ_one {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) : P.φ 1 = 1

theorem CommutingRepetition.Density.Perturbed.φ_star_mul_self {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) (T : P.S.H →L[ℂ] P.S.H) : P.φ (star T * T) = ↑((1 - P.ε) * ‖T P.S.ψ‖ ^ 2 + P.ε * ((Z P.u)⁻¹ * ∑' (k : ℕ), wt k * ‖T (nv P.u k)‖ ^ 2))

theorem CommutingRepetition.Density.Perturbed.φ_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) (T : P.S.H →L[ℂ] P.S.H) : 0 ≤ P.φ (star T * T)

theorem CommutingRepetition.Density.Perturbed.φ_faithful {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) (T : P.S.H →L[ℂ] P.S.H) (h : P.φ (star T * T) = 0) : T = 0

The perturbed state is faithful on B(H).

theorem CommutingRepetition.Density.Perturbed.ω_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) [Nonempty B] (y : Y) : ∑ b : B, P.ω y b = P.φ

theorem CommutingRepetition.Density.Perturbed.ω_nonneg_of_commute {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) [Nonempty B] (y : Y) (b : B) {T : P.S.H →L[ℂ] P.S.H} (hT : Commute T (P.S.F y b)) : 0 ≤ (P.ω y b) (star T * T)

Bob's perturbed functionals are positive on operators commuting with Bob's effect.

theorem CommutingRepetition.Density.Perturbed.φ_traceClass {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) [Nonempty B] : IsTraceClassFunctional P.φ

theorem CommutingRepetition.Density.Perturbed.ω_traceClass {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) [Nonempty B] (y : Y) (b : B) : IsTraceClassFunctional (P.ω y b)

theorem CommutingRepetition.Density.Perturbed.corr_eq {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) [Nonempty B] (x : X) (y : Y) (a : A) (b : B) : P.corr x y a b = (1 - P.ε) * P.S.correlation x y a b + P.ε / ↑(Fintype.card B) * ((faithfulState P.u) (P.S.E x a)).re

theorem CommutingRepetition.Density.Perturbed.norm_E_le_one {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) [Nonempty B] (x : X) (a : A) : ‖P.S.E x a‖ ≤ 1

POVM elements are contractions.

theorem CommutingRepetition.Density.Perturbed.abs_corr_sub_le {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) [Nonempty B] (x : X) (y : Y) (a : A) (b : B) : |P.corr x y a b - P.S.correlation x y a b| ≤ 2 * P.ε

theorem CommutingRepetition.Density.Perturbed.l1Dist_le {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (P : Perturbed X Y A B) [Nonempty B] : l1Dist P.S.correlation P.corr ≤ 2 * P.ε * (↑(Fintype.card X) * ↑(Fintype.card Y) * ↑(Fintype.card A) * ↑(Fintype.card B))

theorem CommutingRepetition.Density.exists_perturbed {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty B] (S : CommutingStrategy X Y A B) {δ : ℝ} (hδ : 0 < δ) : ∃ (P : Perturbed X Y A B), TopologicalSpace.SeparableSpace P.S.H ∧ l1Dist S.correlation P.corr < δ

Stage E1: every commuting correlation is approximated in ℓ¹ by the perturbed correlation of a separable strategy whose perturbed state is faithful.