OAI/Analysis/KadisonKastler/SeparableAlgebraPair.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.cstarHull line 22
2. def OAI.KadisonKastler.starAlgebraBall line 25
3. theorem OAI.KadisonKastler.zero_mem_starAlgebraBall line 28
4. theorem OAI.KadisonKastler.cstarHull_mono line 31
5. theorem OAI.KadisonKastler.subset_cstarHull line 34
6. theorem OAI.KadisonKastler.cstarHull_le line 37
7. theorem OAI.KadisonKastler.isSeparable_cstarHull line 41
8. theorem OAI.KadisonKastler.infDist_le_of_mem_closure line 47

   Source documentation

   The bound on distance to a fixed set passes through norm closure.

   theorem infDist_le_of_mem_closure {s t : Set (H →L[ℂ] H)} {r : ℝ}
       (h : ∀ x ∈ s, Metric.infDist x t ≤ r) {x : H →L[ℂ] H}
       (hx : x ∈ closure s) : Metric.infDist x t ≤ r :=
   …

9. theorem OAI.KadisonKastler.exists_separable_seed_extension line 53

   Source documentation

   Add a countable family of near approximants to the second seed set.

   theorem exists_separable_seed_extension (M N : VonNeumannAlgebra H)
       {s t : Set (H →L[ℂ] H)} (hs : s.Countable) (ht : t.Countable)
       (hsM : s ⊆ M) (htN : t ⊆ N) {r : ℝ} (hr : kkDistance M N < r) :
       ∃ t' : Set (H →L[ℂ] H), t'.Countable ∧ t ⊆ t' ∧ t' ⊆ N ∧
         ∀ x ∈ starAlgebraBall (cstarHull s),
           Metric.infDist x (starAlgebraBall (cstarHull t')) ≤ r := by
   …

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

10. structure OAI.KadisonKastler.SeparableSeeds line 84
11. def OAI.KadisonKastler.SeparableSeeds.Extends line 92
12. theorem OAI.KadisonKastler.SeparableSeeds.exists_extension line 100
13. def OAI.KadisonKastler.SeparableSeeds.next line 110
14. theorem OAI.KadisonKastler.SeparableSeeds.next_spec line 114
15. def OAI.KadisonKastler.SeparableSeeds.stages line 118
16. theorem OAI.KadisonKastler.SeparableSeeds.stages_left_mono line 123
17. theorem OAI.KadisonKastler.SeparableSeeds.stages_right_mono line 128
18. def OAI.KadisonKastler.increasingCstarClosure line 133
19. theorem OAI.KadisonKastler.le_increasingCstarClosure line 136
20. theorem OAI.KadisonKastler.isSeparable_increasingCstarClosure line 140
21. theorem OAI.KadisonKastler.infDist_increasingCstarClosure_ball line 148
22. theorem OAI.KadisonKastler.exists_near_separable_algebra_pair_countable line 167

    Source documentation

    The alternating countable construction produces nearby closed separable test algebras containing any prescribed finite operator tests.

    theorem exists_near_separable_algebra_pair_countable (M N : VonNeumannAlgebra H)
        (E F : Set (H →L[ℂ] H)) (hEc : E.Countable) (hFc : F.Countable)
        (hE : ∀ x ∈ E, x ∈ M) (hF : ∀ x ∈ F, x ∈ N)
        {g : ℝ} (hg : kkDistance M N < g) :
        ∃ A B : StarSubalgebra ℂ (H →L[ℂ] 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 := by
    …

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

23. theorem OAI.KadisonKastler.exists_near_separable_algebra_pair line 221

    Source documentation

    Finite prescribed tests are a special case of the countable construction.

    theorem exists_near_separable_algebra_pair (M N : VonNeumannAlgebra H)
        (E F : Finset (H →L[ℂ] H)) (hE : ∀ x ∈ E, x ∈ M) (hF : ∀ x ∈ F, x ∈ N)
        {g : ℝ} (hg : kkDistance M N < g) :
        ∃ A B : StarSubalgebra ℂ (H →L[ℂ] 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 :=
    …

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