Exponential and logarithmic functions

Lens

MotivationH

Grains on a chessboard

A well-known legend, told in many versions across India, Persia and the Arab world, says that the inventor of chess asked a king for a modest reward: one grain of wheat on the first square of the board, two on the second, four on the third, doubling on each of the $64$ squares. The king laughed at so small a request — until his treasurers worked it out. The last square alone needs $2^{63} \approx 9.2 \times 10^{18}$ grains. The whole board needs $2^{64} - 1$ , more wheat than the world has ever harvested.

Or take a sheet of paper $0.1$ mm thick. Fold it in half $42$ times (if you could): it would be about $440\,000$ km thick, farther than the Moon.

Multiplying by the same factor again and again — exponential growth — is utterly unlike adding the same amount again and again. This lesson makes exponents work for all real numbers. It introduces logarithms to answer "how many doublings?", and it meets the number $e \approx 2.71828$ , which turns up whenever growth is continuous.

IntuitionH

Adding versus multiplying

Compare two savings plans over five years. In plan A you add $100$ each year; in plan B your savings grow by $10\%$ each year (multiply by $1.1$ ).

year	0	1	2	3	4	5
A: add 100	1000	1100	1200	1300	1400	1500
B: multiply by 1.1	1000	1100	1210	1331	1464.1	1610.51

In A the differences between consecutive years are constant; in B the ratios are. At first they look alike. Soon B pulls ahead, and the gap widens faster and faster: after $30$ years plan A holds $4000$ and plan B more than $17\,000$ .

Decay works the same way. A medicine or a radioactive substance with a half-life of $8$ days keeps $\tfrac12$ of what it had every $8$ days: $100\% \to 50\% \to 25\% \to 12.5\% \to \cdots$ In this model it never quite reaches zero.

DefinitionsH

Definitions

For a real number $a > 0$ and a positive integer $n$ , $a^n = a \cdot a \cdots a$ ( $n$ factors). From this, $a^m a^n = a^{m+n}$ and $(a^m)^n = a^{mn}$ by counting factors.

Definition— zero, negative and rational exponents

For $a > 0$ , integers $m$ and positive integers $n$ :

a^0 = 1, \qquad a^{-n} = \frac{1}{a^n}, \qquad a^{1/n} = \sqrt[n]{a} \ \text{(the positive $n$-th root)}, \qquad a^{m/n} = \left(a^{1/n}\right)^m.

For an irrational exponent such as $\sqrt 2$ , $a^{\sqrt 2}$ is the number that $a^{1.4}, a^{1.41}, a^{1.414}, \dots$ approach. This gives $2^{\sqrt 2} \approx 2.665$ . Making this precise needs the completeness of the real numbers. Mathlib instead defines $a^x = e^{x \ln a}$ , which gives the same values.

Definition— exponential function

For a fixed base $a > 0$ , $a \neq 1$ , the function $x \mapsto a^x$ on $\R$ is the exponential function with base $a$ . It is increasing if $a > 1$ (growth) and decreasing if $0 < a < 1$ (decay).

Definition— logarithm

For $a > 0$ with $a \ne 1$ and $x > 0$ , the logarithm of $x$ to base $a$ , $\log_a x$ , is the number $y$ with $a^y = x$ . The natural logarithm is $\ln x = \log_e x$ .

So $\log_2 8 = 3$ because $2^3 = 8$ , $\log_{10} 0.01 = -2$ because $10^{-2} = 0.01$ , and $\log_a 1 = 0$ for every base. A logarithm answers the question "which power?", or in growth terms, "how many doublings (or tenfoldings)?"

Definition— the number e

$e$ is the limit of $\left(1 + \tfrac1n\right)^n$ as $n$ grows without bound; $e = 2.718281828\ldots$ The function $x \mapsto e^x$ is called the exponential function, $\exp x$ .

That this limit exists is a theorem, proved below.

ProofH

Why the definitions are forced

Theorem— The laws of exponents determine the exponents

Suppose a function $E : \R \to \R$ , not identically zero, satisfies the law $E(x + y) = E(x)\,E(y)$ for all real $x, y$ , and let $a = E(1)$ . Then:

$E(0) = 1$ ;
$E(-x) = \dfrac{1}{E(x)}$ , and $E(x) > 0$ for all $x$ ;
$E(n x) = E(x)^n$ for every integer $n$ ; in particular $E(n) = a^n$ ;
$E\!\left(\tfrac{m}{n}\right)$ is the positive $n$ -th root of $a^m$ , for all integers $m$ and $n > 0$ .

Proof

Pick $x$ with $E(x) \neq 0$ . Then $E(x) = E(x + 0) = E(x)E(0)$ , and dividing by $E(x)$ gives $E(0) = 1$ .
$E(x)E(-x) = E(x - x) = E(0) = 1$ , so $E(-x) = 1/E(x)$ and $E(x) \ne 0$ . Also $E(x) = E\!\left(\tfrac x2 + \tfrac x2\right) = E\!\left(\tfrac x2\right)^2 \ge 0$ , so $E(x) > 0$ .
For $n \ge 0$ by induction: $E((n + 1)x) = E(nx + x) = E(x)^n E(x)$ . For negative $n$ use part 2.
By part 3, $E\!\left(\tfrac mn\right)^n = E\!\left(n \cdot \tfrac mn\right) = E(m) = a^m$ , and $E\!\left(\tfrac mn\right) > 0$ by part 2. A positive number has only one positive $n$ -th root: if $0 < u < v$ then $u^n < v^n$ .

∎

So if we want the law $a^{x + y} = a^x a^y$ to keep working, then $a^0$ must be $1$ , $a^{-n}$ must be $1/a^n$ , and $a^{m/n}$ must be $\sqrt[n]{a^m}$ . The definitions are not conventions chosen for convenience: they are the only ones consistent with the law. Part 4 also shows that $a^{m/n}$ does not depend on how the fraction is written ( $a^{2/4} = a^{1/2}$ ), because it is pinned down by the value of $\tfrac mn$ alone.

