theorem CommutingRepetition.VN.smul_mem_vn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (c : ℂ) {y : H →L[ℂ] H} (hy : y ∈ N) : c • y ∈ N

The n = 1 matrix trick on an abstract Hilbert space

(Stated on an abstract type: the continuous functional calculus instance is not found on the operator algebra of a subtype ↥K, so the square root is taken here and the result is instantiated at E := ↥K below.)

theorem CommutingRepetition.VN.re_inner_apply_le_of_commute {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (b S : E →L[ℂ] E) (hb : 0 ≤ b) (hS : Commute b S) (v : E) : RCLike.re (inner ℂ (S v) (b (S v))) ≤ ‖S‖ ^ 2 * RCLike.re (inner ℂ v (b v))

For 0 ≤ b commuting with S: re ⟪S v, b (S v)⟫ ≤ ‖S‖² re ⟪v, b v⟫ (via b = r²).

Compression of a single operator

noncomputable def CommutingRepetition.VN.compressTo {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (K : Submodule ℂ H) [CompleteSpace ↥K] (T : H →L[ℂ] H) : ↥K →L[ℂ] ↥K

The compression P T ι : K → K of an operator on H.

Equations

• CommutingRepetition.VN.compressTo K T = K.orthogonalProjectionOnto ∘SL T ∘SL K.subtypeL

theorem CommutingRepetition.VN.compressTo_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (T : H →L[ℂ] H) (v : ↥K) : (compressTo K T) v = K.orthogonalProjectionOnto (T ↑v)

theorem CommutingRepetition.VN.coe_compressTo_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (T : H →L[ℂ] H) (v : ↥K) : ↑((compressTo K T) v) = K.starProjection (T ↑v)

theorem CommutingRepetition.VN.coe_compressTo_apply_of_invariant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] {T : H →L[ℂ] H} (hT : ∀ v ∈ K, T v ∈ K) (v : ↥K) : ↑((compressTo K T) v) = T ↑v

theorem CommutingRepetition.VN.inner_compressTo_left {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (T : H →L[ℂ] H) (v w : ↥K) : inner ℂ ((compressTo K T) v) w = inner ℂ (T ↑v) ↑w

theorem CommutingRepetition.VN.inner_compressTo_right {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (T : H →L[ℂ] H) (v w : ↥K) : inner ℂ v ((compressTo K T) w) = inner ℂ (↑v) (T ↑w)

theorem CommutingRepetition.VN.compressTo_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (S T : H →L[ℂ] H) : compressTo K (S + T) = compressTo K S + compressTo K T

theorem CommutingRepetition.VN.compressTo_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (c : ℂ) (T : H →L[ℂ] H) : compressTo K (c • T) = c • compressTo K T

theorem CommutingRepetition.VN.compressTo_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] : compressTo K 0 = 0

theorem CommutingRepetition.VN.compressTo_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] : compressTo K 1 = 1

theorem CommutingRepetition.VN.compressTo_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (T : H →L[ℂ] H) : compressTo K (star T) = star (compressTo K T)

theorem CommutingRepetition.VN.compressTo_mul_of_invariant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (S : H →L[ℂ] H) {T : H →L[ℂ] H} (hT : ∀ v ∈ K, T v ∈ K) : compressTo K (S * T) = compressTo K S * compressTo K T

theorem CommutingRepetition.VN.compressTo_mul_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (S T : H →L[ℂ] H) : compressTo K S * compressTo K T = compressTo K (S * K.starProjection * T)

P S ι P T ι = P (S p T) ι.

theorem CommutingRepetition.VN.compressTo_starProjection_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (T : H →L[ℂ] H) : compressTo K (K.starProjection * T) = compressTo K T

theorem CommutingRepetition.VN.norm_compressTo_apply_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (T : H →L[ℂ] H) (v : ↥K) : ‖(compressTo K T) v‖ ≤ ‖T‖ * ‖v‖

theorem CommutingRepetition.VN.norm_compressTo_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (T : H →L[ℂ] H) : ‖compressTo K T‖ ≤ ‖T‖

theorem CommutingRepetition.VN.isNormalMap_compressTo {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] : IsNormalMap (compressTo K)

Compression preserves bounded strong convergence.

theorem CommutingRepetition.VN.compressTo_star_mul_self_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (y : H →L[ℂ] H) : 0 ≤ compressTo K (star y * y)

P y*y ι is a positive operator on K.

theorem CommutingRepetition.VN.norm_apply_apply_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (S : ↥K →L[ℂ] ↥K) (y : H →L[ℂ] H) (hS : Commute (compressTo K (star y * y)) S) (v : ↥K) : ‖y ↑(S v)‖ ≤ ‖S‖ * ‖y ↑v‖

If S commutes with P y*y ι then ‖y (S v)‖ ≤ ‖S‖ ‖y v‖.

The compressed algebra and the commutant

theorem CommutingRepetition.VN.starProjection_mem_commutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (N : VonNeumannAlgebra H) (hK : ∀ x ∈ N, ∀ v ∈ K, x v ∈ K) : K.starProjection ∈ N.commutant

The projection onto an N-invariant subspace lies in N′.

theorem CommutingRepetition.VN.compressTo_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (N : VonNeumannAlgebra H) (hK : ∀ x ∈ N, ∀ v ∈ K, x v ∈ K) (x : H →L[ℂ] H) {y : H →L[ℂ] H} (hy : y ∈ N) : compressTo K (x * y) = compressTo K x * compressTo K y

theorem CommutingRepetition.VN.compressTo_commute_commutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (N : VonNeumannAlgebra H) (hK : ∀ x ∈ N, ∀ v ∈ K, x v ∈ K) {x y : H →L[ℂ] H} (hx : x ∈ N) (hy : y ∈ N.commutant) : compressTo K x * compressTo K y = compressTo K y * compressTo K x

Compressions of N and of N′ commute.

Extension of an operator commuting with the compressed commutant

def CommutingRepetition.VN.commOrbit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) : Submodule ℂ H

