Counting elements in an interval with given residue

The theorems in this file generalise Nat.card_multiples in Mathlib/Data/Nat/Factorization/Basic.lean 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_modEq_eq (a b : ℤ) {r : ℤ} (v : ℤ) : {x ∈ Finset.Ico a b | x ≡ v [ZMOD r]} = Finset.map { toFun := fun (x : ℤ) => x + v, inj' := ⋯ } ({x ∈ Finset.Ico (a - v) (b - v) | r ∣ x})

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

theorem Int.Ico_filter_dvd_eq (a b : ℤ) {r : ℤ} (hr : 0 < r) : {x ∈ Finset.Ico a b | r ∣ x} = 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) : {x ∈ Finset.Ioc a b | r ∣ x} = 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) : ↑{x ∈ Finset.Ico a b | r ∣ x}.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) : ↑{x ∈ Finset.Ioc a b | r ∣ x}.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_card (a b : ℤ) {r : ℤ} (hr : 0 < r) (v : ℤ) : ↑{x ∈ Finset.Ico a b | x ≡ v [ZMOD r]}.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 : ℤ) : ↑{x ∈ Finset.Ioc a b | x ≡ v [ZMOD r]}.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 castEmbedding ({x ∈ Finset.Ico a b | x ≡ v [MOD r]}) = {x ∈ Finset.Ico ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}

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

theorem Nat.Ico_filter_modEq_card (a b : ℕ) {r : ℕ} (hr : 0 < r) (v : ℕ) : ↑{x ∈ Finset.Ico a b | x ≡ v [MOD r]}.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 : ℕ) : ↑{x ∈ Finset.Ioc a b | x ≡ v [MOD r]}.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 : ℕ) : ↑(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 : ℕ) : 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.