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_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_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
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)
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.
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.