The orbit N′ ξ (a linear subspace, as N′ is an algebra).

Equations

• CommutingRepetition.VN.commOrbit N ξ = CommutingRepetition.VN.orbit (↑N.commutant) ξ

theorem CommutingRepetition.VN.exists_rep {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) {v : H} (hv : v ∈ commOrbit N ξ) : ∃ y ∈ N.commutant, y ξ = v

theorem CommutingRepetition.VN.apply_mem_commOrbit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) {y : H →L[ℂ] H} (hy : y ∈ N.commutant) : y ξ ∈ commOrbit N ξ

theorem CommutingRepetition.VN.dense_commOrbit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) {ξ : H} (hξ : IsSeparating (↑N) ξ) : Dense ↑(commOrbit N ξ)

noncomputable def CommutingRepetition.VN.rep {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) (v : ↥(commOrbit N ξ)) : H →L[ℂ] H

A representative y ∈ N′ with y ξ = v for v ∈ N′ ξ.

Equations

• CommutingRepetition.VN.rep N ξ v = ⋯.choose

theorem CommutingRepetition.VN.rep_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) (v : ↥(commOrbit N ξ)) : rep N ξ v ∈ N.commutant

theorem CommutingRepetition.VN.rep_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) (v : ↥(commOrbit N ξ)) : (rep N ξ v) ξ = ↑v

theorem CommutingRepetition.VN.norm_apply_le_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] {N : VonNeumannAlgebra H} (S : ↥K →L[ℂ] ↥K) (hS : ∀ y ∈ N.commutant, compressTo K y * S = S * compressTo K y) {y : H →L[ℂ] H} (hy : y ∈ N.commutant) (v : ↥K) : ‖y ↑(S v)‖ ≤ ‖S‖ * ‖y ↑v‖

