Numbering a tuple

A walk is a tuple of darts, and a coin sequence is a tuple of coins. This module numbers such a tuple the way a numeral works: the j-th entry contributes its own number times the base to the j-th power. Reading an entry back is dividing by that power and taking the remainder, which is what an algorithm does.

Main results

• Complexity.NumEnc.instPi — the NumEnc instance for Fin n → α
• Complexity.NumEnc.digit_sum, Complexity.NumEnc.sum_digits — reading a digit, and reassembling a number from its digits

Digits

theorem Complexity.NumEnc.sum_lt_pow {c n : ℕ} (g : ℕ → ℕ) (hg : ∀ i < n, g i < c) : ∑ i ∈ Finset.range n, g i * c ^ i < c ^ n

theorem Complexity.NumEnc.digit_sum {c : ℕ} (hc : 0 < c) (g : ℕ → ℕ) {n j : ℕ} : j < n → (∀ i < n, g i < c) → (∑ i ∈ Finset.range n, g i * c ^ i) / c ^ j % c = g j

theorem Complexity.NumEnc.sum_digits {c n i : ℕ} : i < c ^ n → ∑ j ∈ Finset.range n, i / c ^ j % c * c ^ j = i

The instance

theorem Complexity.NumEnc.get_eq {α : Type} [NumEnc α] {i : ℕ} (hi : i < card α) {a : α} (h : i = enc a) : get hi = a

def Complexity.NumEnc.encAt {α : Type} {n : ℕ} [NumEnc α] (f : Fin n → α) (i : ℕ) : ℕ

The number of the i-th entry of a tuple, or zero past its end.

Equations

• Complexity.NumEnc.encAt f i = if h : i < n then Complexity.NumEnc.enc (f ⟨i, h⟩) else 0

theorem Complexity.NumEnc.encAt_lt {α : Type} {n : ℕ} [NumEnc α] (f : Fin n → α) {i : ℕ} (hi : i < n) : encAt f i < card α

@[instance_reducible]

instance Complexity.NumEnc.instPi {α : Type} (n : ℕ) [NumEnc α] : NumEnc (Fin n → α)

A tuple is numbered like a numeral.

Equations

• One or more equations did not get rendered due to their size.