OAI/Probability/BinarySweep/GridBounds/GroupedMoments.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Signed.action_unitary line 24
2. lemma OAI.BinaryCoordinateSweeps.Signed.matrixMoment_signedConj line 28
3. def OAI.BinaryCoordinateSweeps.Signed.groupedAverage line 33
4. lemma OAI.BinaryCoordinateSweeps.Signed.groupedAverage_law line 37
5. theorem OAI.BinaryCoordinateSweeps.Signed.grouped_projected_moment_le line 48
6. lemma OAI.BinaryCoordinateSweeps.Signed.blockProjection_commutes_average line 59
7. lemma OAI.BinaryCoordinateSweeps.Signed.groupedProjection_commutes_average line 70
8. lemma OAI.BinaryCoordinateSweeps.Signed.groupedProjection_norm_le line 80
9. lemma OAI.BinaryCoordinateSweeps.Signed.blockActive_projection_sum line 87
10. lemma OAI.BinaryCoordinateSweeps.Signed.groupedActive_projection_sum line 101
11. lemma OAI.BinaryCoordinateSweeps.Signed.blockActive_card line 108
12. theorem OAI.BinaryCoordinateSweeps.Density.whitened_board_budget line 127
13. lemma OAI.BinaryCoordinateSweeps.Density.matrix_norm_sq_le_trace line 159
14. lemma OAI.BinaryCoordinateSweeps.Density.projection_overlap_norm_trace line 164
15. lemma OAI.BinaryCoordinateSweeps.Density.commuting_projection_product_psd line 180
16. lemma OAI.BinaryCoordinateSweeps.Density.compress_whitening_cap line 188