theorem CommutingRepetition.VN.WOT.eq_of_clusterPt_of_tendsto {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] {ι : Type u_3} {l : Filter ι} [l.NeBot] {f : ι → Y} {y L : Y} (h : ClusterPt y (Filter.map f l)) (hf : Filter.Tendsto f l (nhds L)) : y = L

A cluster point of a convergent sequence is its limit.

theorem CommutingRepetition.VN.WOT.clusterPt_map_seq {Y : Type u_2} {Z : Type u_3} [TopologicalSpace Y] [TopologicalSpace Z] {ι : Type u_4} {l : Filter ι} {f : ι → Y} {y : Y} (h : ClusterPt y (Filter.map f l)) {Φ : Y → Z} (hΦ : Continuous Φ) : ClusterPt (Φ y) (Filter.map (fun (i : ι) => Φ (f i)) l)

Cluster points are transported by continuous maps.

noncomputable def CommutingRepetition.VN.WOT.coeff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) : H × H → ℂ

The matrix coefficients of an operator.

Equations

• CommutingRepetition.VN.WOT.coeff T p = inner ℂ (T p.1) p.2

theorem CommutingRepetition.VN.WOT.coeff_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : H →L[ℂ] H) (ζ ξ : H) : coeff T (ζ, ξ) = inner ℂ (T ζ) ξ

def CommutingRepetition.VN.WOT.box {H : Type u_1} [NormedAddCommGroup H] : Set (H × H → ℂ)

The compact box containing the coefficient functions of the unit ball.

Equations

• CommutingRepetition.VN.WOT.box = Set.univ.pi fun (p : H × H) => Metric.closedBall 0 (‖p.1‖ * ‖p.2‖)

theorem CommutingRepetition.VN.WOT.isCompact_box {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : IsCompact box

theorem CommutingRepetition.VN.WOT.coeff_mem_box {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →L[ℂ] H} (hT : ‖T‖ ≤ 1) : coeff T ∈ box

theorem CommutingRepetition.VN.WOT.F_eq_of_forall {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) {Φ : (H × H → ℂ) → ℂ} (hΦ : Continuous Φ) (h : ∀ (n : ℕ), Φ (coeff (x n)) = 0) : Φ F = 0

A closed identity satisfied by all coeff (x n) is satisfied by F.

theorem CommutingRepetition.VN.WOT.F_add_right {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (ζ ξ₁ ξ₂ : H) : F (ζ, ξ₁ + ξ₂) = F (ζ, ξ₁) + F (ζ, ξ₂)

theorem CommutingRepetition.VN.WOT.F_smul_right {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (ζ ξ : H) (c : ℂ) : F (ζ, c • ξ) = c * F (ζ, ξ)

theorem CommutingRepetition.VN.WOT.F_add_left {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (ζ₁ ζ₂ ξ : H) : F (ζ₁ + ζ₂, ξ) = F (ζ₁, ξ) + F (ζ₂, ξ)

theorem CommutingRepetition.VN.WOT.F_smul_left {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (ζ ξ : H) (c : ℂ) : F (c • ζ, ξ) = (starRingEnd ℂ) c * F (ζ, ξ)

theorem CommutingRepetition.VN.WOT.F_symm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (ζ ξ : H) : F (ζ, ξ) = (starRingEnd ℂ) (F (ξ, ζ))

theorem CommutingRepetition.VN.WOT.F_commutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) {y : H →L[ℂ] H} (hy : y ∈ N.commutant) (ζ ξ : H) : F (ζ, (star y) ξ) = F (y ζ, ξ)

theorem CommutingRepetition.VN.WOT.F_bound {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (hbox : F ∈ box) (ζ ξ : H) : ‖F (ζ, ξ)‖ ≤ ‖ζ‖ * ‖ξ‖

noncomputable def CommutingRepetition.VN.WOT.sesq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (hbox : F ∈ box) : H →L⋆[ℂ] H →L[ℂ] ℂ

The sesquilinear form F as a bounded sesquilinear map.

Equations

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

theorem CommutingRepetition.VN.WOT.sesq_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (hbox : F ∈ box) (ζ ξ : H) : ((sesq N x hx hF hbox) ζ) ξ = F (ζ, ξ)

noncomputable def CommutingRepetition.VN.WOT.limOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (hbox : F ∈ box) : H →L[ℂ] H

The operator L with ⟪L ζ, ξ⟫ = F (ζ, ξ).

Equations

• CommutingRepetition.VN.WOT.limOp N x hx hF hbox = InnerProductSpace.continuousLinearMapOfBilin (CommutingRepetition.VN.WOT.sesq N x hx hF hbox)

theorem CommutingRepetition.VN.WOT.inner_limOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (hbox : F ∈ box) (ζ ξ : H) : inner ℂ ((limOp N x hx hF hbox) ζ) ξ = F (ζ, ξ)

theorem CommutingRepetition.VN.WOT.limOp_isSelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (hbox : F ∈ box) : IsSelfAdjoint (limOp N x hx hF hbox)

theorem CommutingRepetition.VN.WOT.limOp_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (hbox : F ∈ box) : limOp N x hx hF hbox ∈ N

theorem CommutingRepetition.VN.WOT.norm_limOp_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (hbox : F ∈ box) : ‖limOp N x hx hF hbox‖ ≤ 1

theorem CommutingRepetition.VN.WOT.clusterPt_inner_limOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) {F : H × H → ℂ} (hF : ClusterPt F (Filter.map (fun (n : ℕ) => coeff (x n)) Filter.atTop)) (hbox : F ∈ box) (ζ ξ : H) : ClusterPt (inner ℂ ((limOp N x hx hF hbox) ζ) ξ) (Filter.map (fun (n : ℕ) => inner ℂ ((x n) ζ) ξ) Filter.atTop)

theorem CommutingRepetition.VN.WOT.exists_clusterPt_saBall {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (x : ℕ → H →L[ℂ] H) (hx : ∀ (n : ℕ), x n ∈ N ∧ IsSelfAdjoint (x n) ∧ ‖x n‖ ≤ 1) : ∃ L ∈ N, IsSelfAdjoint L ∧ ‖L‖ ≤ 1 ∧ ∀ (ζ ξ : H), ClusterPt (inner ℂ (L ζ) ξ) (Filter.map (fun (n : ℕ) => inner ℂ ((x n) ζ) ξ) Filter.atTop)

WOT compactness of the self-adjoint unit ball of a von Neumann algebra, in cluster-point form: a sequence in {x ∈ N | x = x*, ‖x‖ ≤ 1} has a cluster point L in that set, with every matrix coefficient ⟪L ζ, ξ⟫ a cluster point of n ↦ ⟪x n ζ, ξ⟫.

theorem CommutingRepetition.VN.WOT.tendsto_eq_of_clusterPt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {L : H →L[ℂ] H} {x : ℕ → H →L[ℂ] H} {ζ ξ : H} (hL : ClusterPt (inner ℂ (L ζ) ξ) (Filter.map (fun (n : ℕ) => inner ℂ ((x n) ζ) ξ) Filter.atTop)) {Φ : ℂ → ℝ} (hΦ : Continuous Φ) {r : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => Φ (inner ℂ ((x n) ζ) ξ)) Filter.atTop (nhds r)) : Φ (inner ℂ (L ζ) ξ) = r

Consequence used in RvD Lemma 4.3: if a continuous real function of the coefficients converges along the sequence, its limit is the value at L.