Elementary bounds for exponentials and logarithms

TheoremLinear upper bound for \(\log(1 - x)\)#✓fully proved

For every real number \(x\) with \(1 - x > 0\), \(\log(1 - x) \le -x\).

theorem log_one_sub_le_neg (x : ℝ) (h1x : (0 : ℝ) < 1 - x) :
    Real.log (1 - x) ≤ -x

Used by 1

Used byTwo-sided bound for \(\log(1 - x)\)

TheoremQuadratic lower bound for \(\log(1 - x)\)#✓fully proved

For every real number \(x\) with \(0 < x < 1/2\), \(-x - x^2 \le \log(1 - x)\).

theorem neg_add_sq_le_log_one_sub (x : ℝ) (hx0 : 0 < x) (hx : x < 1 / 2) :
    -x - x ^ 2 ≤ Real.log (1 - x)

Used by 1

Used byTwo-sided bound for \(\log(1 - x)\)

TheoremTwo-sided bound for \(\log(1 - x)\)#✓fully proved

For every real number \(x\) with \(0 < x < 1/2\), \(-x - x^2 \le \log(1 - x) \le -x\).

theorem log_one_sub_bounds (x : ℝ) (hx0 : 0 < x) (hx : x < 1 / 2) :
    -x - x ^ 2 ≤ Real.log (1 - x) ∧ Real.log (1 - x) ≤ -x

Uses 2

Proof usesLinear upper bound for \(\log(1 - x)\) · Quadratic lower bound for \(\log(1 - x)\)

TheoremQuadratic upper bound for \(e^{-x}\)#✓fully proved

For every real number \(x \ge 0\), \(e^{-x} \le 1 - x + x^2\).

theorem exp_neg_le_one_sub_add_sq (x : ℝ) (hx : 0 ≤ x) :
    Real.exp (-x) ≤ 1 - x + x ^ 2

Used by 1

Used byA round costs weight in proportion to the algorithm's loss, up to a second-order term

TheoremExplicit exponential bound on a fixed power#✓fully proved

An explicit natural multiple of a positive-rate exponential bounds a fixed power.

theorem pow_le_natCeil_mul_exp (n : ℕ) {c x : ℝ} (hc : 0 < c) (hx : 0 ≤ x) :
    x ^ n ≤ (⌈(n.factorial : ℝ) / c ^ n⌉₊ : ℝ) * exp (c * x)

Used by 1

Used byExistence of a constant bounding a power by an exponential

TheoremExistence of a constant bounding a power by an exponential#✓fully proved

A single natural constant bounds a fixed power by a positive-rate exponential.

theorem exists_nat_pow_le_mul_exp (n : ℕ) {c : ℝ} (hc : 0 < c) :
    ∃ C : ℕ, ∀ x : ℝ, 0 ≤ x → x ^ n ≤ C * exp (c * x)

Uses 1 · Used by 1

Proof usesExplicit exponential bound on a fixed power

Used byPolynomial bounded by a base-two exponential

TheoremPolynomial bounded by a base-two exponential#✓fully proved

The source estimate: a natural-input polynomial is bounded by a base-two exponential.

theorem exists_nat_pow_le_mul_two_rpow (n : ℕ) {c : ℝ} (hc : 0 < c) :
    ∃ C : ℕ, ∀ x : ℕ, (x : ℝ) ^ n ≤ C * (2 : ℝ) ^ (c * x)

Uses 1

Proof usesExistence of a constant bounding a power by an exponential

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.