OAI/Combinatorics/EditDistance/PrimeCharacters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Coprime roots and prime-product Fourier multipliers

  1. theorem OAI.EditFourier.prod_roots_pow line 18
  2. theorem OAI.EditFourier.coprime_roots_nontrivial line 27
  3. theorem OAI.EditFourier.coprime_root_separation line 44
  4. lemma OAI.EditFourier.norm_sub_one_sq_of_norm_one line 65
  5. lemma OAI.EditFourier.character_multiplier_four line 75
  6. lemma OAI.EditFourier.average_character_multiplier line 83
  7. lemma OAI.EditFourier.std_character_pow line 97
  8. theorem OAI.EditFourier.multiplier_comparison line 112