Theorem— Laws of logarithms

For $a > 0$ , $a \ne 1$ , $x, y > 0$ and every real $r$ :

\log_a(xy) = \log_a x + \log_a y, \qquad \log_a\!\left(\frac xy\right) = \log_a x - \log_a y, \qquad \log_a(x^r) = r \log_a x,

and the change-of-base formula $\log_a x = \dfrac{\ln x}{\ln a}$ .

Proof

Let $u = \log_a x$ and $v = \log_a y$ , so $a^u = x$ and $a^v = y$ . Then $a^{u + v} = a^u a^v = xy$ , so $\log_a(xy) = u + v$ . Similarly $a^{u - v} = x/y$ and $a^{ru} = (a^u)^r = x^r$ . For change of base, write $x = a^u$ and take $\ln$ of both sides: $\ln x = u \ln a$ , so $u = \ln x / \ln a$ (and $\ln a \ne 0$ because $a \ne 1$ ).

∎

Theorem— Exponentials and logarithms are inverse functions

For $a > 0$ , $a \neq 1$ , the function $x \mapsto a^x$ is a bijection from $\R$ onto $(0, \infty)$ . Its inverse is $y \mapsto \log_a y$ :

a^{\log_a y} = y \ \ (y > 0), \qquad \log_a(a^x) = x \ \ (x \in \R).

Proof

Injective: if $a > 1$ and $x < y$ , then $a^y = a^x a^{y - x}$ with $a^{y - x} > 1$ , so $a^y > a^x$ . The function is strictly increasing, hence injective (for $0 < a < 1$ it is strictly decreasing). Surjective onto $(0, \infty)$ : every value is positive by the theorem above. That every $y > 0$ is actually reached uses the completeness of the real numbers (an intermediate value argument); we take it from the construction of $\ln$ , as Mathlib does. A bijection has an inverse, and by definition that inverse is $\log_a$ .

∎

The graph of $y = \log_a x$ is therefore the reflection of the graph of $y = a^x$ in the line $y = x$ , as for every inverse function (see functions and their graphs).

Theorem— log₂ 3 is irrational

There are no integers $m, n$ with $n > 0$ and $\log_2 3 = \tfrac mn$ .

Proof

Suppose $\log_2 3 = \tfrac mn$ . Then $2^{m/n} = 3$ , so $2^m = 3^n$ . Since $3 > 1$ , $\log_2 3 > 0$ and so $m > 0$ . But $2^m$ is even and $3^n$ is odd, so they cannot be equal.

∎

ProofH

Exponential growth beats every polynomial

Theorem— Bernoulli's inequality

For every real $h \ge -1$ and every whole number $n$ : $(1 + h)^n \ge 1 + nh$ .

Proof

Induction on $n$ ; the case $n = 0$ reads $1 \ge 1$ . If $(1 + h)^n \ge 1 + nh$ , multiply by $1 + h \ge 0$ :

(1 + h)^{n + 1} \ge (1 + nh)(1 + h) = 1 + (n + 1)h + nh^2 \ge 1 + (n + 1)h.

∎

Theorem— Exponentials outgrow powers

Let $a > 1$ and let $k$ be a whole number. Then $\dfrac{a^n}{n^k}$ grows beyond every bound as $n \to \infty$ . In particular $a^n > n^k$ for all large enough $n$ .

Proof

Write $a = 1 + h$ with $h > 0$ . By the binomial theorem every term of $(1 + h)^n$ is positive, so for $n \ge k + 1$ , keeping just the term containing $h^{k+1}$ ,

a^n \ge \binom{n}{k+1} h^{k+1} = \frac{n(n-1)\cdots(n-k)}{(k+1)!}\, h^{k+1}.

If $n \ge 2(k + 1)$ , each factor $n - j$ with $j \le k$ is at least $\tfrac n2$ . So

\frac{a^n}{n^k} \ge \frac{(n/2)^{k+1} h^{k+1}}{(k+1)!\; n^k} = \frac{(h/2)^{k+1}}{(k+1)!}\cdot n,

a fixed positive number times $n$ , which grows beyond every bound.

∎

The crossover can come late. $2^n > n^{10}$ holds for $n = 1$ , fails for every $n$ from $2$ to $58$ , and holds for every $n \ge 59$ . Exponential growth is slow to start and then unstoppable.

Theorem— The limit defining e exists

The numbers $s_n = \left(1 + \tfrac1n\right)^n$ increase with $n$ and satisfy $2 \le s_n < 3$ . Hence they approach a limit $e$ with $2 < e < 3$ .

Proof

$s_n \ge 1 + n \cdot \tfrac1n = 2$ by Bernoulli's inequality. By the binomial theorem,

s_n = \sum_{k=0}^{n} \binom nk \frac{1}{n^k} = \sum_{k=0}^{n} \frac{1}{k!}\left(1 - \frac1n\right)\left(1 - \frac2n\right)\cdots\left(1 - \frac{k-1}{n}\right).

Each bracket grows when $n$ grows, and $s_{n+1}$ has one more (positive) term than $s_n$ . So $s_{n+1} > s_n$ . Each bracket is less than $1$ , so

s_n \le \sum_{k=0}^{n} \frac{1}{k!} \le 1 + 1 + \frac12 + \frac14 + \cdots + \frac{1}{2^{n-1}} < 3,

using $k! \ge 2^{k-1}$ . An increasing sequence that is bounded above has a limit; this is the completeness of the real numbers. The limit is at least $s_2 = \tfrac94 > 2$ . For the upper bound, $3! = 6$ is larger than $2^2 = 4$ , so the estimate above loses at least $\tfrac14 - \tfrac16 = \tfrac1{12}$ once $n \ge 3$ . Every $s_n$ is therefore at most $3 - \tfrac1{12}$ , and so is the limit.

∎

A refinement of the same argument shows $e = 1 + 1 + \tfrac1{2!} + \tfrac1{3!} + \cdots$ . More generally, compounding a rate $r$ ever more often gives $\left(1 + \tfrac rn\right)^n \to e^r$ . That is why continuous growth at rate $r$ is described by $e^{rt}$ .

