Polynomially bounded functions are closed under products

Proved

SipserGacsLautemann.polynomiallyBounded_mul

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 product $n \mapsto f(n) \cdot 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$ . Products are exactly what appears when a machine performs a polynomially bounded number of rounds, each of polynomially bounded cost — the shape of every simulation argument in this mission.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem polynomiallyBounded_mul {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