Bounded_Summation_is_Primitive_Recursive

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

computabilityprimitive-recursive-functionsproofwiki

Let the function $f: \N^{k+1} \to \N$ be primitive recursive. Then so is the function $g: \N^{k+1} \to \N$ defined as $\displaystyle g \left({n_1, n_2, \ldots, n_k, z}\right) = \begin{cases} 0 & : z = 0 \\ \sum_{y \mathop = 1}^z f \left({n_1, n_2, \ldots, n_k, y}\right) & : z > 0 \end{cases}$

Preamble

import Mathlib.Computability.Primrec

Formal statement

theorem Bounded_Summation_is_Primitive_Recursive (f : ℕ → ℕ) (hf : Nat.Primrec f) : Nat.Primrec (fun n => (List.range n).map f |>.foldl (· + ·) 0) := by sorry

Source

https://proofwiki.org/wiki/Bounded_Summation_is_Primitive_Recursive

View graph