OAI/Analysis/KadisonSimilarity/FreeProduct/GeneratedCompression.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.factorsTraciallyGenerate_of_norm_generation line 25

   Source documentation

   Norm generation implies generation of the actual tracial Hilbert space.

   theorem factorsTraciallyGenerate_of_norm_generation
       (hgen : (factorAlgebra A D).topologicalClosure = ⊤) :
       G.FactorsTraciallyGenerate A D := by
   …

   Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra

2. theorem OAI.KadisonSimilarity.factorAlgebra_comap_generates line 53

   Source documentation

   Pulling the two factors into their closed generated algebra preserves their ordinary norm-generation property.

   theorem factorAlgebra_comap_generates (A D S : StarSubalgebra ℂ P)
       (hA : A ≤ S) (hD : D ≤ S) (hS : (factorAlgebra A D).topologicalClosure = S)
       [IsClosed (S : Set P)] :
       (factorAlgebra (A.comap S.subtype) (D.comap S.subtype)).topologicalClosure = ⊤ := by
   …

3. instance OAI.KadisonSimilarity.isClosed_comap_subtype line 81
4. theorem OAI.KadisonSimilarity.alternatingCenteredWord_subtype line 85
5. theorem OAI.KadisonSimilarity.scalarFree_subtype line 97
6. theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_narrow_compression_on_generated_algebra line 112

   Source documentation

   The narrow compression bound is proved in the cyclic Hilbert space of the generated algebra, then read in the ambient C-star norm.

   theorem norm_narrow_compression_on_generated_algebra
       (hA : A ≤ S) (hD : D ≤ S) (hS : (factorAlgebra A D).topologicalClosure = S)
       (published : RicardXuCompressionInput (G.baseGeometry S)
         (A.comap S.subtype) (D.comap S.subtype))
       (hτ : G.trace 1 = 1) (hfaithful : Function.Injective G.vector)
       (hfree : ScalarFree G.trace D A)
       (e : A) (he : IsStarProjection (e : P))
       (b : D) (hbself : star b = b) (hb0 : G.trace (b : P) = 0)
       {u : ℝ} (hu : 0 ≤ u) (hetrace : G.trace (e : P) = (u : ℂ))
       (hb₂ : (G.trace (star (b : P) * (b : P))).re ≤ u) (hbnorm : ‖(b : P)‖ ≤ 1) :
       ‖(e : P) * (b : P) * (e : P)‖ ≤ 3 * u := by
   …

   Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra, OAI.KadisonSimilarity.RicardXuCompressionInput, OAI.KadisonSimilarity.ScalarFree