Runs of multiples: definitions

For a finite set S of positive integers and a ∈ S, kVal S a is the least positive integer k with k * a ∉ S. We write L S a = kVal S a - 1 for the length of the run a, 2a, …, L a inside S, and A S t for the set of a ∈ S whose run has length ≥ t.

noncomputable def RunsOfMultiples.kVal (S : Finset ℕ) (a : ℕ) : ℕ

kVal S a is the least positive integer k with k * a ∉ S.

Equations

• RunsOfMultiples.kVal S a = sInf {k : ℕ | 0 < k ∧ k * a ∉ S}

def RunsOfMultiples.A (S : Finset ℕ) (t : ℕ) : Finset ℕ

The elements of S whose first t multiples all lie in S.

Equations

• RunsOfMultiples.A S t = {a ∈ S | ∀ i ∈ Finset.Icc 1 t, i * a ∈ S}

noncomputable def RunsOfMultiples.L (S : Finset ℕ) (a : ℕ) : ℕ

Run length L S a = kVal S a - 1.

Equations

• RunsOfMultiples.L S a = RunsOfMultiples.kVal S a - 1

theorem RunsOfMultiples.kVal_set_nonempty (S : Finset ℕ) {a : ℕ} (ha : 0 < a) : {k : ℕ | 0 < k ∧ k * a ∉ S}.Nonempty

theorem RunsOfMultiples.kVal_pos (S : Finset ℕ) {a : ℕ} (ha : 0 < a) : 0 < kVal S a

theorem RunsOfMultiples.kVal_not_mem (S : Finset ℕ) {a : ℕ} (ha : 0 < a) : kVal S a * a ∉ S

theorem RunsOfMultiples.mul_mem_of_lt_kVal (S : Finset ℕ) {a i : ℕ} (hi : 0 < i) (hik : i < kVal S a) : i * a ∈ S

theorem RunsOfMultiples.forall_mul_mem_iff (S : Finset ℕ) {a : ℕ} (ha : 0 < a) (t : ℕ) : (∀ i ∈ Finset.Icc 1 t, i * a ∈ S) ↔ t < kVal S a

The run characterisation: the first t multiples of a lie in S iff t < kVal S a.

theorem RunsOfMultiples.mem_A_iff (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {a t : ℕ} : a ∈ A S t ↔ a ∈ S ∧ t ≤ L S a

theorem RunsOfMultiples.A_subset (S : Finset ℕ) (t : ℕ) : A S t ⊆ S

theorem RunsOfMultiples.A_anti (S : Finset ℕ) {s t : ℕ} (hst : s ≤ t) : A S t ⊆ A S s

theorem RunsOfMultiples.mul_mem_of_mem_A {S : Finset ℕ} {t a i : ℕ} (ha : a ∈ A S t) (hi1 : 1 ≤ i) (hit : i ≤ t) : i * a ∈ S

If a ∈ A S t and 1 ≤ i ≤ t then i * a ∈ S.

theorem RunsOfMultiples.L_le_card (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {a : ℕ} (haS : a ∈ S) : L S a ≤ S.card

The run length is at most |S|.

theorem RunsOfMultiples.sum_kVal_eq (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) : ∑ a ∈ S, kVal S a = S.card + ∑ a ∈ S, L S a