Periodic Functions on ℕ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file identifies a few functions on ℕ which are periodic, and also proves a lemma about periodic predicates which helps determine their cardinality when filtering intervals over them.

source

theorem nat.periodic_gcd (a : ℕ) :

function.periodic a.gcd a

source

theorem nat.periodic_coprime (a : ℕ) :

function.periodic a.coprime a

source

theorem nat.periodic_mod (a : ℕ) :

function.periodic (λ (n : ℕ), n % a) a

source

theorem function.periodic.map_mod_nat {α : Type u_1} {f : ℕ → α} {a : ℕ} (hf : function.periodic f a) (n : ℕ) :

f (n % a) = f n

source

theorem nat.filter_multiset_Ico_card_eq_of_periodic (n a : ℕ) (p : ℕ → Prop) [decidable_pred p] (pp : function.periodic p a) :

⇑multiset.card (multiset.filter p (multiset.Ico n (n + a))) = nat.count p a

An interval of length a filtered over a periodic predicate of period a has cardinality equal to the number naturals below a for which p a is true.

source

theorem nat.filter_Ico_card_eq_of_periodic (n a : ℕ) (p : ℕ → Prop) [decidable_pred p] (pp : function.periodic p a) :

(finset.filter p (finset.Ico n (n + a))).card = nat.count p a

An interval of length a filtered over a periodic predicate of period a has cardinality equal to the number naturals below a for which p a is true.