OuterRowsMod.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Residue classes in a finite interval

Each residue class modulo w occurs at least n / w times in Fin n. On any interval of length at most w, reduction modulo w is injective.

theorem OAI.QuantitativeVanDerWaerden.card_mod_row_lower line 16

Source documentation

Each row modulo w contains at least one point from each complete block.

theorem card_mod_row_lower (n w : ℕ) (hw : 0 < w) (j : Fin w) :
    n / w ≤ (Finset.univ.filter (fun i : Fin n => i.val % w = j.val)).card := by
…

theorem OAI.QuantitativeVanDerWaerden.card_mod_row_subtype_lower line 38

Source documentation

Subtype-cardinality form of card_mod_row_lower.

theorem card_mod_row_subtype_lower (n w : ℕ) (hw : 0 < w) (j : Fin w) :
    n / w ≤ Fintype.card {i : Fin n // i.val % w = j.val} := by
…

theorem OAI.QuantitativeVanDerWaerden.eq_of_mod_eq_of_mem_interval line 43

Source documentation

Equal residues in one interval of width w represent the same number.

theorem eq_of_mod_eq_of_mem_interval {a w x y : ℕ}
    (hxlo : a ≤ x) (hxhi : x < a + w)
    (hylo : a ≤ y) (hyhi : y < a + w)
    (hmod : x % w = y % w) : x = y := by
…

theorem OAI.QuantitativeVanDerWaerden.div_le_div_of_mul_le line 52
Source documentation
Cross multiplication gives a comparison of the integer row-size bounds.
```
theorem div_le_div_of_mul_le {M w d L : ℕ}
    (hw : 0 < w) (hd : 0 < d) (h : M * w ≤ d * L) :
    M / d ≤ L / w := by
…
```
theorem OAI.QuantitativeVanDerWaerden.div_ten_le_div_of_sandwich line 63