OAI/NumberTheory/ShortEgyptian/MomentRecurrence.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortEgyptian.momentDimension line 12
  2. def OAI.ShortEgyptian.descentR line 13
  3. def OAI.ShortEgyptian.descentAlpha line 14
  4. lemma OAI.ShortEgyptian.descentR_ge_two line 16
  5. lemma OAI.ShortEgyptian.descentR_eq line 17
  6. lemma OAI.ShortEgyptian.descentAlpha_bounds line 18
  7. def OAI.ShortEgyptian.MomentScale line 25
  8. lemma OAI.ShortEgyptian.eventually_MomentScale line 30
  9. lemma OAI.ShortEgyptian.level_moment line 33
  10. lemma OAI.ShortEgyptian.shifted_subset_sum line 70
  11. def OAI.ShortEgyptian.levelDensity line 82
  12. lemma OAI.ShortEgyptian.levelDensity_bounds line 85
  13. lemma OAI.ShortEgyptian.levelDensity_last line 90
  14. lemma OAI.ShortEgyptian.level_holder line 94
  15. lemma OAI.ShortEgyptian.density_precise_recurrence line 106