OAI/Analysis/JiangSu/Comparison/ComplexScalar.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectComparison.finite_scalar_unbounded line 14
2. theorem OAI.DirectComparison.finite_complex_scalar line 48
3. example OAI.DirectPacking.(example at line 85) line 85
4. def OAI.DirectComparison.ProjectionPacking.toPartition line 95
5. theorem OAI.DirectPacking.weighted_family_of_kraus_average line 121