Theorem 8.6 — properties of the exponential function

Proved

Rudin.ch08_exp_properties

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysis

The exponential function satisfies $E(z+w) = E(z)E(w)$ ; it is its own derivative; it is strictly increasing and positive on $\mathbb{R}$ with $E(x) \to \infty$ as $x \to +\infty$ and $E(x) \to 0$ as $x \to -\infty$ ; and $x^n e^{-x} \to 0$ for every $n$ , so $E$ grows faster than every power.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch08_fourier

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.6: the exponential function satisfies the addition formula, is its own
derivative, is positive and strictly increasing on the real line with limits `+∞` and `0` at
`±∞`, and grows faster than every power. -/
theorem ch08_exp_properties :
    (∀ z w : ℂ, Complex.exp (z + w) = Complex.exp z * Complex.exp w) ∧
    (∀ x : ℝ, HasDerivAt Real.exp (Real.exp x) x) ∧
    StrictMono Real.exp ∧
    Tendsto Real.exp atTop atTop ∧
    Tendsto Real.exp atBot (𝓝 0) ∧
    (∀ n : ℕ, Tendsto (fun x : ℝ => x ^ n * Real.exp (-x)) atTop (𝓝 0)) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 8, p. 180, Theorem 8.6

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Six unconditional assertions about the exponential function, combined into one statement:

Addition formula (complex). For all $z,w \in \mathbb{C}$ : $\exp(z+w) = \exp z \cdot \exp w$ .
Derivative (real). For every $x \in \mathbb{R}$ , the real exponential is differentiable at $x$ with derivative $e^{x}$ .
Strict monotonicity. The real exponential is strictly increasing: $x < y \Rightarrow e^x < e^y$ .
Limit at $+\infty$ . $e^x \to +\infty$ as $x \to +\infty$ .
Limit at $-\infty$ . $e^x \to 0$ as $x \to -\infty$ .
Dominance over powers. For every natural number $n$ : $x^{n} e^{-x} \to 0$ as $x \to +\infty$ .

Positivity of $e^x$ is not stated explicitly. Item 6 includes $n = 0$ .

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph