OAI/Analysis/IrrationalRotation/Product/ProductCocycle.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductCocycle.rotate_zero line 13
  2. theorem OAI.Invariant233.ProductCocycle.rotate_add line 18
  3. theorem OAI.Invariant233.ProductCocycle.representative_mem_Ico line 23
  4. theorem OAI.Invariant233.ProductCocycle.coe_representative line 27
  5. theorem OAI.Invariant233.ProductCocycle.representative_add line 31
  6. theorem OAI.Invariant233.ProductCocycle.representative_rotate line 42
  7. theorem OAI.Invariant233.ProductCocycle.measurable_representative line 48
  8. theorem OAI.Invariant233.ProductCocycle.measurable_cocycleVersion line 51
  9. theorem OAI.Invariant233.ProductCocycle.cocycleVersion_pos line 62
  10. theorem OAI.Invariant233.ProductCocycle.cocycleVersion_zero line 66
  11. theorem OAI.Invariant233.ProductCocycle.measurePreserving_rotate line 72
  12. theorem OAI.Invariant233.ProductCocycle.cocycleVersion_add_of_finite_support line 85
  13. theorem OAI.Invariant233.ProductCocycle.cocycleVersion_ratio_le_one line 96
  14. theorem OAI.Invariant233.ProductCocycle.cocycleVersion_one_le_one line 107
  15. theorem OAI.Invariant233.ProductCocycle.cocycleVersion_eq_finite_sum line 121
  16. theorem OAI.Invariant233.ProductCocycle.exists_finset_cocycleVersion_one line 129
  17. theorem OAI.Invariant233.ProductCocycle.exists_invariant_cocycle_core line 154
  18. theorem OAI.Invariant233.ProductCocycle.ae_exists_finset_cocycleVersion_one line 180