OAI/NumberTheory/ShortEgyptian/WindowSpectrum.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortEgyptian.natWindow line 12
  2. theorem OAI.ShortEgyptian.natCast_injOn_range line 14
  3. theorem OAI.ShortEgyptian.natWindow_card line 22
  4. theorem OAI.ShortEgyptian.natWindow_sum line 25
  5. def OAI.ShortEgyptian.frequencyDistance line 29
  6. theorem OAI.ShortEgyptian.frequencyDistance_pos line 31
  7. theorem OAI.ShortEgyptian.char_nat_eq_phase line 38
  8. theorem OAI.ShortEgyptian.natWindow_char_bound line 48
  9. theorem OAI.ShortEgyptian.sum_injective_nonneg_bound line 68
  10. theorem OAI.ShortEgyptian.harmonic_square_tail line 81
  11. theorem OAI.ShortEgyptian.frequency_square_tail line 91
  12. theorem OAI.ShortEgyptian.window_spectral_tail line 132