OAI/Combinatorics/EditDistance/FourierAverages.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Uniform averages and quadratic displacement on finite groups

  1. def OAI.EditFourier.quadraticVariation line 13
  2. lemma OAI.EditFourier.torus_variation_single line 21
  3. lemma OAI.EditFourier.torus_variation_average line 32
  4. theorem OAI.EditFourier.torus_quadratic_comparison line 43
  5. def OAI.EditAverage.avg line 76
  6. lemma OAI.EditAverage.avg_nonneg line 79
  7. lemma OAI.EditAverage.avg_mono line 82
  8. lemma OAI.EditAverage.avg_const line 85
  9. lemma OAI.EditAverage.avg_add line 89
  10. lemma OAI.EditAverage.avg_mul line 92
  11. lemma OAI.EditAverage.avg_sum line 95
  12. lemma OAI.EditAverage.avg_comm line 100
  13. lemma OAI.EditAverage.avg_equiv line 105
  14. lemma OAI.EditAverage.avg_shift line 109
  15. lemma OAI.EditFourier.quadraticVariation_eq_avg line 121
  16. lemma OAI.EditFourier.quadraticVariation_pullback_average line 124
  17. theorem OAI.EditFourier.group_quadratic_comparison line 143