OAI/Analysis/KadisonKastler/IndependentUnitaryVariance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Variance bounds for independently separated unitary transport blocks.

  1. theorem OAI.KadisonKastler.countableUnitaryL2_forward_inverse line 20
  2. theorem OAI.KadisonKastler.independent_unitary_inverse_independent line 30
  3. theorem OAI.KadisonKastler.independent_unitary_variance_left line 42
  4. theorem OAI.KadisonKastler.independent_unitary_variance_right line 55