OAI/NumberTheory/Ostmann/ZeroDensity/ProgressionLiftCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform integer-lift counts in a residue class

  1. theorem OAI.Ostmann.progression_Ico_card_le line 14

    Source documentation

    A residue class has at most interval length / modulus + 1 representatives. This form is uniform in the residue and works across zero.

    theorem progression_Ico_card_le (lo hi q r : ℤ) (hlo : lo ≤ hi) (hq : 0 < q) :
    (((Finset.Ico lo hi).filter fun n => n ≡ r [ZMOD q]).card : ℚ) ≤
      ((hi : ℚ) - lo) / q + 1 := by
…