noncomputable def KolakoskiSequence.setToSeq (s : Set ℕ) (n : ℕ) : ℕ

Equations

• KolakoskiSequence.setToSeq s n = Classical.epsilon fun (k : ℕ) => k ∈ s ∧ (s.filter fun (x : ℕ) => x < k).ncard = n

noncomputable def KolakoskiSequence.runs {α : Type u_1} (a : ℕ → α) : ℕ → ℕ

Equations

• KolakoskiSequence.runs a = KolakoskiSequence.setToSeq {n : ℕ | n = 0 ∨ a (n - 1) ≠ a n}

def KolakoskiSequence.lengths (a : ℕ → ℕ) (n : ℕ) : ℕ

Equations

• KolakoskiSequence.lengths a n = a (n + 1) - a n

def KolakoskiSequence.IsKolakoski (K : ℕ → ℕ) : Prop

Equations

• KolakoskiSequence.IsKolakoski K = (Set.range K = {1, 2} ∧ KolakoskiSequence.lengths (KolakoskiSequence.runs K) = K)

noncomputable def KolakoskiSequence.kolakoski : ℕ → ℕ

Equations

• KolakoskiSequence.kolakoski = Classical.epsilon fun (K : ℕ → ℕ) => KolakoskiSequence.IsKolakoski K ∧ K 0 = 1