OAI/NumberTheory/ShortEgyptian/IteratedDifferencing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortEgyptian.phase_sub line 10
  2. theorem OAI.ShortEgyptian.backwardDifferences_sub line 14
  3. theorem OAI.ShortEgyptian.backwardDifferences_smul line 23
  4. theorem OAI.ShortEgyptian.backwardDifferences_translate line 29
  5. theorem OAI.ShortEgyptian.backwardDifferences_commute line 39
  6. theorem OAI.ShortEgyptian.interval_phase_correlation line 45
  7. theorem OAI.ShortEgyptian.iterated_interval_vdc line 73
  8. theorem OAI.ShortEgyptian.phase_sum_second_derivative_int line 141