OAI/NumberTheory/Ostmann/Conclusion/Scales.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Conclusion.bulkScale line 10
  2. def OAI.Ostmann.Conclusion.bulkSize line 12
  3. def OAI.Ostmann.Conclusion.initialGap line 14
  4. def OAI.Ostmann.Conclusion.stepGap line 17
  5. def OAI.Ostmann.Conclusion.frequencyBudget line 21
  6. def OAI.Ostmann.Conclusion.frequencyBound line 25
  7. theorem OAI.Ostmann.Conclusion.bulkSize_even line 28
  8. theorem OAI.Ostmann.Conclusion.bulkSize_bounds line 31
  9. theorem OAI.Ostmann.Conclusion.bulkSize_tendsto_atTop line 41
  10. theorem OAI.Ostmann.Conclusion.sum_dyadic line 51
  11. theorem OAI.Ostmann.Conclusion.sum_dyadic_log line 57
  12. theorem OAI.Ostmann.Conclusion.frequencyBudget_eq line 69
  13. def OAI.Ostmann.Conclusion.finalRate line 85
  14. theorem OAI.Ostmann.Conclusion.finalRate_div_tendsto line 89
  15. theorem OAI.Ostmann.Conclusion.finalRate_tendsto_atBot line 107
  16. theorem OAI.Ostmann.Conclusion.exists_depth_for_final_rate line 119