Pierce expansions

DefinitionPierce remainder trajectory#✓fully proved

For natural numbers \(n\) and \(a\), the Pierce 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} = n \bmod t_j\) is the remainder of \(n\) modulo \(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 n % traj n a j

Used by 11

Used byA bound on when a Pierce trajectory vanishes · Pierce trajectories vanish at a positive step · Pierce length · The Pierce length is at most any positive vanishing step · The Pierce length is positive · The Pierce trajectory vanishes at the Pierce length · The Pierce trajectory is nonzero before the Pierce length · First step of the Pierce trajectory · Step of the Pierce trajectory at a zero term · Step of the Pierce trajectory at a nonzero term · Initial term of the Pierce trajectory

TheoremInitial term of the Pierce trajectory#✓fully proved

For all natural numbers \(n\) and \(a\), the Pierce 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 usesPierce remainder trajectory

Used byFirst step of the Pierce trajectory

TheoremStep of the Pierce trajectory at a zero term#✓fully proved

Let \(n\), \(a\) and \(j\) be natural numbers and let \(t_0, t_1, \dots\) be the Pierce 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 1

Statement usesPierce remainder trajectory

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

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

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

Uses 1 · Used by 1

Statement usesPierce remainder trajectory

Used byFirst step of the Pierce trajectory

TheoremFirst step of the Pierce trajectory#✓fully proved

Let \(n\) and \(t\) be natural numbers with \(t \ne 0\). Then the Pierce remainder trajectory of \(t\) with respect to \(n\) is, at step \(1\), equal to \(n \bmod t\), the remainder of \(n\) modulo \(t\).

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

Uses 3

Statement usesPierce remainder trajectory

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

TheoremA bound on when a Pierce trajectory vanishes#✓fully proved

For natural numbers \(n\) and \(a\), let \((t_j)_{j \ge 0}\) be the Pierce remainder trajectory: \(t_0 = a\), and \(t_{j+1} = n \bmod t_j\) if \(t_j \ne 0\), \(t_{j+1} = 0\) if \(t_j = 0\). 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 1 · Used by 1

Statement usesPierce remainder trajectory

Used byPierce trajectories vanish at a positive step

TheoremPierce trajectories vanish at a positive step#✓fully proved

For all natural numbers \(n\) and \(a\), the Pierce remainder trajectory \((t_j)_{j \ge 0}\) of \(n\) and \(a\) (with \(t_0 = a\)) satisfies \(t_j = 0\) for some \(j \ge 1\).

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

Uses 2 · Used by 5

Statement usesPierce remainder trajectory

Proof usesA bound on when a Pierce trajectory vanishes

Used byPierce length · The Pierce length is at most any positive vanishing step · The Pierce length is positive · The Pierce trajectory vanishes at the Pierce length · The Pierce trajectory is nonzero before the Pierce length

DefinitionPierce length#✓fully proved

For natural numbers \(n\) and \(a\), let \((t_j)_{j \ge 0}\) be the Pierce remainder trajectory, with \(t_0 = a\), \(t_{j+1} = n \bmod t_j\) if \(t_j \ne 0\) and \(t_{j+1} = 0\) if \(t_j = 0\). The Pierce length \(\ell(n, a)\) is the least \(j \ge 1\) with \(t_j = 0\); such a \(j\) always exists.

For \(1 \le a \le n\) this is the length of the Pierce expansion of \(a / n\).

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

Uses 2 · Used by 7

Statement usesPierce trajectories vanish at a positive step · Pierce remainder trajectory

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

TheoremThe Pierce length is positive#✓fully proved

For all natural numbers \(n\) and \(a\), the Pierce length \(\ell(n, a)\) satisfies \(\ell(n, a) \ge 1\).

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

Uses 3

Statement usesPierce length

Proof usesPierce trajectories vanish at a positive step · Pierce remainder trajectory

TheoremThe Pierce trajectory vanishes at the Pierce length#✓fully proved

For all natural numbers \(n\) and \(a\), the Pierce remainder trajectory \((t_j)_{j \ge 0}\) of \(n\) and \(a\) satisfies \(t_{\ell(n, a)} = 0\), where \(\ell(n, a)\) is the Pierce length.

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

Uses 3

Statement usesPierce length · Pierce remainder trajectory

Proof usesPierce trajectories vanish at a positive step

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

For natural numbers \(n\), \(a\) and \(j\) with \(j \ge 1\), if the Pierce remainder trajectory \((t_i)_{i \ge 0}\) of \(n\) and \(a\) satisfies \(t_j = 0\), then the Pierce length \(\ell(n, a)\) satisfies \(\ell(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 usesPierce length · Pierce remainder trajectory

Proof usesPierce trajectories vanish at a positive step

TheoremThe Pierce trajectory is nonzero before the Pierce length#✓fully proved

For natural numbers \(n\), \(a\) and \(j\) with \(1 \le j < \ell(n, a)\), where \(\ell(n, a)\) is the Pierce length, the Pierce remainder trajectory \((t_i)_{i \ge 0}\) of \(n\) and \(a\) satisfies \(t_j \ne 0\).

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 usesPierce length · Pierce remainder trajectory

Proof usesPierce trajectories vanish at a positive step

DefinitionMaximal Pierce length#✓fully proved

For a natural number \(n\), the maximal Pierce length \(P(n)\) is the maximum of the Pierce lengths \(\ell(n, a)\) over \(1 \le a \le n\), with \(P(0) = 0\).

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

Uses 1 · Used by 3

Statement usesPierce length

Used byEach Pierce length is at most the maximal Pierce length · A uniform bound on Pierce lengths bounds the maximal Pierce length · Maximal Pierce length via iterated remainder sets

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

For natural numbers \(n\) and \(a\) with \(1 \le a \le n\), the Pierce length \(\ell(n, a)\) satisfies \(\ell(n, a) \le P(n)\), where \(P(n) = \max_{1 \le b \le n} \ell(n, b)\) is the maximal Pierce length.

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

Uses 2

Statement usesPierce length · Maximal Pierce length

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

Let \(n\) and \(L\) be natural numbers. If the Pierce length \(\ell(n, a)\) satisfies \(\ell(n, a) \le L\) for every \(a\) with \(1 \le a \le n\), then the maximal Pierce length \(P(n) = \max_{1 \le a \le n} \ell(n, a)\) (which is \(0\) when \(n = 0\)) satisfies \(P(n) \le L\).

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

Uses 2

Statement usesPierce length · Maximal Pierce length

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.