OAI/Probability/BinarySweep/TensorBounds/BlockTypes.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Signed.submatrix_sum_eq line 23
2. def OAI.BinaryCoordinateSweeps.Signed.blockProjection line 29
3. lemma OAI.BinaryCoordinateSweeps.Signed.blockProjection_psd line 35
4. lemma OAI.BinaryCoordinateSweeps.Signed.blockProjection_idempotent line 41
5. lemma OAI.BinaryCoordinateSweeps.Signed.block_tensor_density line 53
6. lemma OAI.BinaryCoordinateSweeps.Signed.block_density_domination line 67
7. lemma OAI.BinaryCoordinateSweeps.Signed.blockProjection_central line 84
8. lemma OAI.BinaryCoordinateSweeps.piTensorMatrices_pow line 131
9. lemma OAI.BinaryCoordinateSweeps.gram_trace_real line 139
10. lemma OAI.BinaryCoordinateSweeps.tensor_matrixMoment line 146
11. lemma OAI.BinaryCoordinateSweeps.matrixMoment_reindex line 159
12. def OAI.BinaryCoordinateSweeps.Signed.blockAverage line 178
13. lemma OAI.BinaryCoordinateSweeps.Signed.blockAverage_tensor line 182
14. lemma OAI.BinaryCoordinateSweeps.Signed.block_projected_moment line 194
15. theorem OAI.BinaryCoordinateSweeps.Signed.block_projected_moment_le line 207