@[reducible, inline]

abbrev CommutingRepetition.VN.Hinf (H : Type u_2) [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Type u_2

H^∞ = ℓ²(ℕ, H).

Equations

• CommutingRepetition.VN.Hinf H = ↥(lp (fun (x : ℕ) => H) 2)

ℓ² bookkeeping

theorem CommutingRepetition.VN.two_toReal : ENNReal.toReal 2 = 2

theorem CommutingRepetition.VN.summable_norm_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : Hinf H) : Summable fun (i : ℕ) => ‖↑f i‖ ^ 2

theorem CommutingRepetition.VN.norm_sq_eq_tsum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : Hinf H) : ‖f‖ ^ 2 = ∑' (i : ℕ), ‖↑f i‖ ^ 2

theorem CommutingRepetition.VN.memℓp_of_summable_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {g : ℕ → H} (hg : Summable fun (i : ℕ) => ‖g i‖ ^ 2) : Memℓp g 2

noncomputable def CommutingRepetition.VN.mkVec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (g : ℕ → H) (hg : Summable fun (i : ℕ) => ‖g i‖ ^ 2) : Hinf H

The element of ℓ²(ℕ, H) with coordinates g.

Equations

• CommutingRepetition.VN.mkVec g hg = ⟨g, ⋯⟩

theorem CommutingRepetition.VN.mkVec_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (g : ℕ → H) (hg : Summable fun (i : ℕ) => ‖g i‖ ^ 2) (i : ℕ) : ↑(mkVec g hg) i = g i

theorem CommutingRepetition.VN.norm_le_of_tsum_sq_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {f : Hinf H} {C : ℝ} (hC : 0 ≤ C) (h : ∑' (i : ℕ), ‖↑f i‖ ^ 2 ≤ C ^ 2) : ‖f‖ ≤ C

The amplification of an operator

theorem CommutingRepetition.VN.summable_norm_sq_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (f : Hinf H) : Summable fun (i : ℕ) => ‖x (↑f i)‖ ^ 2

noncomputable def CommutingRepetition.VN.amplPre {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : Hinf H →ₗ[ℂ] Hinf H

x ⊗ 1 as a linear map.

Equations

• CommutingRepetition.VN.amplPre x = { toFun := fun (f : CommutingRepetition.VN.Hinf H) => CommutingRepetition.VN.mkVec (fun (i : ℕ) => x (↑f i)) ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem CommutingRepetition.VN.amplPre_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (f : Hinf H) (i : ℕ) : ↑((amplPre x) f) i = x (↑f i)

theorem CommutingRepetition.VN.norm_amplPre_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (f : Hinf H) : ‖(amplPre x) f‖ ≤ ‖x‖ * ‖f‖

noncomputable def CommutingRepetition.VN.ampl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : Hinf H →L[ℂ] Hinf H

The amplification x ⊗ 1 on ℓ²(ℕ, H).

Equations

• CommutingRepetition.VN.ampl x = (CommutingRepetition.VN.amplPre x).mkContinuous ‖x‖ ⋯

theorem CommutingRepetition.VN.ampl_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (f : Hinf H) (i : ℕ) : ↑((ampl x) f) i = x (↑f i)

theorem CommutingRepetition.VN.norm_ampl_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : ‖ampl x‖ ≤ ‖x‖

theorem CommutingRepetition.VN.ampl_ext {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x : H →L[ℂ] H} {T : Hinf H →L[ℂ] Hinf H} (h : ∀ (f : Hinf H) (i : ℕ), ↑(T f) i = x (↑f i)) : T = ampl x

theorem CommutingRepetition.VN.ampl_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x y : H →L[ℂ] H) : ampl (x + y) = ampl x + ampl y

theorem CommutingRepetition.VN.ampl_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : ℂ) (x : H →L[ℂ] H) : ampl (c • x) = c • ampl x

theorem CommutingRepetition.VN.ampl_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : ampl 0 = 0

theorem CommutingRepetition.VN.ampl_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : ampl 1 = 1

theorem CommutingRepetition.VN.ampl_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x y : H →L[ℂ] H) : ampl (x * y) = ampl x * ampl y

theorem CommutingRepetition.VN.inner_ampl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (f g : Hinf H) : inner ℂ ((ampl x) f) g = ∑' (i : ℕ), inner ℂ (x (↑f i)) (↑g i)

