SeparableContractionTests.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Countable weak-operator contraction tests

On a separable Hilbert space, the weak-operator unit ball embeds in a countable product of copies of ℂ, by its coefficients on a dense sequence of vectors. Compactness makes this an embedding. Thus each von Neumann algebra has a countable weakly dense family of contractions.

abbrev OAI.KadisonSimilarity.WeakOperatorUnitBall line 26
Source documentation
The operator unit ball, with the topology induced by the weak-operator topology.
```
abbrev WeakOperatorUnitBall (H : Type*) [NormedAddCommGroup H]
    [InnerProductSpace ℂ H] :=
…
```
theorem OAI.KadisonSimilarity.secondCountable_weakOperatorUnitBall line 32
Source documentation
Countably many matrix coefficients determine the topology on the weak operator unit ball of a separable Hilbert space.
```
theorem secondCountable_weakOperatorUnitBall :
    SecondCountableTopology (WeakOperatorUnitBall H) := by
…
```
Mentions: OAI.KadisonSimilarity.WeakOperatorUnitBall

theorem OAI.KadisonSimilarity.exists_separable_contraction_tests line 60

Source documentation

A concrete von Neumann algebra on a separable Hilbert space has a countable weak-operator dense family in its closed unit ball.

theorem exists_separable_contraction_tests (P : VonNeumannAlgebra H) :
    ∃ test : ℕ → P.toStarSubalgebra,
      (∀ n, ‖test n‖ ≤ 1) ∧
      ∀ T : H →L[ℂ] H, T ∈ P → ‖T‖ ≤ 1 →
        ofCLM T ∈ closure (Set.range fun n => ofCLM (test n : H →L[ℂ] H)) := by
…

theorem OAI.KadisonSimilarity.exists_countable_scalar_commutator_tests line 89

Source documentation

It suffices to verify the scalar commutator bound on some countable family of contractions, constructed from separability.

theorem exists_countable_scalar_commutator_tests (P : VonNeumannAlgebra H) :
    ∃ test : ℕ → P.toStarSubalgebra,
      (∀ n, ‖test n‖ ≤ 1) ∧
      ∀ (Y : H →L[ℂ] H) (c : ℝ), 0 ≤ c →
        (∀ n, ‖commutator Y (test n)‖ ≤ c) → scalarCommutatorNorm P Y ≤ c := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.scalarCommutatorNorm