OAI/Probability/BinarySweep/MatrixBounds/TraceConvex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.TraceHolder.trace_mul_diagonal_le line 16
2. lemma OAI.BinaryCoordinateSweeps.TraceHolder.trace_prod_density_le line 25
3. def OAI.BinaryCoordinateSweeps.TraceHolder.Admissible line 39
4. def OAI.BinaryCoordinateSweeps.TraceHolder.exponentSet line 43
5. lemma OAI.BinaryCoordinateSweeps.TraceHolder.word_absorb_phase line 46
6. lemma OAI.BinaryCoordinateSweeps.TraceHolder.admissible_complex line 61
7. lemma OAI.BinaryCoordinateSweeps.TraceHolder.vertex_mem_exponentSet line 72
8. lemma OAI.BinaryCoordinateSweeps.TraceHolder.convex_exponentSet line 98
9. theorem OAI.BinaryCoordinateSweeps.TraceHolder.trace_diagonal_simplex line 147
10. lemma OAI.BinaryCoordinateSweeps.TraceHolder.prod_sandwich_succ line 174
11. lemma OAI.BinaryCoordinateSweeps.TraceHolder.trace_prod_sandwich line 188
12. theorem OAI.BinaryCoordinateSweeps.TraceHolder.trace_diagonal_sandwich line 198