Star projections and invariant subspaces

theorem CommutingRepetition.VN.commute_of_range_invariant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {e y : H →L[ℂ] H} (he : IsStarProjection e) (h : ∀ (v : H), e (y (e v)) = y (e v)) (h' : ∀ (v : H), e ((star y) (e v)) = (star y) (e v)) : Commute e y

A star projection commutes with every operator that, together with its adjoint, leaves its range invariant.

Matrix entries on ℓ²(ℕ, H)

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

The (j, k) matrix entry of an operator on ℓ²(ℕ, H).

Equations

• CommutingRepetition.VN.entry T j k = CommutingRepetition.VN.ev j ∘SL T ∘SL CommutingRepetition.VN.sgl k

theorem CommutingRepetition.VN.entry_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : Hinf H →L[ℂ] Hinf H) (j k : ℕ) (v : H) : (entry T j k) v = ↑(T ((sgl k) v)) j

theorem CommutingRepetition.VN.commute_entry_of_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : Hinf H →L[ℂ] Hinf H} {x : H →L[ℂ] H} (h : Commute T (ampl x)) (j k : ℕ) : Commute (entry T j k) x

theorem CommutingRepetition.VN.commute_ampl_of_entries {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : Hinf H →L[ℂ] Hinf H} {x : H →L[ℂ] H} (h : ∀ (j k : ℕ), Commute (entry T j k) x) : Commute T (ampl x)

The density theorem

theorem CommutingRepetition.VN.inner_ampl_eq_zero_of_mem_wstar {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} (𝔄 : StarSubalgebra ℂ (H →L[ℂ] H)) (hS : S ⊆ ↑𝔄) {x : H →L[ℂ] H} (hx : x ∈ wstar S) (U V : Hinf H) (h : ∀ a ∈ 𝔄, inner ℂ U ((ampl a) V) = 0) : inner ℂ U ((ampl x) V) = 0

von Neumann density for vector functionals. If S ⊆ 𝔄 with 𝔄 a *-subalgebra, x ∈ W*(S) and ⟪U, (a ⊗ 1) V⟫ = 0 for all a ∈ 𝔄, then ⟪U, (x ⊗ 1) V⟫ = 0.

Two-vector form

theorem CommutingRepetition.VN.inner_sgl_sgl_nat {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (j k : ℕ) (u v : H) : inner ℂ ((sgl j) u) ((sgl k) v) = if j = k then inner ℂ u v else 0

theorem CommutingRepetition.VN.inner_pair_ampl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) (u₁ u₂ v₁ v₂ : H) : inner ℂ ((sgl 0) u₁ + (sgl 1) u₂) ((ampl a) ((sgl 0) v₁ + (sgl 1) v₂)) = inner ℂ u₁ (a v₁) + inner ℂ u₂ (a v₂)

theorem CommutingRepetition.VN.inner_pair_eq_zero_of_mem_wstar {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} (𝔄 : StarSubalgebra ℂ (H →L[ℂ] H)) (hS : S ⊆ ↑𝔄) {x : H →L[ℂ] H} (hx : x ∈ wstar S) (u₁ u₂ v₁ v₂ : H) (h : ∀ a ∈ 𝔄, inner ℂ u₁ (a v₁) + inner ℂ u₂ (a v₂) = 0) : inner ℂ u₁ (x v₁) + inner ℂ u₂ (x v₂) = 0

Density for a pair of vector functionals: if ⟪u₁, a v₁⟫ + ⟪u₂, a v₂⟫ = 0 for all a ∈ 𝔄 then also for x ∈ W*(S).

theorem CommutingRepetition.VN.inner_eq_zero_of_mem_wstar {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} (𝔄 : StarSubalgebra ℂ (H →L[ℂ] H)) (hS : S ⊆ ↑𝔄) {x : H →L[ℂ] H} (hx : x ∈ wstar S) (u v : H) (h : ∀ a ∈ 𝔄, inner ℂ u (a v) = 0) : inner ℂ u (x v) = 0

Density for one vector functional.