Worked examplesH

Worked examples

Example— Simplifying with the laws

$8^{2/3} = \left(8^{1/3}\right)^2 = 2^2 = 4$ . Also $\dfrac{3^{5} \cdot 3^{-2}}{3^{4}} = 3^{5 - 2 - 4} = 3^{-1} = \tfrac13$ , and $\log_2 48 - \log_2 3 = \log_2 16 = 4$ .

Example— Solving an exponential equation

Solve $5 \cdot 3^x = 200$ . Divide by $5$ : $3^x = 40$ . Take logarithms: $x = \log_3 40 = \dfrac{\ln 40}{\ln 3} \approx 3.358$ . Check: $3^{3.358} \approx 40.0$ .

Example— Half-life

Iodine-131, used in medicine to treat thyroid disease, has a half-life of about $8$ days. Of an initial amount $A_0$ , after $t$ days there remains $A(t) = A_0 \left(\tfrac12\right)^{t/8}$ . When is only $10\%$ left? We need $\left(\tfrac12\right)^{t/8} = \tfrac1{10}$ , so $\tfrac t8 \ln \tfrac12 = \ln \tfrac1{10}$ and

t = 8 \cdot \frac{\ln 10}{\ln 2} \approx 26.6 \text{ days}.

Example— Doubling time

Savings growing by $5\%$ a year double when $1.05^t = 2$ , that is, after $t = \dfrac{\ln 2}{\ln 1.05} \approx 14.2$ years. Since $\ln(1 + r) \approx r$ for small $r$ , the doubling time is about $\dfrac{0.693}{r}$ . Bankers call this the rule of 70: at $5\%$ , about $70/5 = 14$ years.

Example— Logarithmic scales

Some quantities range over so many powers of ten that we measure them by their logarithms. Acidity is measured by $\mathrm{pH} = -\log_{10}[\mathrm{H}^+]$ , where $[\mathrm{H}^+]$ is the hydrogen-ion concentration in moles per litre. Lemon juice at pH $2$ has $10^{5}$ times the hydrogen-ion concentration of a solution at pH $7$ . A logarithmic scale turns "times $10$ " into "plus $1$ ".

Formal mathematicsF

The proofs, checked by Lean

The "laws force the definitions" theorem is proved for an arbitrary function E : ℝ → ℝ satisfying E (x + y) = E x * E y that is not identically zero. These are exactly parts 1–4 of the theorem:

law_zeroLean 4Proved here from basic factsFormally verified

/-- **Why `a⁰ = 1`.** If `E(x + y) = E(x)·E(y)` for all `x, y` and `E` is not the zero function,
then `E 0 = 1`: pick `x` with `E x ≠ 0`; then `E x = E(x + 0) = E x · E 0`, and cancelling the
non-zero number `E x` leaves `E 0 = 1`. -/
theorem law_zero (hadd : ∀ x y, E (x + y) = E x * E y) (hE : ∃ x, E x ≠ 0) : E 0 = 1 := by
  obtain ⟨x, hx⟩ := hE
  have h : E x * E 0 = E x * 1 := by rw [← hadd, add_zero, mul_one]
  exact mul_left_cancel₀ hx h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

law_negLean 4Proved here from basic factsFormally verified

/-- **Why `a⁻ˣ = 1/aˣ`.** `E(x)·E(−x) = E(x + (−x)) = E 0 = 1`, so `E(−x)` is the reciprocal of
`E(x)` (and in particular `E x` is never zero). -/
theorem law_neg (hadd : ∀ x y, E (x + y) = E x * E y) (hE : ∃ x, E x ≠ 0) (x : ℝ) :
    E (-x) = (E x)⁻¹ := by
  have h : E x * E (-x) = 1 := by rw [← hadd, add_neg_cancel, law_zero hadd hE]
  exact eq_inv_of_mul_eq_one_right h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

law_posLean 4Proved here from basic factsFormally verified

/-- **Powers of a positive base are positive.** `E x = E(x/2 + x/2) = E(x/2)² ≥ 0`, and
`E x ≠ 0` because `E x · E(−x) = 1`. So `E x > 0`. -/
theorem law_pos (hadd : ∀ x y, E (x + y) = E x * E y) (hE : ∃ x, E x ≠ 0) (x : ℝ) :
    0 < E x := by
  have hsq : E x = E (x / 2) * E (x / 2) := by rw [← hadd]; ring_nf
  have hne : E x ≠ 0 := by
    intro h0
    have h1 : E x * E (-x) = 1 := by rw [← hadd, add_neg_cancel, law_zero hadd hE]
    rw [h0, zero_mul] at h1
    exact zero_ne_one h1
  have hnn : 0 ≤ E x := by rw [hsq]; exact mul_self_nonneg _
  exact lt_of_le_of_ne hnn (Ne.symm hne)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

law_natLean 4Proved here from basic factsFormally verified

/-- **Whole-number multiples:** `E(n·x) = E(x)ⁿ`, by induction on `n`:
`E((n + 1)x) = E(nx + x) = E(x)ⁿ · E(x)`. -/
theorem law_nat (hadd : ∀ x y, E (x + y) = E x * E y) (hE : ∃ x, E x ≠ 0) (x : ℝ) (n : ℕ) :
    E (n * x) = E x ^ n := by
  induction n with
  | zero => simp [law_zero hadd hE]
  | succ n ih =>
    rw [Nat.cast_succ, add_mul, one_mul, hadd, ih, pow_succ]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

law_intLean 4Proved here from basic factsFormally verified

/-- **Integer multiples:** `E(n·x) = E(x)ⁿ` for every integer `n`, negative ones included,
combining `law_nat` with `law_neg`. -/
theorem law_int (hadd : ∀ x y, E (x + y) = E x * E y) (hE : ∃ x, E x ≠ 0) (x : ℝ) (n : ℤ) :
    E (n * x) = E x ^ n := by
  cases n with
  | ofNat m =>
    simp only [Int.ofNat_eq_natCast, Int.cast_natCast, zpow_natCast]
    exact law_nat hadd hE x m
  | negSucc m =>
    rw [Int.cast_negSucc, zpow_negSucc, neg_mul, law_neg hadd hE, ← law_nat hadd hE x (m + 1)]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

