def KolakoskiSequence.f₁ (xs : List ℕ) : List ℕ

Equations

• KolakoskiSequence.f₁ xs = List.flatMap (fun (x : ℕ × ℕ) => match x with | (x, n) => List.replicate x (if Even n then 1 else 2)) (xs.zip (List.range xs.length))

@[irreducible]

def KolakoskiSequence.f₂ (xs : List ℕ) (n k : ℕ) : List ℕ

Equations

• KolakoskiSequence.f₂ xs n k = if k = 0 ∨ n ≤ xs.length then xs else KolakoskiSequence.f₂ (KolakoskiSequence.f₁ xs) n (k - 1)

def KolakoskiSequence.f₃ (n : ℕ) : List ℕ

Equations

• KolakoskiSequence.f₃ n = List.take n (KolakoskiSequence.f₂ [1, 2] n n)

def KolakoskiSequence.kolakoski' (n : ℕ) : ℕ

Equations

• KolakoskiSequence.kolakoski' n = (KolakoskiSequence.f₃ (n + 1))[n]!

class KolakoskiSequence.KolIter (xs : List ℕ) : Prop

• h : ∃ (n : ℕ), f₁^[n] [1, 2] = xs

class KolakoskiSequence.Diverse {α : Type u_1} (a : ℕ → α) : Prop

• h (N : ℕ) : ∃ (n : ℕ), N ≤ n ∧ a N ≠ a n

theorem KolakoskiSequence.kolIter_iff {xs : List ℕ} : KolIter xs ↔ ∃ (n : ℕ), f₁^[n] [1, 2] = xs

@[simp]

instance KolakoskiSequence.kolIter_zero : KolIter [1, 2]

@[simp]

instance KolakoskiSequence.kolIter_succ {xs : List ℕ} [h : KolIter xs] : KolIter (f₁ xs)

@[simp]

instance KolakoskiSequence.kolIter_iterate {xs : List ℕ} {n : ℕ} [h : KolIter xs] : KolIter (f₁^[n] xs)

@[simp]

theorem KolakoskiSequence.f₂_0 {xs : List ℕ} {n : ℕ} : f₂ xs n 0 = xs

@[simp]

theorem KolakoskiSequence.f₃_0 : f₃ 0 = []

@[simp]

theorem KolakoskiSequence.prefix_f₁ {xs : List ℕ} [h : KolIter xs] : xs <+: f₁ xs

@[simp]

theorem KolakoskiSequence.prefix_iterate_f₁ {xs : List ℕ} {n : ℕ} [h : KolIter xs] : xs <+: f₁^[n] xs

@[simp]

theorem KolakoskiSequence.length_f₁ {xs : List ℕ} : (f₁ xs).length = xs.sum

@[simp]

theorem KolakoskiSequence.base_prefix_of_kolIter {xs : List ℕ} [h : KolIter xs] : [1, 2] <+: xs

@[simp]

theorem KolakoskiSequence.not_kolIter_nil : ¬KolIter []

@[simp]

theorem KolakoskiSequence.ne_nil_of_kolIter {xs : List ℕ} [h : KolIter xs] : xs ≠ []

@[simp]

theorem KolakoskiSequence.length_pos_of_kolIter {xs : List ℕ} [h : KolIter xs] : 0 < xs.length

@[simp]

theorem KolakoskiSequence.one_lt_length_of_kolIter {xs : List ℕ} [h : KolIter xs] : 1 < xs.length

@[simp]

theorem KolakoskiSequence.getElem_zero_of_kolIter {xs : List ℕ} [h : KolIter xs] : xs[0] = 1

@[simp]

theorem KolakoskiSequence.getElem_one_of_kolIter {xs : List ℕ} [h : KolIter xs] : xs[1] = 2

@[simp]

theorem KolakoskiSequence.mem_iff_of_kolIter {xs : List ℕ} {x : ℕ} [h : KolIter xs] : x ∈ xs ↔ x = 1 ∨ x = 2

@[simp]

theorem KolakoskiSequence.length_lt_sum_of_kolIter {xs : List ℕ} [h : KolIter xs] : xs.length < xs.sum

