OAI/Probability/SignedSweeps/EvenDensity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SignedSweeps.EvenColorDensity line 12
2. def OAI.SignedSweeps.EvenColorDensity.matrix line 29
3. def OAI.SignedSweeps.EvenColorDensity.tensor line 32
4. lemma OAI.SignedSweeps.EvenColorDensity.tensor_commute line 36
5. lemma OAI.SignedSweeps.EvenColorDensity.tensor_entropy_upper line 41
6. def OAI.SignedSweeps.EvenColorDensity.conjugateDiagonal line 47
7. lemma OAI.SignedSweeps.pair_twirl_mem_density_hull line 69
8. theorem OAI.SignedSweeps.exists_even_density_domination line 100