The last step compares E with Mathlib's real power a ^ x. At every rational number they agree, so the law alone determines all the rational exponents:

law_ratLean 4Proved here from basic factsFormally verified

/-- **The values at fractions are forced.** Let `a = E 1`. For every rational `q`, `E q` equals
Mathlib's real power `a ^ q`. Write `q = m/n` with `n > 0`: then `E(q)ⁿ = E(n·q) = E(m) = aᵐ`,
so `E q` is a positive `n`-th root of `aᵐ`. A positive number has only one positive `n`-th
root, and `a ^ q` is one, so the two agree. -/
theorem law_rat (hadd : ∀ x y, E (x + y) = E x * E y) (hE : ∃ x, E x ≠ 0) (q : ℚ) :
    E q = E 1 ^ (q : ℝ) := by
  have ha : 0 < E 1 := law_pos hadd hE 1
  have hn : (q.den : ℝ) ≠ 0 := by exact_mod_cast q.den_nz
  -- `E(q)ⁿ = aᵐ`
  have h1 : E q ^ q.den = E 1 ^ q.num := by
    rw [← law_nat hadd hE, ← law_int hadd hE, mul_one]
    congr 1
    exact_mod_cast q.den_mul_eq_num
  -- `(a ^ q)ⁿ = aᵐ`
  have h2 : (E 1 ^ (q : ℝ)) ^ q.den = E 1 ^ q.num := by
    rw [← Real.rpow_natCast, ← Real.rpow_mul ha.le, ← Real.rpow_intCast]
    congr 1
    exact_mod_cast q.mul_den_eq_num
  rw [← h2] at h1
  exact (pow_left_inj₀ (law_pos hadd hE q).le (Real.rpow_pos_of_pos ha _).le q.den_nz).mp h1

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

rpow_add_libraryLean 4Applies a library theoremFormally verified

/-- **The law of exponents for real powers:** `a^(x + y) = aˣ · aʸ` for `a > 0` and all real
`x, y`. This applies Mathlib's `Real.rpow_add`. So Mathlib's `x ↦ a ^ x` is a function `E` of the
kind studied above, and `law_rat` shows it is the *only* such function with `E 1 = a` at the
rationals. -/
theorem rpow_add_library {a : ℝ} (ha : 0 < a) (x y : ℝ) : a ^ (x + y) = a ^ x * a ^ y :=
  Real.rpow_add ha x y

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

exp_add_libraryLean 4Applies a library theoremFormally verified

/-- **`exp` turns addition into multiplication:** `e^(x + y) = eˣ · eʸ`. This applies
`Real.exp_add`. -/
theorem exp_add_library (x y : ℝ) : exp (x + y) = exp x * exp y :=
  Real.exp_add x y

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

The laws of logarithms, derived from the law for exp and the fact that exp is injective. The library version follows for comparison:

log_mul_from_expLean 4Proved here from basic factsFormally verified

/-- **The product law for logarithms**, derived from the exponential law. Both sides have the
same exponential — `exp(log x + log y) = exp(log x)·exp(log y) = xy = exp(log(xy))` — and `exp`
is injective, so they are equal. -/
theorem log_mul_from_exp {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
    log (x * y) = log x + log y := by
  apply Real.exp_injective
  rw [Real.exp_add, Real.exp_log hx, Real.exp_log hy, Real.exp_log (mul_pos hx hy)]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

log_rpow_from_expLean 4Proved here from basic factsFormally verified

/-- **The power law for logarithms:** `log(xʳ) = r·log x` for `x > 0`. Mathlib defines
`xʳ = exp(log x · r)`, so `exp(log(xʳ)) = xʳ = exp(r · log x)`; injectivity of `exp` finishes. -/
theorem log_rpow_from_exp {x : ℝ} (hx : 0 < x) (r : ℝ) : log (x ^ r) = r * log x := by
  apply Real.exp_injective
  rw [Real.exp_log (Real.rpow_pos_of_pos hx r), Real.rpow_def_of_pos hx, mul_comm]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

log_mul_libraryLean 4Applies a library theoremFormally verified

/-- The product law as stated in Mathlib, for all non-zero `x, y` (using `log |x|` for negative
numbers). This applies `Real.log_mul`. -/
theorem log_mul_library {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) : log (x * y) = log x + log y :=
  Real.log_mul hx hy

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

Exponentials as bijections, and an exponential equation solved exactly:

rpow_bijectiveLean 4Proved here from basic factsFormally verified

/-- **`x ↦ bˣ` is a bijection from `ℝ` onto `(0, ∞)`** for `b > 0`, `b ≠ 1`: every `y > 0` is
`bˣ` for exactly one `x`, namely `x = log_b y`. Existence is `Real.rpow_logb`; uniqueness:
if `b^x₁ = b^x₂`, take logarithms to get `x₁ log b = x₂ log b`, and `log b ≠ 0`. -/
theorem rpow_bijective {b : ℝ} (hb : 0 < b) (hb1 : b ≠ 1) {y : ℝ} (hy : 0 < y) :
    ∃! x : ℝ, b ^ x = y := by
  refine ⟨logb b y, Real.rpow_logb hb hb1 hy, ?_⟩
  intro x hx
  have hlogb : log b ≠ 0 := Real.log_ne_zero_of_pos_of_ne_one hb hb1
  have h : x * log b = log y := by rw [← log_rpow_from_exp hb x, hx]
  rw [Real.logb, ← h]
  field_simp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

solve_two_powLean 4Proved here from basic factsFormally verified

/-- **Solving an exponential equation:** `2ˣ = 10` has the solution `x = log 10 / log 2`
(about `3.32`). Indeed `2^(log 10 / log 2) = exp(log 2 · log 10 / log 2) = exp(log 10) = 10`. -/
theorem solve_two_pow : (2 : ℝ) ^ (log 10 / log 2) = 10 := by
  have h2 : log 2 ≠ 0 := by positivity
  rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 2), mul_div_cancel₀ _ h2,
    Real.exp_log (by norm_num)]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