theorem CommutingRepetition.VN.apply_eq_of_apply_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] {N : VonNeumannAlgebra H} (ξ : H) (hξK : ξ ∈ K) (S : ↥K →L[ℂ] ↥K) (hS : ∀ y ∈ N.commutant, compressTo K y * S = S * compressTo K y) {y y' : H →L[ℂ] H} (hy : y ∈ N.commutant) (hy' : y' ∈ N.commutant) (h : y ξ = y' ξ) : y ↑(S ⟨ξ, hξK⟩) = y' ↑(S ⟨ξ, hξK⟩)

Two elements of N′ agreeing at ξ agree at S ξ.

noncomputable def CommutingRepetition.VN.extPre {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] {N : VonNeumannAlgebra H} (ξ : H) (hξK : ξ ∈ K) (S : ↥K →L[ℂ] ↥K) (hS : ∀ y ∈ N.commutant, compressTo K y * S = S * compressTo K y) : ↥(commOrbit N ξ) →L[ℂ] H

x̃ on N′ ξ: y ξ ↦ y (S ξ).

Equations

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

theorem CommutingRepetition.VN.extPre_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] {N : VonNeumannAlgebra H} (ξ : H) (hξK : ξ ∈ K) (S : ↥K →L[ℂ] ↥K) (hS : ∀ y ∈ N.commutant, compressTo K y * S = S * compressTo K y) (v : ↥(commOrbit N ξ)) : (extPre K ξ hξK S hS) v = (rep N ξ v) ↑(S ⟨ξ, hξK⟩)

theorem CommutingRepetition.VN.denseRange_subtypeL_commOrbit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {N : VonNeumannAlgebra H} (ξ : H) (hξ : IsSeparating (↑N) ξ) : DenseRange ⇑(commOrbit N ξ).subtypeL

theorem CommutingRepetition.VN.isUniformInducing_subtypeL_commOrbit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {N : VonNeumannAlgebra H} (ξ : H) : IsUniformInducing ⇑(commOrbit N ξ).subtypeL

noncomputable def CommutingRepetition.VN.extOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] {N : VonNeumannAlgebra H} (ξ : H) (hξK : ξ ∈ K) (S : ↥K →L[ℂ] ↥K) (hS : ∀ y ∈ N.commutant, compressTo K y * S = S * compressTo K y) : H →L[ℂ] H

The extension x̃ ∈ B(H) of y ξ ↦ y (S ξ).

Equations

• CommutingRepetition.VN.extOp K ξ hξK S hS = (CommutingRepetition.VN.extPre K ξ hξK S hS).extend (CommutingRepetition.VN.commOrbit N ξ).subtypeL

theorem CommutingRepetition.VN.extOp_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] {N : VonNeumannAlgebra H} (ξ : H) (hξK : ξ ∈ K) (S : ↥K →L[ℂ] ↥K) (hS : ∀ y ∈ N.commutant, compressTo K y * S = S * compressTo K y) (hξ : IsSeparating (↑N) ξ) {y : H →L[ℂ] H} (hy : y ∈ N.commutant) : (extOp K ξ hξK S hS) (y ξ) = y ↑(S ⟨ξ, hξK⟩)

theorem CommutingRepetition.VN.extOp_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] {N : VonNeumannAlgebra H} (ξ : H) (hξK : ξ ∈ K) (S : ↥K →L[ℂ] ↥K) (hS : ∀ y ∈ N.commutant, compressTo K y * S = S * compressTo K y) (hξ : IsSeparating (↑N) ξ) : extOp K ξ hξK S hS ∈ N

theorem CommutingRepetition.VN.compressTo_extOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] {N : VonNeumannAlgebra H} (hK : ∀ x ∈ N, ∀ v ∈ K, x v ∈ K) (ξ : H) (hξK : ξ ∈ K) (S : ↥K →L[ℂ] ↥K) (hS : ∀ y ∈ N.commutant, compressTo K y * S = S * compressTo K y) (hξ : IsSeparating (↑N) ξ) : compressTo K (extOp K ξ hξK S hS) = S

