OAI/NumberTheory/Ostmann/Quadratic/QuadraticGcdRangeBridge.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A genuine dyadic range after removing the common divisor

  1. def OAI.Ostmann.quadraticRangeCoeff line 13
  2. theorem OAI.Ostmann.quadratic_gcd_pair_range_extension line 16
  3. def OAI.Ostmann.quadraticGcdBlockSize line 52
  4. def OAI.Ostmann.quadraticGcdBlockCoeff line 54
  5. theorem OAI.Ostmann.quadratic_gcd_block_range line 57
  6. theorem OAI.Ostmann.quadratic_gcd_block_lower line 67
  7. theorem OAI.Ostmann.quadratic_gcd_block_reindex line 78
  8. theorem OAI.Ostmann.quadratic_range_energy line 88
  9. theorem OAI.Ostmann.quadratic_gcd_block_energy line 106
  10. theorem OAI.Ostmann.quadraticGcdBlockSize_pos line 114
  11. theorem OAI.Ostmann.quadraticGcdBlockSize_le line 119
  12. theorem OAI.Ostmann.quadraticGcdBlockSize_comparable line 124
  13. theorem OAI.Ostmann.quadratic_gcd_block_divisor_moment line 135