OAI/NumberTheory/DirichletL/Energy/WidthSchedule.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.amplification line 12
  2. def OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.count line 13
  3. def OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.scale line 14
  4. def OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.reserve line 15
  5. def OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.mesh line 17
  6. def OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.width line 18
  7. def OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.loss line 19
  8. theorem OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.bounds line 21
  9. lemma OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.reserve_cost line 61
  10. theorem OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.one_time_losses line 72
  11. lemma OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.mesh_lt_prime_width line 92
  12. lemma OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.width_zero line 100
  13. lemma OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.loss_zero line 101
  14. lemma OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.width_succ line 102
  15. lemma OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.loss_succ line 106
  16. lemma OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.child_band line 111
  17. lemma OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.loss_le_final line 117
  18. lemma OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.next_paid_loss line 126
  19. theorem OAI.SevenEighths.CenteredMomentEnergyWidthSchedule.actual_removal_path line 140