StrongCommutantTests.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Countable strong-operator tests for commutation

On a uniformly bounded set of operators, convergence on a countable dense set of vectors implies convergence on every vector. A countable dense set of coordinate sequences therefore supplies all commutant tests.

theorem OAI.KadisonKastler.tendsto_apply_of_dense_contractions line 28

Source documentation

Uniform contraction bounds extend pointwise convergence from a dense sequence to every vector.

theorem tendsto_apply_of_dense_contractions (v : ℕ → H) (hv : DenseRange v)
    (A : ℕ → H →L[ℂ] H) (B : H →L[ℂ] H)
    (hA : ∀ n, ‖A n‖ ≤ 1) (hB : ‖B‖ ≤ 1)
    (h : ∀ j, Tendsto (fun n => A n (v j)) atTop (𝓝 (B (v j)))) (x : H) :
    Tendsto (fun n => A n x) atTop (𝓝 (B x)) := by
…

theorem OAI.KadisonKastler.exists_countable_strong_dense_contractions line 53

Source documentation

Every contraction-valued set on a separable space has a countable subset that approximates each of its elements strongly by a sequence.

theorem exists_countable_strong_dense_contractions [SeparableSpace H]
    (S : Set (H →L[ℂ] H)) (hS : ∀ T ∈ S, ‖T‖ ≤ 1) :
    ∃ E : Set (H →L[ℂ] H), E.Countable ∧ E ⊆ S ∧
      ∀ T ∈ S, ∃ A : ℕ → H →L[ℂ] H,
        (∀ n, A n ∈ E) ∧ ∀ ξ, Tendsto (fun n => A n ξ) atTop (𝓝 (T ξ)) := by
…

theorem OAI.KadisonKastler.commute_of_strong_tendsto line 85

Source documentation

Commutation with a fixed bounded operator is closed under strong convergence.

theorem commute_of_strong_tendsto (A T : H →L[ℂ] H) (B : ℕ → H →L[ℂ] H)
    (hB : ∀ ξ, Tendsto (fun n => B n ξ) atTop (𝓝 (T ξ)))
    (hcomm : ∀ n, Commute A (B n)) : Commute A T := by
…

theorem OAI.KadisonKastler.exists_countable_commutant_tests line 101

Source documentation

Countably many operators determine the entire commutant of an arbitrary contraction-valued set.

theorem exists_countable_commutant_tests [SeparableSpace H]
    (S : Set (H →L[ℂ] H)) (hS : ∀ T ∈ S, ‖T‖ ≤ 1) :
    ∃ E : Set (H →L[ℂ] H), E.Countable ∧ E ⊆ S ∧
      ∀ A : H →L[ℂ] H, (∀ T ∈ E, Commute A T) ↔ ∀ T ∈ S, Commute A T := by
…

theorem OAI.KadisonKastler.exists_countable_unitBall_commutant_tests line 113

Source documentation

The unit ball of any operator set admits countably many commutant tests.

theorem exists_countable_unitBall_commutant_tests [SeparableSpace H]
    (S : Set (H →L[ℂ] H)) :
    ∃ E : Set (H →L[ℂ] H), E.Countable ∧ E ⊆ {T ∈ S | ‖T‖ ≤ 1} ∧
      ∀ A : H →L[ℂ] H, (∀ T ∈ E, Commute A T) ↔ ∀ T ∈ S, ‖T‖ ≤ 1 → Commute A T := by
…