OAI/NumberTheory/Ostmann/ZeroDensity/PositiveResidueProgression.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact finite progression of positive integers in a residue class

  1. theorem OAI.Ostmann.exists_positive_residue_representative line 11
  2. theorem OAI.Ostmann.positive_residue_progression line 19
  3. theorem OAI.Ostmann.sum_positive_residue_progression line 54
  4. theorem OAI.Ostmann.sum_positive_zmod_progression line 63
  5. theorem OAI.Ostmann.positive_progression_length_bounds line 72

    Source documentation

    The floor cutoff loses less than two progression steps, uniformly in the residue. This keeps the inverse estimate at the original quadratic scale.

    theorem positive_progression_length_bounds (q a : ℕ) (B Y : ℝ)
    (hq : 0 < q) (ha : 0 < a) (haq : a ≤ q) (hB : 3 ≤ B) (hY : 1 ≤ Y) :
    let W := ⌊B * q * Y⌋₊
…