OAI/Analysis/BoundedHochschild/WeakCompletelyBoundedClosure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedHochschild.KadisonRingrose.rightAverageOrbit_completelyBounded line 21
2. def OAI.BoundedHochschild.KadisonRingrose.weakMatrixReconstruction line 39

   Source documentation

   Reconstruct a matrix of weak-dual values in the original algebra.

   def weakMatrixReconstruction (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) {n : ℕ}
       (c : Fin n → PartialIso M) (A : CStarMatrix (Fin n) (Fin n) M)
       (F : M → WeakDual ℂ X) : WeakDual ℂ X :=
   …

3. lemma OAI.BoundedHochschild.KadisonRingrose.weakMatrixReconstruction_image line 46
4. lemma OAI.BoundedHochschild.KadisonRingrose.weakMatrixReconstruction_continuous line 55
5. lemma OAI.BoundedHochschild.KadisonRingrose.columnReconstruction_norm line 68
6. theorem OAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit_completelyBounded line 78

   Source documentation

   Every realized member of the weak-star closed averaging orbit has the same complete bound as the original map.

   theorem weakRightAverageOrbit_completelyBounded (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
       (hno : NoFiniteCentralSummand M) (T : M →L[ℂ] M) {C : ℝ}
       (hT : CompletelyBoundedEstimate T C) (S : M →L[ℂ] M)
       (hS : weakOperatorImage e S ∈ weakRightAverageOrbit e T) :
       CompletelyBoundedEstimate S C := by
   …

   Mentions: OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand, OAI.BoundedHochschild.KadisonRingrose.CompletelyBoundedEstimate, OAI.BoundedHochschild.KadisonRingrose.weakOperatorImage, OAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit