Bridging: matrix coefficients and convergence

theorem Orthogonalization.MvN.continuous_inner_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ξ η : H) : Continuous fun (T : H →WOT[ℂ] H) => inner ℂ ξ (T η)

The matrix coefficient T ↦ ⟪ξ, T η⟫ is continuous for the weak operator topology.

theorem Orthogonalization.MvN.continuous_inner_apply' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ξ η : H) : Continuous fun (T : H →WOT[ℂ] H) => inner ℂ (T ξ) η

The matrix coefficient T ↦ ⟪T ξ, η⟫ is continuous for the weak operator topology.

theorem Orthogonalization.MvN.tendsto_iff_forall_inner_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} {f : κ → H →WOT[ℂ] H} {A : H →WOT[ℂ] H} : Filter.Tendsto f l (nhds A) ↔ ∀ (ξ η : H), Filter.Tendsto (fun (k : κ) => inner ℂ ξ ((f k) η)) l (nhds (inner ℂ ξ (A η)))

Convergence in the weak operator topology is convergence of every matrix coefficient ⟪ξ, · η⟫: Mathlib's tendsto_iff_forall_dual_apply_tendsto through the Riesz representation of the dual of H.

theorem Orthogonalization.MvN.tendsto_iff_forall_inner_tendsto' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} {f : κ → H →WOT[ℂ] H} {A : H →WOT[ℂ] H} : Filter.Tendsto f l (nhds A) ↔ ∀ (ξ η : H), Filter.Tendsto (fun (k : κ) => inner ℂ ((f k) ξ) η) l (nhds (inner ℂ (A ξ) η))

Convergence in the weak operator topology, through the coefficients ⟪· ξ, η⟫.

theorem Orthogonalization.MvN.tendsto_ofCLM_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} {T : κ → H →L[ℂ] H} {L : H →L[ℂ] H} : Filter.Tendsto (fun (k : κ) => ContinuousLinearMapWOT.ofCLM (T k)) l (nhds (ContinuousLinearMapWOT.ofCLM L)) ↔ ∀ (ξ η : H), Filter.Tendsto (fun (k : κ) => inner ℂ ξ ((T k) η)) l (nhds (inner ℂ ξ (L η)))

Convergence in the weak operator topology of a family of operators of H →L[ℂ] H, in terms of matrix coefficients.

Compactness of the norm-bounded sets

theorem Orthogonalization.MvN.isCompact_setOf_norm_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (r : ℝ) : IsCompact {T : H →WOT[ℂ] H | ‖T.toCLM‖ ≤ r}

WOT-compactness of the norm-bounded sets of B(H). Proof by the ultrafilter criterion: along an ultrafilter 𝒰 on {T | ‖T‖ ≤ r}, each coefficient ⟪T ξ, η⟫ lies in the compact disc of radius r ‖ξ‖ ‖η‖, hence converges to some c ξ η; the limit c is sesquilinear and bounded by r ‖ξ‖ ‖η‖, so it is ⟪L ξ, η⟫ for an operator L with ‖L‖ ≤ r, and 𝒰 converges to ofCLM L in the weak operator topology.

theorem Orthogonalization.MvN.isCompact_of_isClosed_of_norm_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →WOT[ℂ] H)} (hS : IsClosed S) {r : ℝ} (hr : ∀ T ∈ S, ‖T.toCLM‖ ≤ r) : IsCompact S

A closed set of operators bounded in norm is WOT-compact.

theorem Orthogonalization.MvN.exists_clusterPt_of_norm_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} [l.NeBot] {T : κ → H →L[ℂ] H} {r : ℝ} (hT : ∀ (k : κ), ‖T k‖ ≤ r) : ∃ (L : H →L[ℂ] H), ‖L‖ ≤ r ∧ ClusterPt (ContinuousLinearMapWOT.ofCLM L) (Filter.map (fun (k : κ) => ContinuousLinearMapWOT.ofCLM (T k)) l)

A norm-bounded family of operators has a WOT cluster point of the same norm bound.

Closed conditions in the weak operator topology

theorem Orthogonalization.MvN.isClosed_setOf_inner_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (ξ η : H) (z : ℂ) : IsClosed {T : H →WOT[ℂ] H | inner ℂ ξ (T η) = z}

Fixing one matrix coefficient is a closed condition.

theorem Orthogonalization.MvN.isClosed_setOf_isSelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : IsClosed {T : H →WOT[ℂ] H | IsSelfAdjoint T.toCLM}

Self-adjointness is a closed condition: it says ⟪T ξ, η⟫ = ⟪ξ, T η⟫ for all ξ, η.

theorem Orthogonalization.MvN.isClosed_setOf_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : IsClosed {T : H →WOT[ℂ] H | 0 ≤ T.toCLM}

Positivity is a closed condition: self-adjointness and 0 ≤ ⟪T ξ, ξ⟫ for all ξ.

theorem Orthogonalization.MvN.isClosed_setOf_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) : IsClosed {T : H →WOT[ℂ] H | T.toCLM ≤ a}

T ≤ a is a closed condition.

theorem Orthogonalization.MvN.isClosed_setOf_ge {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) : IsClosed {T : H →WOT[ℂ] H | a ≤ T.toCLM}

a ≤ T is a closed condition.

theorem Orthogonalization.MvN.isClosed_setOf_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : IsClosed {T : H →WOT[ℂ] H | T.toCLM ≤ 1}

T ≤ 1 is a closed condition.

theorem Orthogonalization.MvN.isClosed_setOf_mul_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (a b : H →L[ℂ] H) : IsClosed {T : H →WOT[ℂ] H | a * T.toCLM * b = T.toCLM}

The support condition a T b = T is closed: left and right multiplication by a fixed operator are WOT-continuous.

