OAI/NumberTheory/Ostmann/Construction/EndpointBaseScale.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An integer endpoint scale compatible with every selected dyadic block

  1. def OAI.Ostmann.endpointBaseScale line 11
  2. def OAI.Ostmann.endpointSize line 12
  3. def OAI.Ostmann.endpointLogScale line 13
  4. theorem OAI.Ostmann.two_rpow_three_fifths_le line 15
  5. theorem OAI.Ostmann.eventual_endpoint_scale line 21