OAI/Analysis/IrrationalRotation/Operators/TowerTraceBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.TowerTraceBounds.diagonal_isStarProjection line 22
2. theorem OAI.Invariant233.TowerTraceBounds.selectedFloor_isStarProjection line 31
3. theorem OAI.Invariant233.TowerTraceBounds.diagonal_trace_eq line 50
4. theorem OAI.Invariant233.TowerTraceBounds.vectorTrace_sum_re line 58
5. theorem OAI.Invariant233.TowerTraceBounds.height_weighted_trace_eq_one line 63
6. theorem OAI.Invariant233.TowerTraceBounds.selectedFloor_trace_le_inv_height line 78
7. theorem OAI.Invariant233.TowerTraceBounds.norm_sub_apply_sq_le_four_div_height line 102