OAI/NumberTheory/DirichletL/Descent/Basic.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseMoment.MarkedMargins line 10
  2. def OAI.SevenEighths.InverseMoment.CanonicalMargins line 13
  3. theorem OAI.SevenEighths.InverseMoment.markedMargins_of_strict line 16
  4. theorem OAI.SevenEighths.InverseMoment.markedMargins_subcollection line 27
  5. theorem OAI.SevenEighths.InverseMoment.canonicalMargins_subcollection line 33
  6. theorem OAI.SevenEighths.InverseMoment.canonicalMargins_weaken line 39
  7. def OAI.SevenEighths.InverseMoment.decrease line 44
  8. def OAI.SevenEighths.InverseMoment.childF line 46
  9. def OAI.SevenEighths.InverseMoment.childM line 49
  10. theorem OAI.SevenEighths.InverseMoment.canonical_transition line 52
  11. theorem OAI.SevenEighths.InverseMoment.child_margins_sharp line 60
  12. theorem OAI.SevenEighths.InverseMoment.child_margins line 75
  13. theorem OAI.SevenEighths.InverseMoment.child_row_decrease line 85
  14. theorem OAI.SevenEighths.InverseMoment.childF_upper line 93
  15. theorem OAI.SevenEighths.InverseMoment.clipping_bounds line 101
  16. theorem OAI.SevenEighths.InverseMoment.step_energy_exponent line 109
  17. def OAI.SevenEighths.InverseMoment.initialF line 117
  18. def OAI.SevenEighths.InverseMoment.initialM line 119
  19. theorem OAI.SevenEighths.InverseMoment.initial_margins_sharp line 122
  20. theorem OAI.SevenEighths.InverseMoment.initial_margins line 133
  21. theorem OAI.SevenEighths.InverseMoment.initial_prefactor_identity line 145
  22. theorem OAI.SevenEighths.InverseMoment.initial_energy_exponent line 151
  23. theorem OAI.SevenEighths.InverseMoment.total_step_loss line 157
  24. theorem OAI.SevenEighths.InverseMoment.depth_margin line 163