PublishedKaplansky.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The published bounded-density input

Irving Kaplansky, A theorem on rings of operators, Pacific Journal of Mathematics 1 (1951), 227--232, Theorem 1, p. 227: https://msp.org/pjm/1951/1-2/pjm-v1-n2-p06-s.pdf

The paper's terminology "unit sphere" is the closed unit ball, as the norm bounds in the proof on pp. 228 and 230--231 explicitly show. The input below is its finite-strong-neighborhood specialization to a unital star algebra and its bicommutant. The already proved double commutant theorem supplies the required strong density. No statement comparing two algebras or their Kadison--Kastler distances is assumed.

def OAI.KadisonKastler.PublishedKaplanskyDensity line 31
Source documentation
Kaplansky's published unit-ball density theorem, retaining only finite vector tests needed in the nonseparable reduction.
```
def PublishedKaplanskyDensity : Prop :=
…
```
def OAI.KadisonKastler.generatedVonNeumannAlgebra line 41
Source documentation
The actual von Neumann algebra generated by a unital star algebra.
```
def generatedVonNeumannAlgebra (A : StarSubalgebra ℂ (H →L[ℂ] H)) :
    VonNeumannAlgebra H where
…
```
theorem OAI.KadisonKastler.generatedVonNeumannAlgebra_coe line 51
theorem OAI.KadisonKastler.subset_generatedVonNeumannAlgebra line 60
theorem OAI.KadisonKastler.generatedVonNeumannAlgebra_le_of_le line 67
Source documentation
A concrete von Neumann algebra contains the generated algebra of each of its star subalgebras.
```
theorem generatedVonNeumannAlgebra_le_of_le
    (A : StarSubalgebra ℂ (H →L[ℂ] H)) (B : VonNeumannAlgebra H)
    (hAB : A ≤ B.toStarSubalgebra) : generatedVonNeumannAlgebra A ≤ B := by
…
```
Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra

theorem OAI.KadisonKastler.PublishedKaplanskyDensity.exists_strong_contraction_net line 79

Source documentation

Turn the finite-neighborhood published statement into an actual strongly convergent net of contractions.

theorem PublishedKaplanskyDensity.exists_strong_contraction_net
    (hK : PublishedKaplanskyDensity.{u})
    (A : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
    (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
    (hn : ‖T‖ ≤ 1) :
    ∃ a : Finset H × ℕ → A, (∀ d, ‖a d‖ ≤ 1) ∧
      ∀ x : H, Tendsto (fun d => (a d : H →L[ℂ] H) x) atTop (𝓝 (T x)) := by
…

theorem OAI.KadisonKastler.PublishedKaplanskyDensity.exists_weak_contraction_net line 103

Source documentation

The same actual net converges on every matrix coefficient.

theorem PublishedKaplanskyDensity.exists_weak_contraction_net
    (hK : PublishedKaplanskyDensity.{u})
    (A : StarSubalgebra ℂ (H →L[ℂ] H)) (T : H →L[ℂ] H)
    (hT : T ∈ Set.centralizer (Set.centralizer (A : Set (H →L[ℂ] H))))
    (hn : ‖T‖ ≤ 1) :
    ∃ a : Finset H × ℕ → A, (∀ d, ‖a d‖ ≤ 1) ∧
      ∀ x y : H, Tendsto (fun d => inner ℂ y ((a d : H →L[ℂ] H) x))
        atTop (𝓝 (inner ℂ y (T x))) := by
…

theorem OAI.KadisonKastler.PublishedKaplanskyDensity.weakUnitBallDense line 117
Source documentation
The contractive elements of the original algebra give a concrete weakly dense test family in its generated von Neumann algebra.
```
theorem PublishedKaplanskyDensity.weakUnitBallDense
    (hK : PublishedKaplanskyDensity.{u})
    (A : StarSubalgebra ℂ (H →L[ℂ] H)) :
    WeakUnitBallDense (fun a : {a : A // ‖a‖ ≤ 1} => (a.val : H →L[ℂ] H))
      (generatedVonNeumannAlgebra A) := by
…
```
Mentions: OAI.KadisonKastler.WeakUnitBallDense, OAI.KadisonKastler.generatedVonNeumannAlgebra