theorem Orthogonalization.MvN.isClosed_setOf_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (a : H →L[ℂ] H) : IsClosed {T : H →WOT[ℂ] H | Commute T.toCLM a}

Commutation with a fixed operator is a closed condition.

theorem Orthogonalization.MvN.isClosed_setOf_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) : IsClosed {T : H →WOT[ℂ] H | T.toCLM ∈ M}

Membership in a von Neumann algebra is a closed condition: T ∈ M = M′′ says that T commutes with every element of the commutant M′.

Limits stay in the closed sets

theorem Orthogonalization.MvN.mem_of_tendsto_ofCLM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} [l.NeBot] {T : κ → H →L[ℂ] H} {L : H →L[ℂ] H} (M : VonNeumannAlgebra H) (h : Filter.Tendsto (fun (k : κ) => ContinuousLinearMapWOT.ofCLM (T k)) l (nhds (ContinuousLinearMapWOT.ofCLM L))) (hT : ∀ (k : κ), T k ∈ M) : L ∈ M

A WOT-limit of elements of M lies in M.

theorem Orthogonalization.MvN.nonneg_of_tendsto_ofCLM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} [l.NeBot] {T : κ → H →L[ℂ] H} {L : H →L[ℂ] H} (h : Filter.Tendsto (fun (k : κ) => ContinuousLinearMapWOT.ofCLM (T k)) l (nhds (ContinuousLinearMapWOT.ofCLM L))) (hT : ∀ (k : κ), 0 ≤ T k) : 0 ≤ L

A WOT-limit of positive operators is positive.

theorem Orthogonalization.MvN.le_of_tendsto_ofCLM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} [l.NeBot] {T : κ → H →L[ℂ] H} {L a : H →L[ℂ] H} (h : Filter.Tendsto (fun (k : κ) => ContinuousLinearMapWOT.ofCLM (T k)) l (nhds (ContinuousLinearMapWOT.ofCLM L))) (hT : ∀ (k : κ), T k ≤ a) : L ≤ a

A WOT-limit of operators ≤ a is ≤ a.

theorem Orthogonalization.MvN.ge_of_tendsto_ofCLM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} [l.NeBot] {T : κ → H →L[ℂ] H} {L a : H →L[ℂ] H} (h : Filter.Tendsto (fun (k : κ) => ContinuousLinearMapWOT.ofCLM (T k)) l (nhds (ContinuousLinearMapWOT.ofCLM L))) (hT : ∀ (k : κ), a ≤ T k) : a ≤ L

A WOT-limit of operators ≥ a is ≥ a.

theorem Orthogonalization.MvN.isSelfAdjoint_of_tendsto_ofCLM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} [l.NeBot] {T : κ → H →L[ℂ] H} {L : H →L[ℂ] H} (h : Filter.Tendsto (fun (k : κ) => ContinuousLinearMapWOT.ofCLM (T k)) l (nhds (ContinuousLinearMapWOT.ofCLM L))) (hT : ∀ (k : κ), IsSelfAdjoint (T k)) : IsSelfAdjoint L

A WOT-limit of self-adjoint operators is self-adjoint.

theorem Orthogonalization.MvN.commute_of_tendsto_ofCLM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {κ : Type u_2} {l : Filter κ} [l.NeBot] {T : κ → H →L[ℂ] H} {L a : H →L[ℂ] H} (h : Filter.Tendsto (fun (k : κ) => ContinuousLinearMapWOT.ofCLM (T k)) l (nhds (ContinuousLinearMapWOT.ofCLM L))) (hT : ∀ (k : κ), Commute (T k) a) : Commute L a

A WOT-limit of operators commuting with a commutes with a.

theorem Orthogonalization.MvN.mul_eq_of_tendsto_ofCLM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {κ : Type u_2} {l : Filter κ} [l.NeBot] {T : κ → H →L[ℂ] H} {L a b : H →L[ℂ] H} (h : Filter.Tendsto (fun (k : κ) => ContinuousLinearMapWOT.ofCLM (T k)) l (nhds (ContinuousLinearMapWOT.ofCLM L))) (hT : ∀ (k : κ), a * T k * b = T k) : a * L * b = L

A WOT-limit of operators supported in (a, b) (a T b = T) is so supported.

theorem Orthogonalization.MvN.norm_le_of_tendsto_ofCLM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_2} {l : Filter κ} [l.NeBot] {T : κ → H →L[ℂ] H} {L : H →L[ℂ] H} {r : ℝ} (h : Filter.Tendsto (fun (k : κ) => ContinuousLinearMapWOT.ofCLM (T k)) l (nhds (ContinuousLinearMapWOT.ofCLM L))) (hT : ∀ (k : κ), ‖T k‖ ≤ r) : ‖L‖ ≤ r

The norm bound passes to WOT-limits (as a closed-set statement it is the compactness lemma's set; here it is the direct coefficient estimate).

Convexity

theorem Orthogonalization.MvN.convex_setOf_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Convex ℝ {T : H →WOT[ℂ] H | 0 ≤ T.toCLM}

The positive cone is convex.

theorem Orthogonalization.MvN.convex_setOf_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) : Convex ℝ {T : H →WOT[ℂ] H | T.toCLM ≤ a}

The order interval {T | T ≤ a} is convex.

theorem Orthogonalization.MvN.convex_setOf_ge {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) : Convex ℝ {T : H →WOT[ℂ] H | a ≤ T.toCLM}

The order interval {T | a ≤ T} is convex.

theorem Orthogonalization.MvN.convex_setOf_norm_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (r : ℝ) : Convex ℝ {T : H →WOT[ℂ] H | ‖T.toCLM‖ ≤ r}

The norm balls are convex.