OAI/NumberTheory/Ostmann/Construction/SmallEndpointBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Numerical cost of the removed small endpoints

  1. theorem OAI.Ostmann.sqrt_log_prefix_bound line 11
  2. theorem OAI.Ostmann.endpoint_count_product_bound line 32
  3. theorem OAI.Ostmann.eventual_small_endpoint_error line 51