Mathlib.Data.Nat.Periodic

Module docstring

{"# 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. "}

Nat.periodic_gcd theorem

(a : ℕ) : Periodic (gcd a) a

Full source

theorem periodic_gcd (a : ℕ) : Periodic (gcd a) a := by
  simp only [forall_const, gcd_add_self_right, eq_self_iff_true, Periodic]

Periodicity of the Greatest Common Divisor Function with Fixed First Argument

Informal description

For any natural number $a$, the function $\gcd(a, \cdot)$ is periodic with period $a$, meaning that for all natural numbers $n$, we have $\gcd(a, n + a) = \gcd(a, n)$.

Nat.periodic_coprime theorem

(a : ℕ) : Periodic (Coprime a) a

Full source

theorem periodic_coprime (a : ℕ) : Periodic (Coprime a) a := by
  simp only [coprime_add_self_right, forall_const, eq_iff_iff, Periodic]

Periodicity of Coprimality with Fixed Natural Number

Informal description

For any natural number $a$, the predicate $\text{Coprime}(a, \cdot)$ is periodic with period $a$, meaning that for all natural numbers $n$, $\text{Coprime}(a, n) = \text{Coprime}(a, n + a)$.

Nat.periodic_mod theorem

(a : ℕ) : Periodic (fun n => n % a) a

Full source

theorem periodic_mod (a : ℕ) : Periodic (fun n => n % a) a := by
  simp only [forall_const, eq_self_iff_true, add_mod_right, Periodic]

Periodicity of Modulo Operation on Natural Numbers

Informal description

For any natural number $a$, the function $n \mapsto n \bmod a$ is periodic with period $a$.

Function.Periodic.map_mod_nat theorem

{α : Type*} {f : ℕ → α} {a : ℕ} (hf : Periodic f a) : ∀ n, f (n % a) = f n

Full source

theorem _root_.Function.Periodic.map_mod_nat {α : Type*} {f : ℕ → α} {a : ℕ} (hf : Periodic f a) :
    ∀ n, f (n % a) = f n := fun n => by
  conv_rhs => rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]

Periodic Function Property under Modulo Operation

Informal description

For any function $f \colon \mathbb{N} \to \alpha$ that is periodic with period $a \in \mathbb{N}$, and for any natural number $n$, the value of $f$ at $n \bmod a$ is equal to the value of $f$ at $n$, i.e., $f(n \bmod a) = f(n)$.

Nat.filter_multiset_Ico_card_eq_of_periodic theorem

(n a : ℕ) (p : ℕ → Prop) [DecidablePred p] (pp : Periodic p a) : card (filter p (Ico n (n + a))) = a.count p

Full source

/-- 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 filter_multiset_Ico_card_eq_of_periodic (n a : ℕ) (p : ℕ → Prop) [DecidablePred p]
    (pp : Periodic p a) : card (filter p (Ico n (n + a))) = a.count p := by
  rw [count_eq_card_filter_range, Finset.card, Finset.filter_val, Finset.range_val, ←
    multiset_Ico_map_mod n, ← map_count_True_eq_filter_card, ← map_count_True_eq_filter_card,
    map_map]
  congr; funext n
  exact (Function.Periodic.map_mod_nat pp n).symm

Cardinality of Filtered Periodic Interval Equals Count of Period Elements

Informal description

For any natural numbers $n$ and $a$, and any decidable periodic predicate $p$ on $\mathbb{N}$ with period $a$, the cardinality of the multiset obtained by filtering the interval $[n, n + a)$ with $p$ is equal to the count of elements in $\{0, \dots, a-1\}$ that satisfy $p$. That is, \[ \text{card}(\text{filter } p \ [n, n + a)) = \text{count}(p, \{0, \dots, a-1\}). \]

Nat.filter_Ico_card_eq_of_periodic theorem

(n a : ℕ) (p : ℕ → Prop) [DecidablePred p] (pp : Periodic p a) : ((Ico n (n + a)).filter p).card = a.count p

Full source

/-- 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 filter_Ico_card_eq_of_periodic (n a : ℕ) (p : ℕ → Prop) [DecidablePred p]
    (pp : Periodic p a) : ((Ico n (n + a)).filter p).card = a.count p :=
  filter_multiset_Ico_card_eq_of_periodic n a p pp

Cardinality of Filtered Periodic Interval Equals Count over One Period

Informal description

For any natural numbers $n$ and $a$, and any decidable periodic predicate $p$ on $\mathbb{N}$ with period $a$, the cardinality of the filtered interval $[n, n + a)$ under $p$ is equal to the number of elements in $\{0, \dots, a-1\}$ satisfying $p$. That is, \[ |\{x \in [n, n + a) \mid p(x)\}| = |\{k \in \{0, \dots, a-1\} \mid p(k)\}|. \]