The irrationality of $\log_2 3$ : first the statement about whole numbers, then the bridge from the real logarithm to it. Irrational x is Mathlib's notion: $x$ is not equal to any rational number.

two_pow_ne_three_powLean 4Proved here from basic factsFormally verified

/-- **No power of 2 is a power of 3** (except `2⁰ = 3⁰`): if `q ≥ 1` then `2ᵖ ≠ 3^q`.
A power of 3 is odd. A power of 2 is even unless `p = 0`, and then `2⁰ = 1 < 3 ≤ 3^q`. -/
theorem two_pow_ne_three_pow (p q : ℕ) (hq : 0 < q) : 2 ^ p ≠ 3 ^ q := by
  intro h
  have hodd : 3 ^ q % 2 = 1 := by
    rw [Nat.pow_mod]
    norm_num
  rcases Nat.eq_zero_or_pos p with rfl | hp
  · have : 3 ≤ 3 ^ q := Nat.le_self_pow (Nat.pos_iff_ne_zero.mp hq) 3
    simp at h
    omega
  · have heven : 2 ^ p % 2 = 0 := by
      obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.mp hp)
      rw [pow_succ, Nat.mul_mod_left]
    omega

Axioms used: propext, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

irrational_logb_two_threeLean 4Proved here from basic factsFormally verified

/-- **`log₂ 3` is irrational.** Suppose `log₂ 3 = m/n` with integers `m` and `n > 0`. Then
`2^(m/n) = 3`, so `2ᵐ = 3ⁿ`. Since `log₂ 3 > 0`, `m > 0`, and this contradicts
`two_pow_ne_three_pow`. -/
theorem irrational_logb_two_three : Irrational (logb 2 3) := by
  rintro ⟨q, hq⟩
  have hpos : 0 < logb 2 3 := Real.logb_pos (by norm_num) (by norm_num)
  have hq0 : (0 : ℝ) < q := hq ▸ hpos
  have hnum : 0 < q.num := Rat.num_pos.mpr (by exact_mod_cast hq0)
  -- `2 ^ q = 3`
  have h3 : (2 : ℝ) ^ (q : ℝ) = 3 := by
    rw [hq]; exact Real.rpow_logb (by norm_num) (by norm_num) (by norm_num)
  -- raise both sides to the power `n = q.den`
  have hpow : (2 : ℝ) ^ (q.num.toNat) = 3 ^ q.den := by
    have hm : ((q.num.toNat : ℕ) : ℝ) = (q : ℝ) * q.den := by
      have h1 : ((q.num.toNat : ℕ) : ℤ) = q.num := Int.toNat_of_nonneg hnum.le
      have h2 : ((q.num.toNat : ℕ) : ℝ) = (q.num : ℝ) := by exact_mod_cast h1
      rw [h2]
      exact_mod_cast q.mul_den_eq_num.symm
    rw [← h3, ← Real.rpow_natCast, ← Real.rpow_natCast, ← Real.rpow_mul (by norm_num), hm]
  have hnat : 2 ^ (q.num.toNat) = 3 ^ q.den := by exact_mod_cast hpow
  exact two_pow_ne_three_pow _ _ q.den_pos hnat

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

Growth. Bernoulli's inequality and two consequences are proved here. The general facts " $e^x$ beats every power" and " $(1 + t/n)^n \to e^t$ " are applied from Mathlib:

bernoulliLean 4Proved here from basic factsFormally verified

/-- **Bernoulli's inequality:** `(1 + h)ⁿ ≥ 1 + n h` for `h ≥ −1`. Induction on `n`:
`(1 + h)ⁿ⁺¹ = (1 + h)ⁿ(1 + h) ≥ (1 + nh)(1 + h) = 1 + (n + 1)h + nh² ≥ 1 + (n + 1)h`,
using `1 + h ≥ 0` in the first step. (Mathlib: `one_add_mul_le_pow`.) -/
theorem bernoulli {h : ℝ} (hh : -1 ≤ h) (n : ℕ) : 1 + n * h ≤ (1 + h) ^ n := by
  induction n with
  | zero => simp
  | succ n ih =>
    have h1 : 0 ≤ 1 + h := by linarith
    have hn : (0 : ℝ) ≤ n := Nat.cast_nonneg n
    calc 1 + ((n + 1 : ℕ) : ℝ) * h ≤ 1 + (n + 1) * h + n * h ^ 2 := by
          push_cast; nlinarith [sq_nonneg h]
      _ = (1 + n * h) * (1 + h) := by ring
      _ ≤ (1 + h) ^ n * (1 + h) := mul_le_mul_of_nonneg_right ih h1
      _ = (1 + h) ^ (n + 1) := by rw [pow_succ]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

e_ge_twoLean 4Proved here from basic factsFormally verified

/-- **A first estimate for e:** `(1 + 1/n)ⁿ ≥ 2` for every `n ≥ 1`, by Bernoulli's inequality
with `h = 1/n`: `(1 + 1/n)ⁿ ≥ 1 + n · (1/n) = 2`. -/
theorem e_ge_two (n : ℕ) (hn : 1 ≤ n) : 2 ≤ (1 + 1 / (n : ℝ)) ^ n := by
  have hpos : (0 : ℝ) < n := by exact_mod_cast hn
  have hh : (-1 : ℝ) ≤ 1 / n := by
    have : (0 : ℝ) ≤ 1 / n := by positivity
    linarith
  have h := bernoulli hh n
  have h1 : (n : ℝ) * (1 / n) = 1 := by field_simp
  linarith

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

sq_lt_two_powLean 4Proved here from basic factsFormally verified

