OAI/Probability/BinarySweep/MatrixBounds/SymmetricDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Density.psd_trace_domination line 13
2. lemma OAI.BinaryCoordinateSweeps.Density.rankOne_conjugate line 41
3. lemma OAI.BinaryCoordinateSweeps.Density.rankOne_projection_bound line 46
4. lemma OAI.BinaryCoordinateSweeps.Density.symmetricProjector_identity line 58
5. lemma OAI.BinaryCoordinateSweeps.Density.symmetricProjector_idempotent line 83
6. lemma OAI.BinaryCoordinateSweeps.Density.symmetric_rankOne_bound line 93
7. theorem OAI.BinaryCoordinateSweeps.Density.symmetric_vector_postselection line 99