OAI/NumberTheory/TwoPoint/Walks/CanonicalRoughScale.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Reparametrizing the stronger qualitative estimate at the actual quantitative prime-band endpoint exp(L^.995). The gain survives the finite tuple expansion and the final reciprocal L normalizer.

  1. def OAI.TwoPointCorrelations.canonicalRoughParameter line 13
  2. lemma OAI.TwoPointCorrelations.canonicalRoughParameter_prime_endpoint line 15
  3. lemma OAI.TwoPointCorrelations.canonicalRoughParameter_square_ge line 21
  4. lemma OAI.TwoPointCorrelations.canonicalRoughParameter_error line 33
  5. lemma OAI.TwoPointCorrelations.canonicalRoughParameter_tendsto line 39
  6. lemma OAI.TwoPointCorrelations.tuple_expansion_small_power line 42
  7. lemma OAI.TwoPointCorrelations.canonical_centering_rate_bound line 56