/-- **Doubling beats squaring:** `n² < 2ⁿ` for every `n ≥ 5`. Induction: true at `n = 5`
(`25 < 32`); and if `n² < 2ⁿ` with `n ≥ 5`, then
`(n + 1)² = n² + 2n + 1 < n² + n² < 2ⁿ + 2ⁿ = 2ⁿ⁺¹`, because `2n + 1 < n²` once `n ≥ 3`. -/
theorem sq_lt_two_pow (n : ℕ) (hn : 5 ≤ n) : n ^ 2 < 2 ^ n := by
  induction n, hn using Nat.le_induction with
  | base => norm_num
  | succ n hn ih =>
    have h : 2 * n + 1 < n ^ 2 := by nlinarith
    calc (n + 1) ^ 2 = n ^ 2 + (2 * n + 1) := by ring
      _ < n ^ 2 + n ^ 2 := by omega
      _ < 2 ^ n + 2 ^ n := by omega
      _ = 2 ^ (n + 1) := by ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

exp_beats_powersLean 4Applies a library theoremFormally verified

/-- **The exponential function eventually exceeds every power:** `eˣ / xⁿ → ∞` as `x → ∞`, for
every natural number `n`. This applies Mathlib's `Real.tendsto_exp_div_pow_atTop`. -/
theorem exp_beats_powers (n : ℕ) : Tendsto (fun x : ℝ => exp x / x ^ n) atTop atTop :=
  Real.tendsto_exp_div_pow_atTop n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

compound_interest_limitLean 4Applies a library theoremFormally verified

/-- **Compound interest and e:** `(1 + t/n)ⁿ → eᵗ` as `n → ∞`; with `t = 1` this is
`(1 + 1/n)ⁿ → e`. This applies Mathlib's `Real.tendsto_one_add_div_pow_exp`. -/
theorem compound_interest_limit (t : ℝ) :
    Tendsto (fun n : ℕ => (1 + t / n) ^ n) atTop (𝓝 (exp t)) :=
  Real.tendsto_one_add_div_pow_exp t

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ExponentialLogarithmicFunctions.leanTry it in the Lean web editor

ComputationC

Racing exponentials, and watching e appear

Doubling against powers: when does 2^n win for good?PythonExact computationExhaustive finite checkComputationally tested

"""Doubling against powers: when does 2^n overtake n^k for good?

For each k we search for the last n with 2^n <= n^k, using exact integer
arithmetic. A finite search alone cannot show that 2^n stays ahead forever,
so we add the lesson's argument: going from n to n + 1 multiplies 2^n by 2 but
n^k only by (1 + 1/n)^k, which is less than 2 once n is large enough. If
2^n > n^k holds at some n beyond that point, it holds for every larger n.
"""

def ratio_below_two_from(k):
    """Least n >= 1 with (n + 1)^k < 2 n^k, i.e. (1 + 1/n)^k < 2 (exact).

    The ratio decreases as n grows, so it stays below 2 from then on.
    """
    n = 1
    while (n + 1) ** k >= 2 * n ** k:
        n += 1
    return n

def crossover(k):
    """Least N such that 2^n > n^k for every n >= N (proved, not just tested).

    Checks every n up to the point where the induction step takes over.
    """
    start = ratio_below_two_from(k)
    n = start
    while 2 ** n <= n ** k:  # find a point beyond `start` where 2^n is ahead
        n += 1
    last_failure = max((m for m in range(1, n) if 2 ** m <= m ** k), default=0)
    return last_failure + 1

def holds_from(k, big_n, upto):
    """Check 2^n > n^k for all n with big_n <= n <= upto (exact)."""
    return all(2 ** n > n ** k for n in range(big_n, upto + 1))

def folded_thickness_km(folds, sheet_mm=0.1):
    """Thickness in km of a sheet of `sheet_mm` mm after `folds` doublings."""
    return sheet_mm * 2 ** folds / 1_000_000

