OAI/Analysis/IrrationalRotation/Rotation/WeightedShiftPowers.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.WeightedShift.reindex_apply line 10
  2. theorem OAI.Invariant233.WeightedShift.shift_apply line 13
  3. theorem OAI.Invariant233.WeightedShift.diagonal_apply line 16
  4. theorem OAI.Invariant233.WeightedShift.operator_apply line 19
  5. theorem OAI.Invariant233.WeightedShift.operator_pow_apply_add line 22
  6. theorem OAI.Invariant233.WeightedShift.operator_pow_apply line 33
  7. theorem OAI.Invariant233.WeightedShift.norm_operator_pow_le line 38
  8. theorem OAI.Invariant233.WeightedShift.norm_product_le_norm_operator_pow line 53
  9. theorem OAI.Invariant233.WeightedShift.orbitProduct_apply line 68
  10. theorem OAI.Invariant233.WeightedShift.operator_pow_eq_shift_diagonal line 71
  11. theorem OAI.Invariant233.WeightedShift.norm_operator_pow line 78
  12. theorem OAI.Invariant233.WeightedShift.norm_operator line 88
  13. theorem OAI.Invariant233.WeightedShift.operator_eq_zero_iff line 92