OAI/NumberTheory/TwoPoint/Halasz/HalaszCountMonotone.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Monotonicity in the summation endpoint, needed to give the short moment one common endpoint after summing over the selected primes.

  1. theorem OAI.TwoPointCorrelations.halasz_vinogradov_count_mono line 12
  2. theorem OAI.TwoPointCorrelations.halasz_vinogradov_prime_recurrence line 33