theorem CommutingRepetition.VN.inner_ampl_right {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (f g : Hinf H) : inner ℂ f ((ampl x) g) = ∑' (i : ℕ), inner ℂ (↑f i) (x (↑g i))

theorem CommutingRepetition.VN.ampl_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : ampl (star x) = star (ampl x)

theorem CommutingRepetition.VN.isNormalMap_ampl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : IsNormalMap ampl

Amplification preserves bounded strong convergence.

Coordinate embeddings and matrix units

noncomputable def CommutingRepetition.VN.sgl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (j : ℕ) : H →L[ℂ] Hinf H

The j-th coordinate embedding H → ℓ²(ℕ, H).

Equations

• CommutingRepetition.VN.sgl j = lp.singleContinuousLinearMap ℂ (fun (x : ℕ) => H) 2 j

noncomputable def CommutingRepetition.VN.ev {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (j : ℕ) : Hinf H →L[ℂ] H

The j-th coordinate evaluation ℓ²(ℕ, H) → H.

Equations

• CommutingRepetition.VN.ev j = lp.evalCLM ℂ (fun (x : ℕ) => H) 2 j

theorem CommutingRepetition.VN.ev_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (j : ℕ) (f : Hinf H) : (ev j) f = ↑f j

theorem CommutingRepetition.VN.sgl_apply_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (j : ℕ) (v : H) : ↑((sgl j) v) j = v

theorem CommutingRepetition.VN.sgl_apply_ne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (j : ℕ) (v : H) {i : ℕ} (h : i ≠ j) : ↑((sgl j) v) i = 0

theorem CommutingRepetition.VN.ev_sgl_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (j : ℕ) (v : H) : (ev j) ((sgl j) v) = v

theorem CommutingRepetition.VN.ev_sgl_ne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {i j : ℕ} (h : i ≠ j) (v : H) : (ev i) ((sgl j) v) = 0

theorem CommutingRepetition.VN.ampl_sgl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (j : ℕ) (v : H) : (ampl x) ((sgl j) v) = (sgl j) (x v)

theorem CommutingRepetition.VN.ev_ampl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (j : ℕ) (f : Hinf H) : (ev j) ((ampl x) f) = x ((ev j) f)

theorem CommutingRepetition.VN.ev_ampl_sgl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (j : ℕ) (v : H) : (ev j) ((ampl x) ((sgl j) v)) = x v

theorem CommutingRepetition.VN.ampl_injective {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Function.Injective ampl

noncomputable def CommutingRepetition.VN.unit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (j k : ℕ) : Hinf H →L[ℂ] Hinf H

The matrix unit e_j e_k*.

Equations

• CommutingRepetition.VN.unit j k = CommutingRepetition.VN.sgl j ∘SL CommutingRepetition.VN.ev k

theorem CommutingRepetition.VN.unit_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (j k : ℕ) (f : Hinf H) : (unit j k) f = (sgl j) (↑f k)

theorem CommutingRepetition.VN.unit_mul_ampl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) (j k : ℕ) : unit j k * ampl x = ampl x * unit j k

theorem CommutingRepetition.VN.hasSum_sgl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : Hinf H) : HasSum (fun (k : ℕ) => (sgl k) (↑f k)) f

The amplified von Neumann algebra

theorem CommutingRepetition.VN.eq_ampl_of_commute_units {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : Hinf H →L[ℂ] Hinf H) (h : ∀ (j k : ℕ), unit j k * T = T * unit j k) : T = ampl (ev 0 ∘SL T ∘SL sgl 0)

An operator on ℓ²(ℕ, H) commuting with all matrix units is an amplification.

noncomputable def CommutingRepetition.VN.amplAlg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) : VonNeumannAlgebra (Hinf H)

The amplification N ⊗ 1 of a von Neumann algebra.

Equations

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

theorem CommutingRepetition.VN.mem_amplAlg_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) {T : Hinf H →L[ℂ] Hinf H} : T ∈ amplAlg N ↔ ∃ x ∈ N, ampl x = T

theorem CommutingRepetition.VN.ampl_mem_amplAlg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) {x : H →L[ℂ] H} (hx : x ∈ N) : ampl x ∈ amplAlg N

Vector states

theorem CommutingRepetition.VN.inner_mkVec_ampl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (g : ℕ → H) (hg : Summable fun (i : ℕ) => ‖g i‖ ^ 2) (T : H →L[ℂ] H) : inner ℂ (mkVec g hg) ((ampl T) (mkVec g hg)) = ∑' (k : ℕ), inner ℂ (g k) (T (g k))

⟪Ξ, (T ⊗ 1) Ξ⟫ = ∑ ⟪ξ_k, T ξ_k⟫.

theorem CommutingRepetition.VN.isSeparating_mkVec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (g : ℕ → H) (hg : Summable fun (i : ℕ) => ‖g i‖ ^ 2) {S : Set (H →L[ℂ] H)} (hS : ∀ x ∈ S, ∑' (k : ℕ), inner ℂ (g k) ((star x * x) (g k)) = 0 → x = 0) : IsSeparating (ampl '' S) (mkVec g hg)

If the state T ↦ ∑ ⟪g k, T (g k)⟫ is faithful on S, the vector (g k) is separating for the amplification of S.