OAI/Probability/ClassicalON/TorusFourier.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ClassicalON.DiscreteTorus line 12
  2. def OAI.ClassicalON.torusWave line 14
  3. theorem OAI.ClassicalON.torusWave_norm line 19
  4. theorem OAI.ClassicalON.torusWave_add line 22
  5. theorem OAI.ClassicalON.torusWave_zero line 30
  6. theorem OAI.ClassicalON.torusWave_conj line 33
  7. theorem OAI.ClassicalON.torusWave_mul_conj line 41
  8. theorem OAI.ClassicalON.sum_stdAddChar_mul line 50
  9. theorem OAI.ClassicalON.sum_torusWave line 57
  10. theorem OAI.ClassicalON.torusWave_orthogonal line 65
  11. theorem OAI.ClassicalON.torusWave_orthogonal_subfamily line 71
  12. theorem OAI.ClassicalON.torusWave_intCast line 77
  13. theorem OAI.ClassicalON.norm_stdAddChar_intCast_sub_one line 87
  14. theorem OAI.ClassicalON.torus_mode_difference line 97