Convergence Propagation

theorem Collatz.converges_step {n : ℕ} (h : CollatzConverges n) : CollatzConverges (collatz n)

theorem Collatz.converges_preimage {n : ℕ} (h : CollatzConverges (collatz n)) : CollatzConverges n

theorem Collatz.not_converges_zero : ¬CollatzConverges 0

theorem Collatz.converges_iterate {n : ℕ} (h : CollatzConverges n) (k : ℕ) : CollatzConverges (collatz^[k] n)

Syracuse Shortcut

def Collatz.collatzShortcut (n : ℕ) : ℕ

The Syracuse shortcut map: for odd n, applies one step of 3n+1 and one step of /2.

Equations

• Collatz.collatzShortcut n = if n % 2 = 0 then n / 2 else (3 * n + 1) / 2

@[simp]

theorem Collatz.collatzShortcut_even {n : ℕ} (h : n % 2 = 0) : collatzShortcut n = n / 2

@[simp]

theorem Collatz.collatzShortcut_odd {n : ℕ} (h : n % 2 = 1) : collatzShortcut n = (3 * n + 1) / 2

theorem Collatz.collatzShortcut_odd_eq_collatz_collatz {n : ℕ} (h : n % 2 = 1) : collatzShortcut n = collatz (collatz n)

Stopping Time

theorem Collatz.stoppingTime_one : stoppingTime 1 converges_one = 0

theorem Collatz.stoppingTime_step {n : ℕ} (hn : n ≠ 1) (h : CollatzConverges n) (h' : CollatzConverges (collatz n)) : stoppingTime n h = stoppingTime (collatz n) h' + 1