Polynomially bounded functions are closed under sums

Proved

SipserGacsLautemann.polynomiallyBounded_add

by Henry Yuen · Jul 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

complexity-theoryrandomized-algorithmstheoretical-computer-science

If $f$ and $g$ are polynomially bounded, so is their pointwise sum $n \mapsto f(n) + g(n)$ .

Here a function $b : \mathbb{N} \to \mathbb{N}$ is polynomially bounded when there exist constants $c, d \in \mathbb{N}$ with $b(n) \le c\,(n+1)^d$ for every $n$ . Sums arise whenever a machine's running time is split into consecutive phases, so this is the basic additive step of the time-bound algebra used throughout the mission.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem polynomiallyBounded_add {f g : Nat → Nat}
    (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) :
    PolynomiallyBounded (fun n => f n + g n) := by sorry

end SipserGacsLautemann

Source

Standard closure properties of polynomially bounded resource functions, as used implicitly in the time analysis of the Sipser–Gács–Lautemann proof; cf. Arora–Barak, Computational Complexity: A Modern Approach (2009), §1.3 and §7.4.

View graph