OAI/NumberTheory/JointDickman/Amplification/AdditionProgressionInterval.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A common interval for additions in a factor-four size window

  1. def OAI.JointDickman.additionIntervalLower line 10
  2. def OAI.JointDickman.additionIntervalUpper line 11
  3. theorem OAI.JointDickman.additionInterval_order line 13
  4. theorem OAI.JointDickman.additionInterval_contains line 20
  5. theorem OAI.JointDickman.additionInterval_denominator line 28
  6. theorem OAI.JointDickman.additionInterval_length line 40