OAI/Probability/ClassicalON/DyadicFourier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ClassicalON.DyadicFreq line 9
  2. def OAI.ClassicalON.dyadicRadius line 11
  3. def OAI.ClassicalON.dyadicPoint line 13
  4. theorem OAI.ClassicalON.dyadicRadius_pos line 16
  5. theorem OAI.ClassicalON.dyadicRadius_le line 20
  6. theorem OAI.ClassicalON.dyadicPoint_bounds line 23
  7. theorem OAI.ClassicalON.dyadicPoint_injective line 31
  8. theorem OAI.ClassicalON.zmod_cast_inj_interval line 59
  9. def OAI.ClassicalON.dyadicTorusPoint line 68
  10. theorem OAI.ClassicalON.dyadicTorusPoint_injective line 71
  11. theorem OAI.ClassicalON.dyadic_shell_card_bounds line 88