OAI/Analysis/IrrationalRotation/Rotation/WeightedShiftDiagonal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.WeightedShift.diagonal_isSelfAdjoint_of_real line 13
2. theorem OAI.Invariant233.WeightedShift.diagonal_isPositive_of_nonneg line 24
3. theorem OAI.Invariant233.WeightedShift.diagonal_nonneg_of_real_coordinates line 43
4. theorem OAI.Invariant233.WeightedShift.diagonal_ker_eq_bot line 49
5. theorem OAI.Invariant233.WeightedShift.operator_ker_eq_bot line 52
6. theorem OAI.Invariant233.WeightedShift.diagonal_denseRange_of_real line 55
7. theorem OAI.Invariant233.WeightedShift.diagonal_single line 66
8. theorem OAI.Invariant233.WeightedShift.norm_coordinate_vector line 74
9. theorem OAI.Invariant233.WeightedShift.ae_strict_diagonal_of_real_weightedShift line 78