OAI/Combinatorics/EditDistance/FourierCharacters.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite Fourier inversion, Parseval, and character displacement

  1. def OAI.EditFourier.transform line 16
  2. theorem OAI.EditFourier.transform_twice line 19
  3. theorem OAI.EditFourier.transform_sub line 33
  4. theorem OAI.EditFourier.transform_shift line 39
  5. theorem OAI.EditFourier.transform_pairing line 55
  6. theorem OAI.EditFourier.transform_conj line 67
  7. theorem OAI.EditFourier.parseval line 77
  8. theorem OAI.EditFourier.displacement line 90
  9. def OAI.EditFourier.fourier line 106
  10. theorem OAI.EditFourier.displacement_normalized line 109
  11. def OAI.EditFourier.productCharacter line 126
  12. theorem OAI.EditFourier.productCharacter_single line 132
  13. theorem OAI.EditFourier.productCharacter_primitive line 142
  14. def OAI.EditFourier.torusCharacter line 153
  15. theorem OAI.EditFourier.torusCharacter_primitive line 157
  16. theorem OAI.EditFourier.norm_pow_sub_one_le line 168
  17. theorem OAI.EditFourier.root_separation line 183