theorem CommutingRepetition.VN.exists_compressTo_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] {N : VonNeumannAlgebra H} (hK : ∀ x ∈ N, ∀ v ∈ K, x v ∈ K) (ξ : H) (hξK : ξ ∈ K) (S : ↥K →L[ℂ] ↥K) (hS : ∀ y ∈ N.commutant, compressTo K y * S = S * compressTo K y) (hξ : IsSeparating (↑N) ξ) : ∃ x ∈ N, compressTo K x = S

An operator on K commuting with the compressed commutant is a compression of N.

The compressed von Neumann algebra

noncomputable def CommutingRepetition.VN.cutdown {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (N : VonNeumannAlgebra H) (hK : ∀ x ∈ N, ∀ v ∈ K, x v ∈ K) (ξ : H) (hξK : ξ ∈ K) (hξ : IsSeparating (↑N) ξ) : VonNeumannAlgebra ↥K

The compressed algebra {P x ι | x ∈ N} on an invariant subspace containing a separating vector is a von Neumann algebra on K.

Equations

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

theorem CommutingRepetition.VN.mem_cutdown_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (N : VonNeumannAlgebra H) (hK : ∀ x ∈ N, ∀ v ∈ K, x v ∈ K) (ξ : H) (hξK : ξ ∈ K) (hξ : IsSeparating (↑N) ξ) {S : ↥K →L[ℂ] ↥K} : S ∈ cutdown K N hK ξ hξK hξ ↔ ∃ x ∈ N, compressTo K x = S

theorem CommutingRepetition.VN.compressTo_mem_cutdown {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (N : VonNeumannAlgebra H) (hK : ∀ x ∈ N, ∀ v ∈ K, x v ∈ K) (ξ : H) (hξK : ξ ∈ K) (hξ : IsSeparating (↑N) ξ) {x : H →L[ℂ] H} (hx : x ∈ N) : compressTo K x ∈ cutdown K N hK ξ hξK hξ

theorem CommutingRepetition.VN.compressTo_injective {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (N : VonNeumannAlgebra H) (hK : ∀ x ∈ N, ∀ v ∈ K, x v ∈ K) (ξ : H) (hξK : ξ ∈ K) (hξ : IsSeparating (↑N) ξ) {x y : H →L[ℂ] H} (hx : x ∈ N) (hy : y ∈ N) (h : compressTo K x = compressTo K y) : x = y

Compression is injective on N (the separating vector lies in K).

theorem CommutingRepetition.VN.isSeparating_cutdown {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (K : Submodule ℂ H) [CompleteSpace ↥K] (N : VonNeumannAlgebra H) (hK : ∀ x ∈ N, ∀ v ∈ K, x v ∈ K) (ξ : H) (hξK : ξ ∈ K) (hξ : IsSeparating (↑N) ξ) : IsSeparating ↑(cutdown K N hK ξ hξK hξ) ⟨ξ, hξK⟩

The separating vector is separating for the compressed algebra.

theorem CommutingRepetition.VN.cyclicSpace_invariant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) (x : H →L[ℂ] H) : x ∈ N → ∀ v ∈ cyclicSpace (↑N) ξ, x v ∈ cyclicSpace (↑N) ξ

The cyclic subspace [N ξ] is N-invariant.

theorem CommutingRepetition.VN.isCyclic_cutdown_cyclicSpace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) (hξ : IsSeparating (↑N) ξ) : IsCyclic ↑(cutdown (cyclicSpace (↑N) ξ) N ⋯ ξ ⋯ hξ) ⟨ξ, ⋯⟩

On the cyclic subspace K = [N ξ], the vector ξ is cyclic for the compressed algebra.