OAI/Analysis/IrrationalRotation/Model/PositiveDiagonalModel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Invariant233.PositiveDiagonalModel.Fiber line 12
  2. abbrev OAI.Invariant233.PositiveDiagonalModel.Space line 13
  3. def OAI.Invariant233.PositiveDiagonalModel.e0 line 15
  4. def OAI.Invariant233.PositiveDiagonalModel.fiberShift line 17
  5. def OAI.Invariant233.PositiveDiagonalModel.fiberShiftUnit line 20
  6. def OAI.Invariant233.PositiveDiagonalModel.integerIterate line 26
  7. theorem OAI.Invariant233.PositiveDiagonalModel.measurable_integerIterate line 30
  8. def OAI.Invariant233.PositiveDiagonalModel.orbitArray line 36
  9. def OAI.Invariant233.PositiveDiagonalModel.realWeight line 39
  10. def OAI.Invariant233.PositiveDiagonalModel.realDiagonal line 46
  11. def OAI.Invariant233.PositiveDiagonalModel.realWeightedShift line 55
  12. def OAI.Invariant233.PositiveDiagonalModel.orbitWeightedShift line 61
  13. theorem OAI.Invariant233.PositiveDiagonalModel.exists_bounded_measurable_representative line 67
  14. def OAI.Invariant233.PositiveDiagonalModel.boundedRepresentative line 88
  15. theorem OAI.Invariant233.PositiveDiagonalModel.boundedRepresentative_measurable line 91
  16. theorem OAI.Invariant233.PositiveDiagonalModel.boundedRepresentative_ae_eq line 95
  17. theorem OAI.Invariant233.PositiveDiagonalModel.boundedRepresentative_bound line 99
  18. def OAI.Invariant233.PositiveDiagonalModel.lpOrbitWeightedShift line 103
  19. def OAI.Invariant233.PositiveDiagonalModel.diagonalState line 108