theorem KolakoskiSequence.length_iterate_f₁_ge {n : ℕ} : n ≤ (f₁^[n] [1, 2]).length

@[simp]

instance KolakoskiSequence.kolIter_f₂ {xs : List ℕ} {n k : ℕ} [h : KolIter xs] : KolIter (f₂ xs n k)

@[simp]

theorem KolakoskiSequence.prefix_f₂ {xs : List ℕ} {n k : ℕ} [h : KolIter xs] : xs <+: f₂ xs n k

@[simp]

theorem KolakoskiSequence.length_iterate_f₁_lt_iff {xs : List ℕ} {n m : ℕ} [h : KolIter xs] : (f₁^[n] xs).length < (f₁^[m] xs).length ↔ n < m

@[simp]

theorem KolakoskiSequence.length_iterate_f₁_eq_iff {xs : List ℕ} {n m : ℕ} [h : KolIter xs] : (f₁^[n] xs).length = (f₁^[m] xs).length ↔ n = m

@[simp]

theorem KolakoskiSequence.length_iterate_f₁_le_iff {xs : List ℕ} {n m : ℕ} [h : KolIter xs] : (f₁^[n] xs).length ≤ (f₁^[m] xs).length ↔ n ≤ m

@[simp]

theorem KolakoskiSequence.iterate_f₁_prefix_iterate_iff {xs : List ℕ} {n m : ℕ} [h : KolIter xs] : f₁^[n] xs <+: f₁^[m] xs ↔ n ≤ m

@[simp]

theorem KolakoskiSequence.iterate_f₁_eq_iff {xs : List ℕ} {n m : ℕ} [h : KolIter xs] : f₁^[n] xs = f₁^[m] xs ↔ n = m

theorem KolakoskiSequence.le_length_f₂ {xs : List ℕ} {n k : ℕ} [h : KolIter xs] (h₁ : n ≤ k) : n ≤ (f₂ xs n k).length

@[simp]

theorem KolakoskiSequence.le_length_f₂_same {xs : List ℕ} {n : ℕ} [h : KolIter xs] : n ≤ (f₂ xs n n).length

@[simp]

theorem KolakoskiSequence.length_f₃ {n : ℕ} : (f₃ n).length = n

@[simp]

theorem KolakoskiSequence.f₃_succ_getElem! {n : ℕ} : (f₃ (n + 1))[n]! = (f₃ (n + 1))[n]

@[simp]

theorem KolakoskiSequence.f₃_eq_iff {n m : ℕ} : f₃ n = f₃ m ↔ n = m

theorem KolakoskiSequence.kolIter_prefix_or_prefix (xs ys : List ℕ) [hx : KolIter xs] [hy : KolIter ys] : xs <+: ys ∨ ys <+: xs

@[simp]

theorem KolakoskiSequence.f₃_prefix_iff_le {n m : ℕ} : f₃ n <+: f₃ m ↔ n ≤ m

@[simp]

theorem KolakoskiSequence.f₁_one : f₃ 1 = [1]

@[simp]

theorem KolakoskiSequence.f₁_two : f₃ 2 = [1, 2]

@[simp]

theorem KolakoskiSequence.mem_f₃_iff {n x : ℕ} : x ∈ f₃ n ↔ x = 1 ∧ 1 ≤ n ∨ x = 2 ∧ 2 ≤ n

@[simp]

theorem KolakoskiSequence.range_kolakoski' : Set.range kolakoski' = {1, 2}

theorem KolakoskiSequence.diverse_iff {α : Type u_1} {a : ℕ → α} : Diverse a ↔ ∀ (N : ℕ), ∃ (n : ℕ), N ≤ n ∧ a N ≠ a n

@[simp]

theorem KolakoskiSequence.kolakoski'_zero : kolakoski' 0 = 1

@[simp]

theorem KolakoskiSequence.kolakoski'_one : kolakoski' 1 = 2

theorem KolakoskiSequence.exi_f₃_prefix_kolIter {i : ℕ} : ∃ (xs : List ℕ), KolIter xs ∧ f₃ i <+: xs