OAI/Probability/BinarySweep/MatrixBounds/SpectralMoment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.TraceHolder.matrixMoment line 12
2. lemma OAI.BinaryCoordinateSweeps.TraceHolder.diagReal_pow line 14
3. lemma OAI.BinaryCoordinateSweeps.TraceHolder.trace_unitary_conj line 18
4. lemma OAI.BinaryCoordinateSweeps.TraceHolder.unitary_conj_pow line 22
5. lemma OAI.BinaryCoordinateSweeps.TraceHolder.matrixMoment_of_svd line 29
6. lemma OAI.BinaryCoordinateSweeps.TraceHolder.matrixMoment_nonneg line 36
7. lemma OAI.BinaryCoordinateSweeps.TraceHolder.matrixMoment_eq_zero_iff line 41
8. lemma OAI.BinaryCoordinateSweeps.TraceHolder.unitary_norm_le_one line 56
9. lemma OAI.BinaryCoordinateSweeps.TraceHolder.diagPower_real line 66
10. lemma OAI.BinaryCoordinateSweeps.TraceHolder.density_normalization line 80