Periodic Functions on ℕ

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.

theorem Nat.periodic_gcd (a : Nat) : Function.Periodic a.gcd a

theorem Nat.periodic_coprime (a : Nat) : Function.Periodic a.Coprime a

theorem Nat.periodic_mod (a : Nat) : Function.Periodic (fun (n : Nat) => HMod.hMod n a) a

theorem Function.Periodic.map_mod_nat {α : Type u_1} {f : Nat → α} {a : Nat} (hf : Periodic f a) (n : Nat) : Eq (f (HMod.hMod n a)) (f n)

theorem Nat.filter_multiset_Ico_card_eq_of_periodic (n a : Nat) (p : Nat → Prop) [DecidablePred p] (pp : Function.Periodic p a) : Eq (Multiset.filter p (Multiset.Ico n (HAdd.hAdd n a))).card (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.

theorem Nat.filter_Ico_card_eq_of_periodic (n a : Nat) (p : Nat → Prop) [DecidablePred p] (pp : Function.Periodic p a) : Eq (Finset.filter p (Finset.Ico n (HAdd.hAdd n a))).card (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.