Verified rational bounds for the exponential

Rational lower and upper bounds for Real.exp are built from truncated Taylor series (expLb/expUb), shown to converge, and packaged into a ComputableℝSeq.exp. This yields IsComputable instances for Real.exp, Real.sinh, Real.cosh, and Real.tanh. The bound functions are executable; the packaged sequence mentions Real.exp itself as its reference value, so exp and the instances are noncomputable Lean terms.

def ComputableℝSeq.Exp.expLb₀ (x : ℚ) (n : ℕ) : ℚ

A valid lower bound when 0 ≤ x. Forms a CauSeq that converges to Real.exp x from below. Functions by dividing n by a constant k so that it's in the range [0,1], taking n terms of the Taylor expansion (which is an under-approximation), and then raising it to k again.

Equations

• ComputableℝSeq.Exp.expLb₀ x n = List.foldr (fun (n : ℕ) (v : ℚ) => 1 + x / ↑⌈x⌉.toNat * v / (↑n + 1)) 1 (List.range n) ^ ⌈x⌉.toNat

def ComputableℝSeq.Exp.expUb₀ (x : ℚ) (n : ℕ) : ℚ

A valid upper bound when 0 ≤ x. CauSeq that converges to Real.exp x from above.

Equations

• ComputableℝSeq.Exp.expUb₀ x n = (List.foldr (fun (n : ℕ) (v : ℚ) => 1 + x / ↑⌈x⌉.toNat * v / (↑n + 1)) 1 (List.range n) + 2 * (x / ↑⌈x⌉.toNat) ^ (n + 1) / ↑(n + 1).factorial) ^ ⌈x⌉.toNat

theorem ComputableℝSeq.Exp.List_foldr_eq_finset_sum (x : ℚ) (n : ℕ) : List.foldr (fun (n : ℕ) (v : ℚ) => 1 + x * v / (↑n + 1)) 1 (List.range n) = ∑ i ∈ Finset.range (n + 1), x ^ i / ↑i.factorial

theorem ComputableℝSeq.Exp.expLb₀_pos {x : ℚ} (n : ℕ) (hx : 0 ≤ x) : 0 < expLb₀ x n

theorem ComputableℝSeq.Exp.expLb₀_ge_one {x : ℚ} (n : ℕ) (hx : 0 ≤ x) : 1 ≤ expLb₀ x n

theorem ComputableℝSeq.Exp.expLb₀_le_exp {x : ℚ} (n : ℕ) (hx : 0 ≤ x) : ↑(expLb₀ x n) ≤ Real.exp ↑x

theorem ComputableℝSeq.Exp.expUb₀_ge_exp (x : ℚ) (n : ℕ) (hx : 0 ≤ x) : Real.exp ↑x ≤ ↑(expUb₀ x n)

theorem Real.one_plus_pow_lt_exp_mul {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : (1 + x) ^ y < exp (x * y)

theorem ComputableℝSeq.Exp.expUb₀_sub_expLb₀ {x : ℚ} (n : ℕ) (hx : 0 ≤ x) : ↑(expUb₀ x n) - ↑(expLb₀ x n) ≤ Real.exp ↑x * (Real.exp (2 * ↑x / ↑n.factorial) - 1)

This proves that the gap between expLb₀ and expUb₀ shrinks at least as fast as exp x * (exp (2x/n!) - 1). This is then used to prove that they are cauchy sequences in n, i.e. taking sufficiently large n makes this go to zero.

def ComputableℝSeq.Exp.expLb (x : ℚ) : ℕ → ℚ

Unlike expLb₀, which only works for 0 ≤ x, this is valid for all x.

Equations

• ComputableℝSeq.Exp.expLb x = if 0 ≤ x then ComputableℝSeq.Exp.expLb₀ x else fun (n : ℕ) => (ComputableℝSeq.Exp.expUb₀ (-x) n)⁻¹

def ComputableℝSeq.Exp.expUb (x : ℚ) : ℕ → ℚ

Unlike expUb₀, which only works for 0 ≤ x, this is valid for all x.

Equations

• ComputableℝSeq.Exp.expUb x = if 0 ≤ x then ComputableℝSeq.Exp.expUb₀ x else fun (n : ℕ) => (ComputableℝSeq.Exp.expLb₀ (-x) n)⁻¹

theorem ComputableℝSeq.Exp.expLb_le_exp (x : ℚ) (n : ℕ) : ↑(expLb x n) ≤ Real.exp ↑x

theorem ComputableℝSeq.Exp.expUb_ge_exp (x : ℚ) (n : ℕ) : Real.exp ↑x ≤ ↑(expUb x n)

theorem ComputableℝSeq.Exp.expUb_sub_expLb_of_nonneg {x : ℚ} (n : ℕ) (hx : 0 ≤ x) : ↑(expUb x n) - ↑(expLb x n) ≤ Real.exp ↑x * (Real.exp (2 * ↑x / ↑n.factorial) - 1)

theorem ComputableℝSeq.Exp.expUb_sub_expLb_of_neg {x : ℚ} (n : ℕ) (hx : x < 0) : ↑(expUb x n) - ↑(expLb x n) ≤ Real.exp (2 * ↑(-x) / ↑n.factorial) - 1

theorem ComputableℝSeq.Exp.expUb_lb_err (x : ℚ) (n : ℕ) : Real.exp ↑x ≤ ↑(expLb x n) + Real.exp ↑|x| * (Real.exp (2 * ↑|x| / ↑n.factorial) - 1) ∧ ↑(expUb x n) - Real.exp ↑|x| * (Real.exp (2 * ↑|x| / ↑n.factorial) - 1) ≤ Real.exp ↑x

theorem ComputableℝSeq.Exp.TLUW_lb_ub : TendstoLocallyUniformlyWithout (fun (n : ℕ) (x : ℚ) => expLb x n) Real.exp ∧ TendstoLocallyUniformlyWithout (fun (n : ℕ) (x : ℚ) => expUb x n) Real.exp

noncomputable def ComputableℝSeq.exp : ComputableℝSeq → ComputableℝSeq

Definition of exp.

Equations

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

@[implicit_reducible]

noncomputable instance IsComputable.instComputableExp (x : ℝ) [hx : IsComputable x] : IsComputable (Real.exp x)

Equations

• IsComputable.instComputableExp x = IsComputable.lift Real.exp ComputableℝSeq.exp IsComputable.instComputableExp._proof_1 hx

@[implicit_reducible]

noncomputable instance IsComputable.instComputableSinh (x : ℝ) [hx : IsComputable x] : IsComputable (Real.sinh x)

Equations

• IsComputable.instComputableSinh x = IsComputable.liftEq ⋯ inferInstance

@[implicit_reducible]

noncomputable instance IsComputable.instComputableCosh (x : ℝ) [hx : IsComputable x] : IsComputable (Real.cosh x)

Equations

• IsComputable.instComputableCosh x = IsComputable.liftEq ⋯ inferInstance

@[implicit_reducible]

noncomputable instance IsComputable.instComputableTanh (x : ℝ) [hx : IsComputable x] : IsComputable (Real.tanh x)

Equations

• IsComputable.instComputableTanh x = IsComputable.liftEq ⋯ inferInstance