English
The fast growing function is defined by cases on the fundamental sequence of an ONote: if the fundamental sequence is inl none, then fastGrowing is the successor function; if inl (some a), it iterates the fastGrowing of a; if inr f, it uses f to define a new function by applying fastGrowing to each f(i).
Русский
Функция быстрого роста определяется по случаям для фундаментальной последовательности ONote: если она равна inl none, то fastGrowing — это функция следующего; если inl (some a), она повторно применяет fastGrowing к a; если inr f, она строит новую функцию через fastGrowing от каждого f(i).
LaTeX
$$$\\forall o\\,{x} :\\; \\text{fundamentalSequence } o = x \\Rightarrow \\, fastGrowing\\ o = \\text{match } x \\text{ with } \\dots$$$
Lean4
/-- The fast growing hierarchy for ordinal notations `< ε₀`. This is a sequence of functions `ℕ → ℕ`
indexed by ordinals, with the definition:
* `f_0(n) = n + 1`
* `f_(α + 1)(n) = f_α^[n](n)`
* `f_α(n) = f_(α[n])(n)` where `α` is a limit ordinal and `α[i]` is the fundamental sequence
converging to `α` -/
def fastGrowing : ONote → ℕ → ℕ
| o =>
match fundamentalSequence o, fundamentalSequence_has_prop o with
| Sum.inl none, _ => Nat.succ
| Sum.inl (some a), h =>
have : a < o := by rw [lt_def, h.1]; apply lt_succ
fun i => (fastGrowing a)^[i] i
| Sum.inr f, h => fun i =>
have : f i < o := (h.2.1 i).2.1
fastGrowing (f i) i
termination_by o => o