def main():
    print("When does 2^n beat n^k for good?  (exact integer arithmetic)")
    print("   k   2^n > n^k for all n >=   (1+1/n)^k < 2 for n >=")
    for k in (2, 3, 5, 10):
        big_n = crossover(k)
        print(f"  {k:2d}   {big_n:22d}   {ratio_below_two_from(k):22d}")
    n = crossover(10)
    print(f"  e.g. 2^{n - 1} = {2 ** (n - 1):,} <= {n - 1}^10 = "
          f"{(n - 1) ** 10:,}")
    print(f"       2^{n} = {2 ** n:,} >  {n}^10 = {n ** 10:,}")
    print("  re-check by brute force up to n = 1000:",
          all(holds_from(k, crossover(k), 1000) for k in (2, 3, 5, 10)))
    print()
    print("Why the table is a proof: from the right-hand column on, each step")
    print("multiplies 2^n by 2 but n^k by less than 2. So once 2^n is ahead")
    print("there, it stays ahead; the exact search covers all smaller n.")
    print()
    km = folded_thickness_km(42)
    print(f"A 0.1 mm sheet folded 42 times would be {km:,.0f} km thick,")
    print("more than the distance to the Moon (about 384,400 km).")
    print()
    print("Epistemic status: all comparisons are exact integer computations.")
    print("Together with the induction step they prove 2^n > n^k for every")
    print("n in the stated range, for these four values of k. The folding")
    print("figure is a calculation, not a feasible experiment.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

A finite search can never show that something holds forever. Here it is combined with an induction step. Once $(1 + 1/n)^k < 2$ , each step from $n$ to $n + 1$ doubles $2^n$ but multiplies $n^k$ by less than $2$ . So the search plus the argument is a complete proof for these values of $k$ .

Next, compound interest. Watch $\left(1 + \tfrac1n\right)^n$ creep towards $e$ , and compare it with the much faster series $\sum 1/k!$ :

Compound interest, the number e, and logarithm tablesPythonNumerical approximationExact computationComputationally tested

"""Compound interest and the number e.

A deposit of 1 at 100% annual interest, compounded n times a year, grows to
(1 + 1/n)^n after one year. As n grows this approaches e = 2.71828..., but
slowly: the error is close to e/(2n). The series 1 + 1 + 1/2! + 1/3! + ...
reaches the same number much faster. We also check that ln turns products
into sums, the idea behind Napier's logarithm tables.
"""

import math
from fractions import Fraction

def compound(n):
    """(1 + 1/n)^n, computed as exp(n * log1p(1/n)) to avoid rounding loss."""
    if n < 1:
        raise ValueError("n must be a positive integer")
    return math.exp(n * math.log1p(1 / n))

def compound_exact(n):
    """(1 + 1/n)^n as an exact fraction (use only for small n)."""
    return (1 + Fraction(1, n)) ** n

def series_partial_sum(terms):
    """1 + 1/1! + 1/2! + ... + 1/(terms - 1)! as an exact fraction."""
    total = Fraction(0)
    factorial = 1
    for k in range(terms):
        if k > 0:
            factorial *= k
        total += Fraction(1, factorial)
    return total

def main():
    print("1 deposited at 100% interest, compounded n times in one year:")
    print(f"{'n':>9}  {'(1 + 1/n)^n':>14}  {'e - value':>10}  {'n * error':>9}")
    for n in [1, 2, 4, 12, 365, 10 ** 4, 10 ** 6]:
        value = compound(n)
        err = math.e - value
        print(f"{n:9d}  {value:14.10f}  {err:10.3e}  {n * err:9.4f}")
    print(f"n * error approaches e/2 = {math.e / 2:.4f}: the error is about"
          " e/(2n).")
    print(f"exact check: (1 + 1/12)^12 = {compound_exact(12)}")
    print(f"           = {float(compound_exact(12)):.10f}")
    print()
    print("the series 1 + 1 + 1/2! + 1/3! + ... (exact fractions):")
    for terms in [3, 5, 8, 12, 16]:
        s = series_partial_sum(terms)
        print(f"  {terms:2d} terms: {float(s):.15f}   e - sum = "
              f"{math.e - float(s):.1e}")
    print()
    print("logarithm tables: ln(xy) = ln x + ln y")
    for x, y in [(2, 3), (7.5, 40), (0.125, 640)]:
        lhs, rhs = math.log(x * y), math.log(x) + math.log(y)
        print(f"  ln({x} * {y}) = {lhs:.12f},  ln {x} + ln {y} ="
              f" {rhs:.12f}")
    print()
    print("Epistemic status: numerical evidence in double-precision arithmetic")
    print("(about 16 significant digits); the e/(2n) pattern is an observed")
    print("estimate, consistent with a calculus argument we do not give here.")
    print("The limit itself is a theorem (in Lean via Mathlib), not something a")
    print("finite table can prove.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The pattern "error $\approx e/(2n)$ " is an observation from the numbers. The table makes it convincing but does not prove it, and calculus can.

Explore

Explore: exponentials, logarithms and e

Move the base $b$ . The curve $y = b^x$ always passes through $(0, 1)$ , and its reflection in $y = x$ , the logarithm $y = \log_b x$ , always passes through $(1, 0)$ . What happens as $b$ passes through $1$ ? Why is $b = 1$ excluded as a base?

An exponential and its inverse

Move the sliders and trace along the curves to read off values.

y = bˣ
y = log_b x
y = x

bb = 2

Trace along xx = 1

y = bˣ: y = 2
y = log_b x: y = 0
y = x: y = 1

Exponential against polynomial: $2^x$ and $x^3$ cross twice. Which is larger between the crossings, and which wins in the end?

Who wins the race?

Move the sliders and trace along the curves to read off values.

y = 2ˣ
y = x³

Trace along xx = 1

y = 2ˣ: y = 2
y = x³: y = 1

Finally, the sequence $\left(1 + \tfrac1n\right)^n$ approaching $e$ . Shrink $\varepsilon$ and see how large $n$ must be before every later term stays within $\varepsilon$ of $e$ :

Sequences and limits

Plot the terms aₙ and test a candidate limit with an ε-band: from some index on, every term must stay inside.

General term of the sequence

a_n =

term inside the band
term outside the band
band from L − ε to L + ε

Terms plottedN = 80Tolerance εε = 0.05

L =

a₈₀ = 2.701485

From n = 27 on, all of the first 2,000 terms lie within ε = 0.05 of L = 2.71828.

Evidence, not proof: a computer can check only finitely many terms. A proof must show |aₙ − L| < ε for every n ≥ N.

Exercises

1. Exponential and logarithmic functions

Warm-upHuman

Compute $2^{-3} \cdot 2^{5}$ .

2. Exponential and logarithmic functions

Warm-upHuman

Compute $\log_3 81$ .

3. Exponential and logarithmic functions

CoreHuman

Compute $16^{3/4}$ .

4. Exponential and logarithmic functions

CoreHuman

For $x > 0$ , which expression equals $\log_2(8x)$ ?

Choose one

3 + \log_2 x

3 \log_2 x

8 \log_2 x

\log_2 8 \cdot \log_2 x

5. Exponential and logarithmic functions

CoreHuman

Solve $5 \cdot 3^x = 200$ .

Choose one

x = \dfrac{\ln 40}{\ln 3} \approx 3.36

x = \dfrac{\ln 200}{\ln 15} \approx 1.96

x = \dfrac{40}{3}

x = \ln\dfrac{40}{3} \approx 2.59

6. Exponential and logarithmic functions

CoreHuman

A hospital receives $160$ mg of iodine-131, which has a half-life of $8$ days. How many milligrams remain after $24$ days?

7. Exponential and logarithmic functions

StretchHuman

In the proof that $\log_2 3$ is irrational we reach $2^m = 3^n$ with whole numbers $m \ge 1$ and $n \ge 1$ . Which of these facts would finish the proof? Choose all that apply.

Choose all that apply

2^m

is even but

3^n

is odd.By unique prime factorisation, a number greater than

1

cannot be both a power of

2

and a power of

3

3^n

grows faster than

2^m

\log_2 3

lies between

1

and

2

8. Exponential and logarithmic functions

CoreFormal

Let b : ℝ with 0 < b and b ≠ 1. Which Lean statement says that $x \mapsto b^x$ is a bijection from $\mathbb{R}$ onto $(0, \infty)$ ?

Choose one

∀ y : ℝ, 0 < y → ∃! x : ℝ, b ^ x = y∀ x : ℝ, ∃! y : ℝ, b ^ x = y∀ y : ℝ, ∃ x : ℝ, b ^ x = y∃! x : ℝ, ∀ y : ℝ, 0 < y → b ^ x = y

9. Exponential and logarithmic functions

StretchComputational

Savings grow by a rate $r$ per year (for example $r = 0.05$ for $5\%$ ). Write years_to_double(r), which returns the smallest whole number of years $n$ with $(1 + r)^n \ge 2$ , and doubling_time(r), which returns the exact doubling time $\dfrac{\ln 2}{\ln(1 + r)}$ using math.log.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

" $\log(x + y) = \log x + \log y$ ." The logarithm turns products into sums: $\log(xy) = \log x + \log y$ . There is no simple rule for $\log(x + y)$ . Test: $\log_{10}(10 + 10) = \log_{10} 20 \approx 1.30$ , but $\log_{10} 10 + \log_{10} 10 = 2$ .

Misconception

" $a^{-n}$ is negative." A negative exponent means a reciprocal, not a negative number: $2^{-3} = \tfrac18 > 0$ . For $a > 0$ , every power $a^x$ is positive, as the theorem above proves.

Misconception

Confusing exponential and linear growth. "Growing by $5$ per year" (add the same amount: linear) is very different from "growing by $5\%$ per year" (multiply by the same factor: exponential). In a table, linear growth has constant differences; exponential growth has constant ratios.

Misconception

"Exponential means fast." Exponential growth with a small rate is slow at first, and it can trail a polynomial for a long time: $1.01^n$ is smaller than $n$ for every $n$ from $2$ to $651$ . What makes it exponential is that it eventually overtakes every polynomial.

ViewpointsH

Many ways of seeing

Algebra— exp translates addition into multiplication

The law $e^{x + y} = e^x e^y$ says that $\exp$ is a structure-preserving map from the real numbers under addition, $(\R, +)$ , to the positive real numbers under multiplication, $(\R_{>0}, \times)$ . It is a bijection, and its inverse $\ln$ preserves structure too: $\ln(xy) = \ln x + \ln y$ . So $\exp$ is an isomorphism: the two structures are the same structure in different clothes. That is exactly why logarithm tables worked: to multiply two numbers, look up their logarithms, add, and look up the answer (see structure-preserving maps).

Number theory— Why a piano can never be perfectly in tune

A musical octave doubles a frequency, and a perfect fifth multiplies it by $\tfrac32$ . Could some number of fifths equal a whole number of octaves? That would mean $\left(\tfrac32\right)^q = 2^p$ , that is, $3^q = 2^{p + q}$ , which the parity argument forbids. Equivalently, $\log_2 \tfrac32$ is irrational. Twelve fifths overshoot seven octaves by the Pythagorean comma $\tfrac{3^{12}}{2^{19}} \approx 1.0136$ . Modern equal temperament compromises: its fifth is $2^{7/12} \approx 1.4983$ , slightly flat of $1.5$ .

Analysis— The function equal to its own slope

Analysts characterise $e^x$ in several equivalent ways: as the power series $\sum_k x^k/k!$ (which is how Mathlib defines it), as the limit of $\left(1 + \tfrac xn\right)^n$ , or as the unique function with $f' = f$ and $f(0) = 1$ . The last property says that the graph's slope at every point equals its height, which is what makes $e$ the natural base for calculus (see introductory calculus). Continuity really is needed in the "laws force the definitions" theorem. The equation $E(x + y) = E(x)E(y)$ also has wildly discontinuous solutions, whose construction (going back to Georg Hamel, 1905) needs the axiom of choice. Every continuous solution that is not identically zero is $a^x$ for $a = E(1)$ .

Physics— Why radioactive decay is exponential

Each unstable nucleus decays independently, with the same small probability per second, regardless of its age. So in each short time interval a fixed fraction of the remaining nuclei decays, and a fixed fraction lost per unit time is exactly exponential decay. Carbon-14 has a half-life of about $5730$ years. Willard Libby's radiocarbon dating (late 1940s) measures how much carbon-14 is left in once-living material to estimate its age. This is a model built on assumptions: steady production of carbon-14 in the past, which is corrected using calibration curves.

History & global context

History and global context

Adding exponents. In The Sand Reckoner (3rd century BCE), Archimedes noted that multiplying terms of a geometric progression corresponds to adding their positions. Jain mathematicians in India, for example in Vīrasena's Dhavalā commentary (9th century), worked with the ardhaccheda of a number, the number of times it can be halved, an idea akin to a base-2 logarithm. Michael Stifel's Arithmetica integra (1544) set the powers of $2$ , including negative exponents, beside their exponents.
Logarithms. John Napier published the first table of logarithms in 1614. Jost Bürgi computed a similar table independently and published it in 1620, and Henry Briggs produced base-10 tables (1617–1624). Logarithm tables and slide rules turned multiplication into addition for navigators, astronomers and engineers for more than three centuries, until electronic calculators replaced them in the 1970s.
The hyperbola and e. Grégoire de Saint-Vincent and Alphonse Antonio de Sarasa (1640s) noticed that areas under the hyperbola $y = 1/x$ behave like logarithms. Jacob Bernoulli met the limit $\left(1 + \tfrac1n\right)^n$ in 1683 while studying compound interest. Leonhard Euler named the number $e$ , gave its series and many of its properties in his Introductio in analysin infinitorum (1748), and Charles Hermite proved in 1873 that $e$ is transcendental.

Grains on a chessboard

Adding versus multiplying

Definitions

Why the definitions are forced

Exponential growth beats every polynomial

Worked examples

The proofs, checked by Lean

Racing exponentials, and watching e appear

Explore: exponentials, logarithms and e

Exercises

Common misconceptions

Many ways of seeing

History and global context

Further reading