OAI/Analysis/KadisonKastler/TupleMatrices.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.fiberReplication line 22
2. theorem OAI.KadisonKastler.norm_fiberReplication_le line 25
3. theorem OAI.KadisonKastler.fiberReplication_mul line 49
4. theorem OAI.KadisonKastler.mul_fiberReplication_star line 55
5. theorem OAI.KadisonKastler.norm_replicatedMatrix_le line 63

   Source documentation

   Replication of each row and column costs only the square roots of the numbers of orderings, rather than their product.

   theorem norm_replicatedMatrix_le (f : I → R) (g : J → S)
       (m n : ℕ) (hf : ∀ r, #{i | f i = r} ≤ m) (hg : ∀ s, #{j | g j = s} ≤ n)
       (T : CStarMatrix R S (H →L[ℂ] H)) :
       ‖CStarMatrix.ofMatrix (fun i j => T (f i) (g j))‖ ≤
         Real.sqrt (m : ℝ) * ‖T‖ * Real.sqrt (n : ℝ) := by
   …