OAI/NumberTheory/TwoPoint/Walks/TupleSmoothCost.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The retained tuple introduces at most a factor two into the smooth Euler cost, because all its primes lie above the canonical lower endpoint.

  1. lemma OAI.TwoPointCorrelations.smooth_half_cost_of_large_factors line 14
  2. lemma OAI.TwoPointCorrelations.eventually_canonical_smooth_half_cost line 40
  3. lemma OAI.TwoPointCorrelations.dilated_tuple_smooth_cost line 64