OAI/Analysis/TracialSplitting/BistochasticTests.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CurrentMain.BistochasticTest line 16
2. def OAI.CurrentMain.BistochasticTest.map line 26
3. def OAI.CurrentMain.BistochasticTest.single line 32
4. def OAI.CurrentMain.BistochasticTest.energy line 40
5. lemma OAI.CurrentMain.BistochasticTest.energy_nonneg line 44
6. lemma OAI.CurrentMain.BistochasticTest.sum_mul_energy line 47
7. lemma OAI.CurrentMain.BistochasticTest.sum_energy_mul line 53
8. lemma OAI.CurrentMain.BistochasticTest.square_add_le line 65
9. lemma OAI.CurrentMain.BistochasticTest.energy_le line 73
10. lemma OAI.CurrentMain.BistochasticTest.energy_perturb line 82
11. lemma OAI.CurrentMain.BistochasticTest.overlap_le line 92
12. lemma OAI.CurrentMain.BistochasticTest.unitary_tests line 110
13. lemma OAI.CurrentMain.BistochasticTest.relative_unitary_tests line 154