SeparableTests.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Common separable reducing spaces for nearby test algebras

The countable dense generators of both algebras generate one separable ambient C*-algebra. Its finite-vector orbit supplies the common reducing space, including when the original Hilbert space is not separable.

theorem OAI.KadisonKastler.exists_separable_common_superalgebra line 21

theorem OAI.KadisonKastler.exists_common_separable_reducingSpace line 39

Source documentation

One closed separable subspace reduces both algebras and contains the finite prescribed vectors.

theorem exists_common_separable_reducingSpace
    (A B : StarSubalgebra ℂ (H →L[ℂ] H))
    (hA : IsSeparable (A : Set (H →L[ℂ] H)))
    (hB : IsSeparable (B : Set (H →L[ℂ] H))) (V : Finset H) :
    ∃ K : Submodule ℂ H, IsClosed (K : Set H) ∧ SeparableSpace K ∧
      (∀ v ∈ V, v ∈ K) ∧
      (∀ a : A, ∀ x ∈ K, (a : H →L[ℂ] H) x ∈ K) ∧
      (∀ b : B, ∀ x ∈ K, (b : H →L[ℂ] H) x ∈ K) := by
…

theorem OAI.KadisonKastler.exists_near_separable_tests line 55

Source documentation

The algebra and reducing-space portions of the separable tests lemma.

theorem exists_near_separable_tests (M N : VonNeumannAlgebra H)
    (E F : Finset (H →L[ℂ] H)) (V : Finset H)
    (hE : ∀ x ∈ E, x ∈ M) (hF : ∀ x ∈ F, x ∈ N)
    {g : ℝ} (hg : kkDistance M N < g) :
    ∃ (A B : StarSubalgebra ℂ (H →L[ℂ] H)) (K : Submodule ℂ H),
      IsClosed (A : Set (H →L[ℂ] H)) ∧ IsClosed (B : Set (H →L[ℂ] H)) ∧
      IsSeparable (A : Set (H →L[ℂ] H)) ∧ IsSeparable (B : Set (H →L[ℂ] H)) ∧
      A ≤ M.toStarSubalgebra ∧ B ≤ N.toStarSubalgebra ∧
      (∀ x ∈ E, x ∈ A) ∧ (∀ x ∈ F, x ∈ B) ∧
      Metric.hausdorffDist (starAlgebraBall A) (starAlgebraBall B) < g ∧
      IsClosed (K : Set H) ∧ SeparableSpace K ∧ (∀ v ∈ V, v ∈ K) ∧
      (∀ a : A, ∀ x ∈ K, (a : H →L[ℂ] H) x ∈ K) ∧
…

Mentions: OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.starAlgebraBall