Documentation

Mathlib.Data.Int.CardIntervalMod

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