def LogAxioms (L : ℝ → ℝ) : Prop

Proposition 5.4.1. There exists a unique function L : (0,∞) → ℝ such that (i) L 1 = 0; (ii) L is differentiable with derivative 1/x; (iii) L is strictly increasing, bijective, and L x → -∞ as x → 0⁺ while L x → ∞ as x → ∞; (iv) L (x*y) = L x + L y for x,y > 0; (v) for rational q and x > 0, L (x^q) = q * L x.

Equations

• One or more equations did not get rendered due to their size.

theorem log_satisfies_LogAxioms : LogAxioms Real.log

\log from mathlib satisfies the axioms characterizing the logarithm.

theorem logAxioms_eq_log_on_pos {L : ℝ → ℝ} (hL : LogAxioms L) {x : ℝ} (hx : 0 < x) : L x = Real.log x

theorem logAxioms_unique_on_pos {L₁ L₂ : ℝ → ℝ} (hL₁ : LogAxioms L₁) (hL₂ : LogAxioms L₂) {x : ℝ} (hx : 0 < x) : L₁ x = L₂ x

theorem exists_unique_log_function : ∃ (L : ℝ → ℝ), LogAxioms L ∧ ∀ (L' : ℝ → ℝ), LogAxioms L' → ∀ {x : ℝ}, 0 < x → L' x = L x

There exists a function (0,∞) → ℝ satisfying the logarithm axioms, unique on (0,∞).

def ExpAxioms (E : ℝ → ℝ) : Prop

Proposition 5.4.2. There exists a unique function E : ℝ → (0,∞) such that (i) E 0 = 1; (ii) E is differentiable with derivative E x; (iii) E is strictly increasing, bijective onto (0,∞), E x → 0 as x → -∞, and E x → ∞ as x → ∞; (iv) E (x + y) = E x * E y; (v) for rational q, E (q * x) = (E x)^q.

Equations

• One or more equations did not get rendered due to their size.

theorem exp_satisfies_ExpAxioms : ExpAxioms Real.exp

Real.exp satisfies the axioms characterizing the exponential.

theorem exists_unique_exp_function : ∃! E : ℝ → ℝ, ExpAxioms E

There exists a unique function ℝ → (0,∞) satisfying the exponential axioms.

theorem exp_mul_rpow (x y : ℝ) : Real.exp (x * y) = Real.exp x ^ y

Proposition 5.4.3. Let x, y ∈ ℝ. (i) exp (x*y) = (exp x)^y. (ii) If x > 0, then ln (x^y) = y * ln x.

theorem log_rpow_pos (x y : ℝ) (hx : 0 < x) : Real.log (x ^ y) = y * Real.log x

See Proposition 5.4.3 (ii). If x > 0, then ln (x^y) = y * ln x.