OAI/NumberTheory/Ostmann/Preliminaries/DivisibleResidueCount.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform counts of multiples in a prescribed coprime residue class

  1. theorem OAI.Ostmann.divisible_residue_class_count line 10
  2. theorem OAI.Ostmann.dyadic_divisible_residue_class_count line 38
  3. theorem OAI.Ostmann.half_kernel_modulus_le line 52

    Source documentation

    The dyadic range absorbs the additive residue-count error for every half kernel of size at most the square root of its upper endpoint.

    theorem half_kernel_modulus_le (L N r : ℕ) (hN : 2 * L ^ 2 ≤ N) (hr : r ^ 2 ≤ 2 * N) :
    L * r ≤ N := by
…