OAI/Probability/BinarySweep/TensorBounds/SignedBlocks.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Signed.blockPerm_inv line 22
2. lemma OAI.BinaryCoordinateSweeps.Signed.signC_blocks line 32
3. def OAI.BinaryCoordinateSweeps.Signed.blockWords line 37
4. lemma OAI.BinaryCoordinateSweeps.Signed.blockWords_apply line 42
5. lemma OAI.BinaryCoordinateSweeps.Signed.blockWords_comp line 46
6. theorem OAI.BinaryCoordinateSweeps.Signed.actionMatrix_blocks line 52
7. def OAI.BinaryCoordinateSweeps.Signed.vacuumDensity line 90
8. lemma OAI.BinaryCoordinateSweeps.Signed.vacuumDensity_psd line 93
9. lemma OAI.BinaryCoordinateSweeps.Signed.vacuumDensity_trace line 98
10. lemma OAI.BinaryCoordinateSweeps.Signed.vacuumDensity_even line 102
11. abbrev OAI.BinaryCoordinateSweeps.Signed.LocalDensityIndex line 107
12. def OAI.BinaryCoordinateSweeps.Signed.localDensity line 110
13. lemma OAI.BinaryCoordinateSweeps.Signed.localDensity_psd line 113
14. lemma OAI.BinaryCoordinateSweeps.Signed.localDensity_trace line 120
15. lemma OAI.BinaryCoordinateSweeps.Signed.localDensity_even line 127
16. lemma OAI.BinaryCoordinateSweeps.Signed.localDensityIndex_card line 135
17. lemma OAI.BinaryCoordinateSweeps.Signed.localDensityIndex_nonempty line 148
18. lemma OAI.BinaryCoordinateSweeps.Signed.projection_complement_psd line 152
19. theorem OAI.BinaryCoordinateSweeps.Signed.local_type_density_domination line 163