OAI/Combinatorics/ProgressionColoring/ResidueFiber.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuantitativeVanDerWaerden.residue_fiber_span line 10

   Source documentation

   The endpoints of a residue fiber of size at least two differ by a positive number of denominator steps, at least one for each intervening index.

   theorem residue_fiber_span (J : Finset ℕ) (hJ : J.Nonempty) {h k : ℕ}
       (hh : 0 < h) (hcard : 2 ≤ J.card)
       (hcongr : ∀ a ∈ J, ∀ b ∈ J, (h : ℤ) ∣ (b : ℤ) - (a : ℤ))
       (hbound : ∀ j ∈ J, j < k) :
       ∃ c : ℕ, 0 < c ∧ J.card - 1 ≤ c ∧
         J.max' hJ - J.min' hJ = c * h ∧ c * h < k := by
   …