OAI/Analysis/IrrationalRotation/Rotation/WeightedOrbitInvariance.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Invariant233.OrbitInvariance.shiftMap line 11
  2. theorem OAI.Invariant233.OrbitInvariance.shiftMap_mul_neg line 14
  3. def OAI.Invariant233.OrbitInvariance.shiftUnit line 19
  4. theorem OAI.Invariant233.OrbitInvariance.weighted_shift_orbit_inclusion line 25
  5. theorem OAI.Invariant233.OrbitInvariance.diagonal_smul line 33
  6. theorem OAI.Invariant233.OrbitInvariance.weighted_shift_orbit_normalized line 38
  7. theorem OAI.Invariant233.OrbitInvariance.weighted_shift_endpoint_identity line 47
  8. theorem OAI.Invariant233.OrbitInvariance.endpoint_orthogonality line 61
  9. theorem OAI.Invariant233.OrbitInvariance.diagonal_endpoint_orthogonality line 75
  10. theorem OAI.Invariant233.OrbitInvariance.summable_endpoint_coefficients line 81
  11. theorem OAI.Invariant233.OrbitInvariance.tsum_endpoint_coefficients_eq_zero line 87
  12. theorem OAI.Invariant233.OrbitInvariance.weighted_shift_convolution_hasSum line 94
  13. theorem OAI.Invariant233.OrbitInvariance.cocycle_coefficients_hasSum line 116
  14. theorem OAI.Invariant233.OrbitInvariance.cocycle_coefficients_absolute_and_zero line 134