OAI/Analysis/BoundedHochschild/MatrixRightAveraging.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedHochschild.KadisonRingrose.finiteRowEstimate_of_columns line 15
2. lemma OAI.BoundedHochschild.KadisonRingrose.matrixAmplification_rowBound line 38
3. lemma OAI.BoundedHochschild.KadisonRingrose.cstar_finite_sum_apply line 52
4. lemma OAI.BoundedHochschild.KadisonRingrose.matrix_mul_scalar_apply line 59
5. lemma OAI.BoundedHochschild.KadisonRingrose.matrixAmplification_rightAverage line 64
6. lemma OAI.BoundedHochschild.KadisonRingrose.matrixScalar_normalized line 73
7. theorem OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage_completelyBounded line 80

   Source documentation

   Finite normalized right averages preserve the original complete bound, not only its level-one operator norm consequence.

   theorem finiteRightAverage_completelyBounded {n : ℕ}
       (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] N) (hno : NoFiniteCentralSummand N)
       (m : Fin (n + 1) → N) (hm : ∑ i, m i * star (m i) = 1)
       (T : N →L[ℂ] N) {C : ℝ} (hT : CompletelyBoundedEstimate T C) :
       CompletelyBoundedEstimate (finiteRightAverage m T) C := by
   …

   Mentions: OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand, OAI.BoundedHochschild.KadisonRingrose.CompletelyBoundedEstimate, OAI.BoundedHochschild.KadisonRingrose.finiteRightAverage