Engel expansions

DefinitionNegated remainder#✓fully proved

For natural numbers \(n\) and \(k\) with \(k \ge 1\), the negated remainder of \(n\) modulo \(k\) is the unique \(u\) with \(0 \le u < k\) and \(u \equiv -n \pmod{k}\): it equals \(0\) when \(k\) divides \(n\) and \(k - (n \bmod k)\) otherwise. For \(k = 0\) it is defined to be \(0\).

def negRem (n k : ℕ) : ℕ :=
  (k - n % k) % k

Used by 7

Used byAn Engel trajectory started at \(a\) vanishes within \(a + 1\) steps · Engel trajectories vanish at a positive step · Characterization of the negated remainder · Engel remainder trajectory · First step of the Engel trajectory · Zero is absorbing for the Engel trajectory · Step of the Engel trajectory at a nonzero term

TheoremCharacterization of the negated remainder#✓fully proved

For natural numbers \(n\), \(k\) and \(u\) with \(k \ne 0\), the negated remainder of \(n\) modulo \(k\) equals \(u\) if and only if \(u < k\) and \(k\) divides \(n + u\).

This is the natural-number form of \(u \equiv -n \pmod{k}\).

theorem negRem_eq_iff {n k u : ℕ} (hk : k ≠ 0) :
    negRem n k = u ↔ u < k ∧ k ∣ n + u

Uses 1

Statement usesNegated remainder

DefinitionEngel remainder trajectory#✓fully proved

For natural numbers \(n\) and \(a\), the Engel remainder trajectory of \(a\) with respect to \(n\) is the sequence \(t_0, t_1, t_2, \dots\) of natural numbers with \(t_0 = a\) and, for every \(j \ge 0\), \(t_{j+1} = 0\) if \(t_j = 0\), while if \(t_j \ne 0\) then \(t_{j+1}\) is the negated remainder of \(n\) modulo \(t_j\): the unique natural number \(u < t_j\) with \(u \equiv -n \pmod{t_j}\). Once the trajectory reaches \(0\) it stays there.

def traj (n a : ℕ) : ℕ → ℕ
  | 0 => a
  | j + 1 => if traj n a j = 0 then 0 else negRem n (traj n a j)

Uses 1 · Used by 11

Statement usesNegated remainder

Used byAn Engel trajectory started at \(a\) vanishes within \(a + 1\) steps · Engel trajectories vanish at a positive step · Engel length · The Engel length is at most any positive vanishing step · The Engel length is positive · Engel trajectory vanishes at the Engel length · Engel trajectory is nonzero at positive steps before the Engel length · First step of the Engel trajectory · Zero is absorbing for the Engel trajectory · Step of the Engel trajectory at a nonzero term · Initial term of the Engel trajectory

TheoremInitial term of the Engel trajectory#✓fully proved

For all natural numbers \(n\) and \(a\), the Engel remainder trajectory of \(a\) with respect to \(n\) has value \(a\) at step \(0\).

theorem traj_zero (n a : ℕ) : traj n a 0 = a

Uses 1 · Used by 1

Statement usesEngel remainder trajectory

Used byFirst step of the Engel trajectory

TheoremZero is absorbing for the Engel trajectory#✓fully proved

Let \(n\), \(a\) and \(j\) be natural numbers and let \(t_0, t_1, \dots\) be the Engel remainder trajectory of \(a\) with respect to \(n\). If \(t_j = 0\), then \(t_{j+1} = 0\).

theorem traj_succ_of_eq_zero {n a j : ℕ} (h : traj n a j = 0) :
    traj n a (j + 1) = 0

Uses 2

Statement usesEngel remainder trajectory

Proof usesNegated remainder

TheoremStep of the Engel trajectory at a nonzero term#✓fully proved

Let \(n\), \(a\) and \(j\) be natural numbers and let \(t_0, t_1, \dots\) be the Engel remainder trajectory of \(a\) with respect to \(n\). If \(t_j \ne 0\), then \(t_{j+1}\) is the negated remainder of \(n\) modulo \(t_j\): the unique natural number \(u < t_j\) with \(u \equiv -n \pmod{t_j}\).

theorem traj_succ_of_ne_zero {n a j : ℕ} (h : traj n a j ≠ 0) :
    traj n a (j + 1) = negRem n (traj n a j)

Uses 2 · Used by 1

Statement usesNegated remainder · Engel remainder trajectory

Used byFirst step of the Engel trajectory

TheoremFirst step of the Engel trajectory#✓fully proved

Let \(n\) and \(t\) be natural numbers with \(t \ne 0\). Then the Engel remainder trajectory of \(t\) with respect to \(n\) is, at step \(1\), the negated remainder of \(n\) modulo \(t\): the unique natural number \(u < t\) with \(u \equiv -n \pmod{t}\).

theorem traj_one {n t : ℕ} (ht : t ≠ 0) : traj n t 1 = negRem n t

Uses 4

Statement usesNegated remainder · Engel remainder trajectory

Proof usesStep of the Engel trajectory at a nonzero term · Initial term of the Engel trajectory

TheoremAn Engel trajectory started at \(a\) vanishes within \(a + 1\) steps#✓fully proved

Let \(n\) and \(a\) be natural numbers and let \(t_0 = a, t_1, t_2, \dots\) be the Engel trajectory of \(a\) with respect to \(n\). Then \(t_i = 0\) for some \(i \le a + 1\).

theorem exists_traj_eq_zero (n a : ℕ) : ∃ i ≤ a + 1, traj n a i = 0

Uses 2 · Used by 1

Statement usesEngel remainder trajectory

Proof usesNegated remainder

Used byEngel trajectories vanish at a positive step

TheoremEngel trajectories vanish at a positive step#✓fully proved

