mathlib3 documentation

data.nat.hyperoperation

Hyperoperation sequence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the Hyperoperation sequence. hyperoperation 0 m k = k + 1 hyperoperation 1 m k = m + k hyperoperation 2 m k = m * k hyperoperation 3 m k = m ^ k hyperoperation (n + 3) m 0 = 1 hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)

References #

https://en.wikipedia.org/wiki/Hyperoperation

Tags #

hyperoperation

def hyperoperation :

ℕ → ℕ → ℕ → ℕ

Implementation of the hyperoperation sequence where hyperoperation n m k is the nth hyperoperation between m and k.

Equations

hyperoperation (n.succ.succ + 1) m (k + 1) = hyperoperation n.succ.succ m (hyperoperation (n.succ.succ + 1) m k)
hyperoperation (n + 3) _x 0 = 1
hyperoperation (1 + 1) m (k + 1) = hyperoperation 1 m (hyperoperation (1 + 1) m k)
hyperoperation 2 _x 0 = 0
hyperoperation (0 + 1) m (k + 1) = hyperoperation 0 m (hyperoperation (0 + 1) m k)
hyperoperation 1 m 0 = m
hyperoperation 0 _x k = k + 1

@[simp]

theorem hyperoperation_zero (m : ℕ) :

hyperoperation 0 m = nat.succ

theorem hyperoperation_ge_three_eq_one (n m : ℕ) :

hyperoperation (n + 3) m 0 = 1

theorem hyperoperation_recursion (n m k : ℕ) :

hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)

@[simp]

theorem hyperoperation_one :

hyperoperation 1 = has_add.add

@[simp]

theorem hyperoperation_two :

hyperoperation 2 = has_mul.mul

@[simp]

theorem hyperoperation_three :

hyperoperation 3 = has_pow.pow

theorem hyperoperation_ge_two_eq_self (n m : ℕ) :

hyperoperation (n + 2) m 1 = m

theorem hyperoperation_two_two_eq_four (n : ℕ) :

hyperoperation (n + 1) 2 2 = 4

theorem hyperoperation_ge_three_one (n k : ℕ) :

hyperoperation (n + 3) 1 k = 1

theorem hyperoperation_ge_four_zero (n k : ℕ) :

hyperoperation (n + 4) 0 k = ite (even k) 1 0