OAI/Analysis/RotationWeights/MeasurableWeight.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CircleModel.CircleX line 56
  2. def OAI.CircleModel.repr line 57
  3. lemma OAI.CircleModel.repr_mem line 58
  4. lemma OAI.CircleModel.repr_mk line 60
  5. lemma OAI.CircleModel.repr_coe line 63
  6. lemma OAI.CircleModel.measurable_repr line 65
  7. def OAI.CircleModel.Xi line 68
  8. def OAI.CircleModel.beta line 69
  9. def OAI.CircleModel.shift line 70
  10. lemma OAI.CircleModel.Xi_shift line 72
  11. lemma OAI.CircleModel.floor_cocycle line 80
  12. def OAI.CircleModel.floorTerm line 87
  13. def OAI.CircleModel.good0 line 90
  14. def OAI.CircleModel.good line 93
  15. lemma OAI.CircleModel.shift_add line 96
  16. lemma OAI.CircleModel.shift_zero line 99
  17. lemma OAI.CircleModel.good_shift line 100
  18. lemma OAI.CircleModel.good_subset_good0 line 109
  19. lemma OAI.CircleModel.floorTerm_add line 113
  20. lemma OAI.CircleModel.floorTerm_zero line 117
  21. lemma OAI.CircleModel.floorTerm_mono line 122
  22. def OAI.CircleModel.exponent line 129
  23. def OAI.CircleModel.cocycle line 132
  24. lemma OAI.CircleModel.summable_exponent line 135
  25. lemma OAI.CircleModel.exponent_add line 144
  26. lemma OAI.CircleModel.cocycle_add line 150
  27. lemma OAI.CircleModel.cocycle_pos line 157
  28. lemma OAI.CircleModel.cocycle_zero line 164
  29. lemma OAI.CircleModel.cocycle_antitone line 168
  30. lemma OAI.CircleModel.measurable_Xi line 180
  31. lemma OAI.CircleModel.measurePreserving_XiMap line 183
  32. lemma OAI.CircleModel.measure_repr_lower line 188
  33. lemma OAI.CircleModel.measure_repr_upper line 205
  34. lemma OAI.CircleModel.floorTerm_event_bound line 222
  35. lemma OAI.CircleModel.ae_good0 line 253
  36. lemma OAI.CircleModel.ae_good line 262
  37. lemma OAI.CircleModel.measurable_floorTerm line 268
  38. lemma OAI.CircleModel.finite_support_iff line 272
  39. lemma OAI.CircleModel.measurableSet_good0 line 287
  40. lemma OAI.CircleModel.measurableSet_good line 294
  41. lemma OAI.CircleModel.measurable_exponent line 300
  42. lemma OAI.CircleModel.measurable_cocycle line 304
  43. lemma OAI.CircleModel.floor_unit_interval_bounds line 312
  44. lemma OAI.CircleModel.floorTerm_difference_le_one line 321
  45. lemma OAI.CircleModel.floorTerm_ordered line 329
  46. lemma OAI.CircleModel.cocycle_ratio_exp line 333
  47. lemma OAI.CircleModel.cocycle_ratio_nonneg line 340
  48. lemma OAI.CircleModel.cocycle_ratio_tail_bound line 344
  49. lemma OAI.CircleModel.cocycle_ratio_ordered line 369
  50. lemma OAI.CircleModel.floor_crossing line 375
  51. lemma OAI.CircleModel.cocycle_ratio_crossing line 385