OAI/NumberTheory/ShortEgyptian/FiniteFourier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortEgyptian.additive_orthogonality line 12
  2. theorem OAI.ShortEgyptian.finite_parseval line 18
  3. theorem OAI.ShortEgyptian.bilinear_character_sq_bound line 43
  4. theorem OAI.ShortEgyptian.bilinear_character_unit_sq_bound line 62
  5. theorem OAI.ShortEgyptian.real_probability_energy_bound line 79
  6. theorem OAI.ShortEgyptian.bilinear_probability_bound line 90
  7. theorem OAI.ShortEgyptian.complex_sum_sq_le line 109
  8. theorem OAI.ShortEgyptian.complex_sum_norm_sq line 117
  9. theorem OAI.ShortEgyptian.finite_van_der_corput line 123