OAI/GroupTheory/SimpleAmenable/Arithmetic/DyadicArithmetic.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.sourceDyadicN line 15
  2. def OAI.SimpleAmenable.sourceDyadicWeight line 16
  3. def OAI.SimpleAmenable.sourceDyadicIndices line 17
  4. theorem OAI.SimpleAmenable.sourceDyadicN_pos line 19
  5. theorem OAI.SimpleAmenable.sourceDyadicN_one_le line 21
  6. theorem OAI.SimpleAmenable.sourceDyadicN_fourth_root line 25
  7. theorem OAI.SimpleAmenable.sourceDyadicN_square_root line 31
  8. theorem OAI.SimpleAmenable.sourceDyadicIndices_exact line 37
  9. theorem OAI.SimpleAmenable.sourceDyadicIndices_card line 43
  10. theorem OAI.SimpleAmenable.sourceDyadic_log line 47
  11. theorem OAI.SimpleAmenable.sourceDyadicWeight_square line 52
  12. theorem OAI.SimpleAmenable.sourceDyadicWeight_energy_bound line 60
  13. theorem OAI.SimpleAmenable.sourceDyadicWeight_energy_tendsto line 76
  14. theorem OAI.SimpleAmenable.sourceDyadic_fine_eventually line 89