WeakOperatorLimits.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The norm estimates and commutation identities used in symmetrization persist under weak-operator limits.

theorem OAI.KadisonSimilarity.norm_le_of_matrix_coefficients line 21
Source documentation
A homogeneous bound on all Hilbert matrix coefficients bounds the operator norm with the same constant.
```
theorem norm_le_of_matrix_coefficients (T : H →L[ℂ] K) {c : ℝ} (hc : 0 ≤ c)
    (h : ∀ x y, ‖inner ℂ y (T x)‖ ≤ c * ‖y‖ * ‖x‖) : ‖T‖ ≤ c := by
…
```

theorem OAI.KadisonSimilarity.norm_le_of_weakOperator_tendsto line 37

Source documentation

Bounded closed balls are weak-operator closed, in the sequential or general-filter form needed by the averaging argument.

theorem norm_le_of_weakOperator_tendsto {l : Filter ι} [l.NeBot]
    (T : ι → H →L[ℂ] K) (S : H →L[ℂ] K)
    (ht : Tendsto (fun i => ofCLM (T i)) l (𝓝 (ofCLM S)))
    {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ᶠ i in l, ‖T i‖ ≤ c) : ‖S‖ ≤ c := by
…

theorem OAI.KadisonSimilarity.weakOperator_tendsto_commutator line 57

Source documentation

Commutation against a fixed bounded operator is weak-operator continuous.

theorem weakOperator_tendsto_commutator {l : Filter ι}
    (T : ι → H →L[ℂ] H) (S A : H →L[ℂ] H)
    (ht : Tendsto (fun i => ofCLM (T i)) l (𝓝 (ofCLM S))) :
    Tendsto (fun i => ofCLM (commutator (T i) A)) l
      (𝓝 (ofCLM (commutator S A))) := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.norm_commutator_le_of_weakOperator_tendsto line 67

Source documentation

A fixed commutator estimate survives weak-operator convergence.

theorem norm_commutator_le_of_weakOperator_tendsto {l : Filter ι} [l.NeBot]
    (T : ι → H →L[ℂ] H) (S A : H →L[ℂ] H)
    (ht : Tendsto (fun i => ofCLM (T i)) l (𝓝 (ofCLM S)))
    {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ᶠ i in l, ‖commutator (T i) A‖ ≤ c) :
    ‖commutator S A‖ ≤ c :=
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.commutator_eq_zero_of_weakOperator_tendsto line 75

Source documentation

In particular exact commutation survives these limits.

theorem commutator_eq_zero_of_weakOperator_tendsto {l : Filter ι} [l.NeBot]
    (T : ι → H →L[ℂ] H) (S A : H →L[ℂ] H)
    (ht : Tendsto (fun i => ofCLM (T i)) l (𝓝 (ofCLM S)))
    (hcomm : ∀ᶠ i in l, commutator (T i) A = 0) : commutator S A = 0 := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.scalarCommutatorNorm_le_of_weakOperator_tendsto line 87

Source documentation

The entire scalar commutator seminorm is lower semicontinuous for the weak-operator topology.

theorem scalarCommutatorNorm_le_of_weakOperator_tendsto {l : Filter ι} [l.NeBot]
    (P : VonNeumannAlgebra H) (T : ι → H →L[ℂ] H) (S : H →L[ℂ] H)
    (ht : Tendsto (fun i => ofCLM (T i)) l (𝓝 (ofCLM S)))
    {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ᶠ i in l, scalarCommutatorNorm P (T i) ≤ c) :
    scalarCommutatorNorm P S ≤ c := by
…

Mentions: OAI.KadisonSimilarity.scalarCommutatorNorm