OAI/Probability/BinarySweep/MatrixBounds/Whitening.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Irrep.symmetric_projection_commutes line 21
2. lemma OAI.BinaryCoordinateSweeps.Irrep.isotypic_norm_cap line 31
3. theorem OAI.BinaryCoordinateSweeps.Irrep.whitening_norm line 50
4. theorem OAI.BinaryCoordinateSweeps.Irrep.whitening_positive line 67
5. lemma OAI.BinaryCoordinateSweeps.Density.trace_product_nonneg line 104
6. lemma OAI.BinaryCoordinateSweeps.Density.trace_product_mono line 110
7. lemma OAI.BinaryCoordinateSweeps.Density.trace_product_re_nonneg line 116
8. lemma OAI.BinaryCoordinateSweeps.Density.trace_product_re_mono line 120
9. lemma OAI.BinaryCoordinateSweeps.Density.tensor_product_trace_re line 125
10. def OAI.BinaryCoordinateSweeps.Density.parityProjection line 146
11. lemma OAI.BinaryCoordinateSweeps.Density.commutes_parity_iff line 149
12. lemma OAI.BinaryCoordinateSweeps.Density.sqrt_commutes line 164
13. theorem OAI.BinaryCoordinateSweeps.Density.exists_even_whitening line 169