OAI/NumberTheory/TwoPoint/ShortIntervals/MRTNestedQuotients.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual nested correction, prefix and gcd quotients. No identification of a rounded quotient with a real quotient is used.

  1. lemma OAI.TwoPointCorrelations.mrt_div_add_one_lower line 10
  2. lemma OAI.TwoPointCorrelations.mrt_nested_outer_lower line 19
  3. lemma OAI.TwoPointCorrelations.mrt_nested_prefix_lower line 28
  4. lemma OAI.TwoPointCorrelations.mrt_nested_prefix_power_lower line 47
  5. lemma OAI.TwoPointCorrelations.mrt_nested_prefix_large line 63
  6. lemma OAI.TwoPointCorrelations.mrt_nested_prefix_prime_ratio line 77
  7. lemma OAI.TwoPointCorrelations.mrt_nested_prefix_upper line 90