OAI/NumberTheory/JointDickman/Amplification/MarkovRemainders.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform control of the Markov multipliers on sieve remainders

  1. theorem OAI.JointDickman.auxiliaryLogLength_between line 13
  2. theorem OAI.JointDickman.prefix_markov_multiplier_bounds line 28
  3. theorem OAI.JointDickman.tail_markov_multiplier_bound line 49