OAI/Analysis/IrrationalRotation/Rotation/FiniteSupportWeights.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.FiniteSupportWeights.ae_finite_support line 20
  2. theorem OAI.Invariant233.FiniteSupportWeights.ae_all_finite_support line 26
  3. def OAI.Invariant233.FiniteSupportWeights.integerCore line 32
  4. theorem OAI.Invariant233.FiniteSupportWeights.ae_mem_integerCore line 35
  5. theorem OAI.Invariant233.FiniteSupportWeights.measurableSet_integerCore line 40
  6. theorem OAI.Invariant233.FiniteSupportWeights.integerCore_subset line 51
  7. theorem OAI.Invariant233.FiniteSupportWeights.mem_integerCore_translate_iff line 58
  8. theorem OAI.Invariant233.FiniteSupportWeights.ae_all_translates_finite_support line 68
  9. theorem OAI.Invariant233.FiniteSupportWeights.finite_support_mul_cost line 76
  10. theorem OAI.Invariant233.FiniteSupportWeights.summable_mul_cost line 84
  11. theorem OAI.Invariant233.FiniteSupportWeights.exp_neg_tsum_mem_Ioc line 88
  12. theorem OAI.Invariant233.FiniteSupportWeights.uniform_nonzero_floor_of_nonneg line 96
  13. theorem OAI.Invariant233.FiniteSupportWeights.uniform_nonzero_floor_of_nonpos line 122
  14. theorem OAI.Invariant233.FiniteSupportWeights.uniform_nonzero_floor_le line 146
  15. theorem OAI.Invariant233.FiniteSupportWeights.measure_nonzero_floor_le line 159
  16. theorem OAI.Invariant233.FiniteSupportWeights.measurableSet_finite_support line 168
  17. theorem OAI.Invariant233.FiniteSupportWeights.ae_finite_floor_support line 193
  18. theorem OAI.Invariant233.FiniteSupportWeights.ae_all_finite_floor_support line 206
  19. theorem OAI.Invariant233.FiniteSupportWeights.exists_invariant_conull_floor_support line 213