Polynomial bounds and logarithms

Polynomially bounded functions have logarithmic logarithms: if s is polynomially bounded, then ⌈log₂ (s n)⌉ is at most e (⌊log₂ n⌋ + 1) for a constant e (PolynomiallyBounded.exists_clog_le_mul_log). Conversely, 2 to the power c (⌊log₂ n⌋ + 1) is polynomially bounded (polynomiallyBounded_two_pow_mul_log). These are the conversions between depth O(log n) and size n ^ O(1) in circuit complexity. Logarithmic bounds c (⌊log₂ n⌋ + 1) are themselves polynomially bounded (polynomiallyBounded_mul_log2_add_one).

Here ⌊log₂ n⌋ + 1, written Nat.log 2 n + 1, is the number of binary digits of n with 0 written as one digit, that is max n.size 1, which unlike Nat.size n is positive at n = 0.

Main results

• Cslib.PolynomiallyBounded.exists_clog_le_mul_log: the logarithm of a polynomially bounded function is O(log n).
• Cslib.polynomiallyBounded_two_pow_mul_log: 2 ^ O(log n) is polynomially bounded.
• Cslib.polynomiallyBounded_clog_two: binary ceiling logarithms preserve polynomial bounds.
• Cslib.polynomiallyBounded_mul_log2_add_one: O(log n) is polynomially bounded.

theorem Cslib.polynomiallyBounded_clog_two {f : ℕ → ℕ} (hf : PolynomiallyBounded f) : PolynomiallyBounded fun (n : ℕ) => Nat.clog 2 (f n)

The binary ceiling logarithm of a polynomially bounded function is polynomially bounded.

theorem Cslib.polynomiallyBounded_two_pow_mul_log (c : ℕ) : PolynomiallyBounded fun (n : ℕ) => 2 ^ (c * (Nat.log 2 n + 1))

2 ^ (c (⌊log₂ n⌋ + 1)) is polynomially bounded: it is at most 2 ^ c (n + 1) ^ c.

theorem Cslib.polynomiallyBounded_mul_log2_add_one (c : ℕ) : PolynomiallyBounded fun (n : ℕ) => c * (n.log2 + 1)

c (log₂ n + 1) is polynomially bounded: it is at most c (n + 1).

theorem Cslib.PolynomiallyBounded.exists_clog_le_mul_log {s : ℕ → ℕ} (hs : PolynomiallyBounded s) : ∃ (e : ℕ), ∀ (n : ℕ), Nat.clog 2 (s n) ≤ e * (Nat.log 2 n + 1)

The binary logarithm of a polynomially bounded function is at most e (⌊log₂ n⌋ + 1) for a constant e.