OAI/Analysis/IrrationalRotation/Rotation/RotationTowerCyclicApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.Rotation.towerMatrixEntries_diagonal_eq_setProjection line 18
  2. theorem OAI.Invariant233.Rotation.sum_towerMatrixEntries_diagonal_eq_one line 27
  3. def OAI.Invariant233.Rotation.towerCyclicOperator line 48
  4. def OAI.Invariant233.Rotation.towerTopProjection line 52
  5. theorem OAI.Invariant233.Rotation.towerCyclicOperator_properties line 56
  6. theorem OAI.Invariant233.Rotation.towerCyclicOperator_vacuum_error_sq_le line 85
  7. theorem OAI.Invariant233.Rotation.towerCyclicOperator_tendsto_apply line 112