OAI/Analysis/IrrationalRotation/Rotation/FieldWeightedShiftPowers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.WeightedShift.fieldOperator_ae line 17
2. theorem OAI.Invariant233.WeightedShift.fieldOperator_pow_ae line 26
3. theorem OAI.Invariant233.WeightedShift.norm_fieldOperator_pow_le line 36
4. theorem OAI.Invariant233.WeightedShift.fieldOperator_norm_quasinilpotent line 48
5. theorem OAI.Invariant233.WeightedShift.fieldOperator_norm_quasinilpotent_of_prefix_bounds line 59
6. theorem OAI.Invariant233.WeightedShift.fieldOperator_eq_zero_iff line 73
7. theorem OAI.Invariant233.WeightedShift.fieldOperator_ne_zero_of_coordinate line 102