Let \(n\) and \(a\) be natural numbers and let \(t_0 = a, t_1, t_2, \dots\) be the Engel trajectory of \(a\) with respect to \(n\). Then \(t_j = 0\) for some \(j \ge 1\).

theorem exists_traj_eq_zero_pos (n a : ℕ) : ∃ j ≥ 1, traj n a j = 0

Uses 3 · Used by 5

Statement usesEngel remainder trajectory

Proof usesAn Engel trajectory started at \(a\) vanishes within \(a + 1\) steps · Negated remainder

Used byEngel length · The Engel length is at most any positive vanishing step · The Engel length is positive · Engel trajectory vanishes at the Engel length · Engel trajectory is nonzero at positive steps before the Engel length

DefinitionEngel length#✓fully proved

For natural numbers \(n\) and \(a\), let \(t_0 = a, t_1, t_2, \dots\) be the Engel trajectory of \(a\) with respect to \(n\). The Engel length \(L(n, a)\) is the least \(j \ge 1\) with \(t_j = 0\).

For \(1 \le a \le n\) this is the number of terms of the Engel expansion of \(a / n\).

noncomputable def length (n a : ℕ) : ℕ :=
  Nat.find (exists_traj_eq_zero_pos n a)

Uses 2 · Used by 7

Statement usesEngel trajectories vanish at a positive step · Engel remainder trajectory

Used byEach Engel length is at most the maximal Engel length · The Engel length is at most any positive vanishing step · The Engel length is positive · Maximal Engel length · A uniform bound on Engel lengths bounds the maximal Engel length · Engel trajectory vanishes at the Engel length · Engel trajectory is nonzero at positive steps before the Engel length

TheoremThe Engel length is positive#✓fully proved

For all natural numbers \(n\) and \(a\), the Engel length \(L(n, a)\) of \(a\) with respect to \(n\) satisfies \(L(n, a) \ge 1\).

theorem length_pos (n a : ℕ) : 1 ≤ length n a

Uses 3

Statement usesEngel length

Proof usesEngel trajectories vanish at a positive step · Engel remainder trajectory

TheoremEngel trajectory vanishes at the Engel length#✓fully proved

For all natural numbers \(n\) and \(a\), let \(L\) be the Engel length of \(a\) with respect to \(n\). Then the Engel remainder trajectory of \(a\) with respect to \(n\) is \(0\) at step \(L\).

theorem traj_length_eq_zero (n a : ℕ) : traj n a (length n a) = 0

Uses 3

Statement usesEngel length · Engel remainder trajectory

Proof usesEngel trajectories vanish at a positive step

TheoremThe Engel length is at most any positive vanishing step#✓fully proved

Let \(n\), \(a\) and \(j\) be natural numbers with \(j \ge 1\), and let \(t_0 = a, t_1, t_2, \dots\) be the Engel trajectory of \(a\) with respect to \(n\). If \(t_j = 0\), then the Engel length \(L(n, a)\) satisfies \(L(n, a) \le j\).

theorem length_le_of_traj_eq_zero {n a j : ℕ} (hj : 1 ≤ j)
    (h : traj n a j = 0) : length n a ≤ j

Uses 3

Statement usesEngel length · Engel remainder trajectory

Proof usesEngel trajectories vanish at a positive step

TheoremEngel trajectory is nonzero at positive steps before the Engel length#✓fully proved

Let \(n\), \(a\) and \(j\) be natural numbers and let \(L\) be the Engel length of \(a\) with respect to \(n\). If \(1 \le j < L\), then the Engel remainder trajectory of \(a\) with respect to \(n\) is nonzero at step \(j\).

theorem traj_ne_zero_of_lt_length {n a j : ℕ} (hj : 1 ≤ j)
    (hlt : j < length n a) : traj n a j ≠ 0

Uses 3

Statement usesEngel length · Engel remainder trajectory

Proof usesEngel trajectories vanish at a positive step

DefinitionMaximal Engel length#✓fully proved

For a natural number \(n\), the maximal Engel length is \(M(n) = \max_{1 \le a \le n} L(n, a)\), where \(L(n, a)\) is the Engel length of \(a\) with respect to \(n\); for \(n = 0\) the maximum is over the empty set and \(M(0) = 0\).

noncomputable def maxLength (n : ℕ) : ℕ :=
  (Finset.Icc 1 n).sup (length n)

Uses 1 · Used by 2

Statement usesEngel length

Used byEach Engel length is at most the maximal Engel length · A uniform bound on Engel lengths bounds the maximal Engel length

TheoremEach Engel length is at most the maximal Engel length#✓fully proved

Let \(n\) and \(a\) be natural numbers with \(1 \le a \le n\). Then the Engel length \(L(n, a)\) of \(a\) with respect to \(n\) is at most the maximal Engel length \(M(n) = \max_{1 \le b \le n} L(n, b)\).

theorem length_le_maxLength {n a : ℕ} (ha : a ∈ Finset.Icc 1 n) :
    length n a ≤ maxLength n

Uses 2

Statement usesEngel length · Maximal Engel length

TheoremA uniform bound on Engel lengths bounds the maximal Engel length#✓fully proved

Let \(n\) and \(B\) be natural numbers. If the Engel length \(L(n, a)\) of \(a\) with respect to \(n\) satisfies \(L(n, a) \le B\) for every \(a\) with \(1 \le a \le n\), then the maximal Engel length \(M(n) = \max_{1 \le a \le n} L(n, a)\) (with \(M(0) = 0\)) satisfies \(M(n) \le B\).

theorem maxLength_le_of_forall {n L : ℕ}
    (h : ∀ a ∈ Finset.Icc 1 n, length n a ≤ L) : maxLength n ≤ L

Uses 2

Statement usesEngel length · Maximal Engel length

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.