Documentation

Mathlib.Data.Nat.Periodic

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_mod (a : ) :
Function.Periodic (fun n => n % a) a
theorem Function.Periodic.map_mod_nat {α : Type u_1} {f : α} {a : } (hf : Function.Periodic f a) (n : ) :
f (n % a) = f n
theorem Nat.filter_multiset_Ico_card_eq_of_periodic (n : ) (a : ) (p : Prop) [DecidablePred 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.

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.