Counting elements in an interval with given residue

The theorems in this file generalise Nat.card_multiples in Mathlib.Data.Nat.Factorization.Basic to all integer intervals and any fixed residue (not just zero, which reduces to the multiples). Theorems are given for Ico and Ioc intervals.

theorem Int.Ico_filter_dvd_eq (a : ℤ) (b : ℤ) {r : ℤ} (hr : 0 < r) : Finset.filter (fun (x : ℤ) => r ∣ x) (Finset.Ico a b) = Finset.map { toFun := fun (x : ℤ) => x * r, inj' := ⋯ } (Finset.Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)

theorem Int.Ioc_filter_dvd_eq (a : ℤ) (b : ℤ) {r : ℤ} (hr : 0 < r) : Finset.filter (fun (x : ℤ) => r ∣ x) (Finset.Ioc a b) = Finset.map { toFun := fun (x : ℤ) => x * r, inj' := ⋯ } (Finset.Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)

theorem Int.Ico_filter_dvd_card (a : ℤ) (b : ℤ) {r : ℤ} (hr : 0 < r) : ↑(Finset.filter (fun (x : ℤ) => r ∣ x) (Finset.Ico a b)).card = max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0

There are ⌈b / r⌉ - ⌈a / r⌉ multiples of r in [a, b), if a ≤ b.

theorem Int.Ioc_filter_dvd_card (a : ℤ) (b : ℤ) {r : ℤ} (hr : 0 < r) : ↑(Finset.filter (fun (x : ℤ) => r ∣ x) (Finset.Ioc a b)).card = max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0

There are ⌊b / r⌋ - ⌊a / r⌋ multiples of r in (a, b], if a ≤ b.

theorem Int.Ico_filter_modEq_eq (a : ℤ) (b : ℤ) {r : ℤ} (v : ℤ) : Finset.filter (fun (x : ℤ) => x ≡ v [ZMOD r]) (Finset.Ico a b) = Finset.map { toFun := fun (x : ℤ) => x + v, inj' := ⋯ } (Finset.filter (fun (x : ℤ) => r ∣ x) (Finset.Ico (a - v) (b - v)))

theorem Int.Ioc_filter_modEq_eq (a : ℤ) (b : ℤ) {r : ℤ} (v : ℤ) : Finset.filter (fun (x : ℤ) => x ≡ v [ZMOD r]) (Finset.Ioc a b) = Finset.map { toFun := fun (x : ℤ) => x + v, inj' := ⋯ } (Finset.filter (fun (x : ℤ) => r ∣ x) (Finset.Ioc (a - v) (b - v)))

theorem Int.Ico_filter_modEq_card (a : ℤ) (b : ℤ) {r : ℤ} (hr : 0 < r) (v : ℤ) : ↑(Finset.filter (fun (x : ℤ) => x ≡ v [ZMOD r]) (Finset.Ico a b)).card = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0

There are ⌈(b - v) / r⌉ - ⌈(a - v) / r⌉ numbers congruent to v mod r in [a, b), if a ≤ b.

theorem Int.Ioc_filter_modEq_card (a : ℤ) (b : ℤ) {r : ℤ} (hr : 0 < r) (v : ℤ) : ↑(Finset.filter (fun (x : ℤ) => x ≡ v [ZMOD r]) (Finset.Ioc a b)).card = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0

There are ⌊(b - v) / r⌋ - ⌊(a - v) / r⌋ numbers congruent to v mod r in (a, b], if a ≤ b.

theorem Nat.Ico_filter_modEq_cast (a : ℕ) (b : ℕ) {r : ℕ} {v : ℕ} : Finset.map Nat.castEmbedding (Finset.filter (fun (x : ℕ) => x ≡ v [MOD r]) (Finset.Ico a b)) = Finset.filter (fun (x : ℤ) => x ≡ ↑v [ZMOD ↑r]) (Finset.Ico ↑a ↑b)

theorem Nat.Ioc_filter_modEq_cast (a : ℕ) (b : ℕ) {r : ℕ} {v : ℕ} : Finset.map Nat.castEmbedding (Finset.filter (fun (x : ℕ) => x ≡ v [MOD r]) (Finset.Ioc a b)) = Finset.filter (fun (x : ℤ) => x ≡ ↑v [ZMOD ↑r]) (Finset.Ioc ↑a ↑b)

theorem Nat.Ico_filter_modEq_card (a : ℕ) (b : ℕ) {r : ℕ} (hr : 0 < r) (v : ℕ) : ↑(Finset.filter (fun (x : ℕ) => x ≡ v [MOD r]) (Finset.Ico a b)).card = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0

There are ⌈(b - v) / r⌉ - ⌈(a - v) / r⌉ numbers congruent to v mod r in [a, b), if a ≤ b. Nat version of Int.Ico_filter_modEq_card.

theorem Nat.Ioc_filter_modEq_card (a : ℕ) (b : ℕ) {r : ℕ} (hr : 0 < r) (v : ℕ) : ↑(Finset.filter (fun (x : ℕ) => x ≡ v [MOD r]) (Finset.Ioc a b)).card = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0

There are ⌊(b - v) / r⌋ - ⌊(a - v) / r⌋ numbers congruent to v mod r in (a, b], if a ≤ b. Nat version of Int.Ioc_filter_modEq_card.

theorem Nat.count_modEq_card_eq_ceil (b : ℕ) {r : ℕ} (hr : 0 < r) (v : ℕ) : ↑(Nat.count (fun (x : ℕ) => x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉

There are ⌈(b - v % r) / r⌉ numbers in [0, b) congruent to v mod r.

theorem Nat.count_modEq_card (b : ℕ) {r : ℕ} (hr : 0 < r) (v : ℕ) : Nat.count (fun (x : ℕ) => x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0

There are b / r + [v % r < b % r] numbers in [0, b) congruent to v mod r, where [·] is the Iverson bracket.