Documentation

Mathlib.Data.Complex.Exponential

Exponential Function #

This file contains the definitions of the real and complex exponential function.

theorem Complex.isCauSeq_abs_exp (z : ℂ) :

IsCauSeq abs fun (n : ℕ) => ∑ m ∈ Finset.range n, Complex.abs (z ^ m / ↑m.factorial)

theorem Complex.isCauSeq_exp (z : ℂ) :

IsCauSeq ⇑Complex.abs fun (n : ℕ) => ∑ m ∈ Finset.range n, z ^ m / ↑m.factorial

def Complex.exp' (z : ℂ) :

CauSeq ℂ ⇑Complex.abs

The Cauchy sequence consisting of partial sums of the Taylor series of the complex exponential function

Equations

Complex.exp' z = ⟨fun (n : ℕ) => ∑ m ∈ Finset.range n, z ^ m / ↑m.factorial, ⋯⟩

Instances For

def Complex.exp (z : ℂ) :

The complex exponential function, defined via its Taylor series

Equations

Complex.exp z = (Complex.exp' z).lim

Instances For

def Complex.termCexp :

Lean.ParserDescr

scoped notation for the complex exponential function

Equations

Complex.termCexp = Lean.ParserDescr.node `Complex.termCexp 1024 (Lean.ParserDescr.symbol "cexp")

Instances For

def Real.exp (x : ℝ) :

The real exponential function, defined as the real part of the complex exponential

Equations

Real.exp x = (Complex.exp ↑x).re

Instances For

def Real.termRexp :

Lean.ParserDescr

scoped notation for the real exponential function

Equations

Real.termRexp = Lean.ParserDescr.node `Real.termRexp 1024 (Lean.ParserDescr.symbol "rexp")

Instances For

@[simp]

theorem Complex.exp_zero :

Complex.exp 0 = 1

theorem Complex.exp_add (x y : ℂ) :

Complex.exp (x + y) = Complex.exp x * Complex.exp y

noncomputable def Complex.expMonoidHom :

Multiplicative ℂ →* ℂ

the exponential function as a monoid hom from Multiplicative ℂ to ℂ

Equations

Complex.expMonoidHom = { toFun := fun (z : Multiplicative ℂ) => Complex.exp (Multiplicative.toAdd z), map_one' := Complex.expMonoidHom.proof_1, map_mul' := Complex.expMonoidHom.proof_2 }

Instances For

@[simp]

theorem Complex.expMonoidHom_apply (z : Multiplicative ℂ) :

Complex.expMonoidHom z = Complex.exp (Multiplicative.toAdd z)

theorem Complex.exp_list_sum (l : List ℂ) :

Complex.exp l.sum = (List.map Complex.exp l).prod

theorem Complex.exp_multiset_sum (s : Multiset ℂ) :

Complex.exp s.sum = (Multiset.map Complex.exp s).prod

theorem Complex.exp_sum {α : Type u_1} (s : Finset α) (f : α → ℂ) :

Complex.exp (∑ x ∈ s, f x) = ∏ x ∈ s, Complex.exp (f x)

theorem Complex.exp_nsmul (x : ℂ) (n : ℕ) :

Complex.exp (n • x) = Complex.exp x ^ n

theorem Complex.exp_nat_mul (x : ℂ) (n : ℕ) :

Complex.exp (↑n * x) = Complex.exp x ^ n

@[simp]

theorem Complex.exp_ne_zero (x : ℂ) :

Complex.exp x ≠ 0

theorem Complex.exp_neg (x : ℂ) :

Complex.exp (-x) = (Complex.exp x)⁻¹

theorem Complex.exp_sub (x y : ℂ) :

Complex.exp (x - y) = Complex.exp x / Complex.exp y

theorem Complex.exp_int_mul (z : ℂ) (n : ℤ) :

Complex.exp (↑n * z) = Complex.exp z ^ n

@[simp]

theorem Complex.exp_conj (x : ℂ) :

Complex.exp ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.exp x)

@[simp]

theorem Complex.ofReal_exp_ofReal_re (x : ℝ) :

↑(Complex.exp ↑x).re = Complex.exp ↑x

@[simp]

theorem Complex.ofReal_exp (x : ℝ) :

↑(Real.exp x) = Complex.exp ↑x

@[simp]

theorem Complex.exp_ofReal_im (x : ℝ) :

(Complex.exp ↑x).im = 0

theorem Complex.exp_ofReal_re (x : ℝ) :

(Complex.exp ↑x).re = Real.exp x

@[simp]

theorem Real.exp_zero :

theorem Real.exp_add (x y : ℝ) :

Real.exp (x + y) = Real.exp x * Real.exp y

noncomputable def Real.expMonoidHom :

Multiplicative ℝ →* ℝ

the exponential function as a monoid hom from Multiplicative ℝ to ℝ

Equations

Real.expMonoidHom = { toFun := fun (x : Multiplicative ℝ) => Real.exp (Multiplicative.toAdd x), map_one' := Real.expMonoidHom.proof_1, map_mul' := Real.expMonoidHom.proof_2 }

Instances For

@[simp]

theorem Real.expMonoidHom_apply (x : Multiplicative ℝ) :

Real.expMonoidHom x = Real.exp (Multiplicative.toAdd x)

theorem Real.exp_list_sum (l : List ℝ) :

Real.exp l.sum = (List.map Real.exp l).prod

theorem Real.exp_multiset_sum (s : Multiset ℝ) :

Real.exp s.sum = (Multiset.map Real.exp s).prod

theorem Real.exp_sum {α : Type u_1} (s : Finset α) (f : α → ℝ) :

Real.exp (∑ x ∈ s, f x) = ∏ x ∈ s, Real.exp (f x)

theorem Real.exp_nsmul (x : ℝ) (n : ℕ) :

Real.exp (n • x) = Real.exp x ^ n

theorem Real.exp_nat_mul (x : ℝ) (n : ℕ) :

Real.exp (↑n * x) = Real.exp x ^ n

@[simp]

theorem Real.exp_ne_zero (x : ℝ) :

Real.exp x ≠ 0

theorem Real.exp_neg (x : ℝ) :

Real.exp (-x) = (Real.exp x)⁻¹

theorem Real.exp_sub (x y : ℝ) :

Real.exp (x - y) = Real.exp x / Real.exp y

theorem Real.sum_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) (n : ℕ) :

∑ i ∈ Finset.range n, x ^ i / ↑i.factorial ≤ Real.exp x

theorem Real.pow_div_factorial_le_exp (x : ℝ) (hx : 0 ≤ x) (n : ℕ) :

x ^ n / ↑n.factorial ≤ Real.exp x

theorem Real.quadratic_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) :

1 + x + x ^ 2 / 2 ≤ Real.exp x

theorem Real.one_le_exp {x : ℝ} (hx : 0 ≤ x) :

1 ≤ Real.exp x

theorem Real.exp_pos (x : ℝ) :

theorem Real.exp_nonneg (x : ℝ) :

0 ≤ Real.exp x

@[simp]

theorem Real.abs_exp (x : ℝ) :

|Real.exp x| = Real.exp x

theorem Real.exp_abs_le (x : ℝ) :

Real.exp |x| ≤ Real.exp x + Real.exp (-x)

theorem Real.exp_strictMono :

StrictMono Real.exp

theorem Real.exp_lt_exp_of_lt {x y : ℝ} (h : x < y) :

Real.exp x < Real.exp y

theorem Real.exp_monotone :

Monotone Real.exp

theorem Real.exp_le_exp_of_le {x y : ℝ} (h : x ≤ y) :

Real.exp x ≤ Real.exp y

@[simp]

theorem Real.exp_lt_exp {x y : ℝ} :

Real.exp x < Real.exp y ↔ x < y

@[simp]

theorem Real.exp_le_exp {x y : ℝ} :

Real.exp x ≤ Real.exp y ↔ x ≤ y

theorem Real.exp_injective :

Function.Injective Real.exp

@[simp]

theorem Real.exp_eq_exp {x y : ℝ} :

Real.exp x = Real.exp y ↔ x = y

@[simp]

theorem Real.exp_eq_one_iff (x : ℝ) :

Real.exp x = 1 ↔ x = 0

@[simp]

theorem Real.one_lt_exp_iff {x : ℝ} :

1 < Real.exp x ↔ 0 < x

@[simp]

theorem Real.exp_lt_one_iff {x : ℝ} :

Real.exp x < 1 ↔ x < 0

@[simp]

theorem Real.exp_le_one_iff {x : ℝ} :

Real.exp x ≤ 1 ↔ x ≤ 0

@[simp]

theorem Real.one_le_exp_iff {x : ℝ} :

1 ≤ Real.exp x ↔ 0 ≤ x

theorem Complex.sum_div_factorial_le {α : Type u_1} [LinearOrderedField α] (n j : ℕ) (hn : 0 < n) :

∑ m ∈ Finset.filter (fun (m : ℕ) => n ≤ m) (Finset.range j), 1 / ↑m.factorial ≤ ↑n.succ / (↑n.factorial * ↑n)

theorem Complex.exp_bound {x : ℂ} (hx : Complex.abs x ≤ 1) {n : ℕ} (hn : 0 < n) :

Complex.abs (Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial) ≤ Complex.abs x ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

theorem Complex.exp_bound' {x : ℂ} {n : ℕ} (hx : Complex.abs x / ↑n.succ ≤ 1 / 2) :

Complex.abs (Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial) ≤ Complex.abs x ^ n / ↑n.factorial * 2

theorem Complex.abs_exp_sub_one_le {x : ℂ} (hx : Complex.abs x ≤ 1) :

Complex.abs (Complex.exp x - 1) ≤ 2 * Complex.abs x

theorem Complex.abs_exp_sub_one_sub_id_le {x : ℂ} (hx : Complex.abs x ≤ 1) :

Complex.abs (Complex.exp x - 1 - x) ≤ Complex.abs x ^ 2

theorem Complex.abs_exp_sub_sum_le_exp_abs_sub_sum (x : ℂ) (n : ℕ) :

Complex.abs (Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial) ≤ Real.exp (Complex.abs x) - ∑ m ∈ Finset.range n, Complex.abs x ^ m / ↑m.factorial

theorem Complex.abs_exp_le_exp_abs (x : ℂ) :

Complex.abs (Complex.exp x) ≤ Real.exp (Complex.abs x)

theorem Complex.abs_exp_sub_sum_le_abs_mul_exp (x : ℂ) (n : ℕ) :

Complex.abs (Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial) ≤ Complex.abs x ^ n * Real.exp (Complex.abs x)

theorem Real.exp_bound {x : ℝ} (hx : |x| ≤ 1) {n : ℕ} (hn : 0 < n) :

|Real.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))

theorem Real.exp_bound' {x : ℝ} (h1 : 0 ≤ x) (h2 : x ≤ 1) {n : ℕ} (hn : 0 < n) :

Real.exp x ≤ ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

theorem Real.abs_exp_sub_one_le {x : ℝ} (hx : |x| ≤ 1) :

|Real.exp x - 1| ≤ 2 * |x|

theorem Real.abs_exp_sub_one_sub_id_le {x : ℝ} (hx : |x| ≤ 1) :

|Real.exp x - 1 - x| ≤ x ^ 2

noncomputable def Real.expNear (n : ℕ) (x r : ℝ) :

A finite initial segment of the exponential series, followed by an arbitrary tail. For fixed n this is just a linear map wrt r, and each map is a simple linear function of the previous (see expNear_succ), with expNear n x r ⟶ exp x as n ⟶ ∞, for any r.

Equations

Real.expNear n x r = ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial + x ^ n / ↑n.factorial * r

Instances For

@[simp]

theorem Real.expNear_zero (x r : ℝ) :

Real.expNear 0 x r = r

@[simp]

theorem Real.expNear_succ (n : ℕ) (x r : ℝ) :

Real.expNear (n + 1) x r = Real.expNear n x (1 + x / (↑n + 1) * r)

theorem Real.expNear_sub (n : ℕ) (x r₁ r₂ : ℝ) :

Real.expNear n x r₁ - Real.expNear n x r₂ = x ^ n / ↑n.factorial * (r₁ - r₂)

theorem Real.exp_approx_end (n m : ℕ) (x : ℝ) (e₁ : n + 1 = m) (h : |x| ≤ 1) :

|Real.exp x - Real.expNear m x 0| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)

theorem Real.exp_approx_succ {n : ℕ} {x a₁ b₁ : ℝ} (m : ℕ) (e₁ : n + 1 = m) (a₂ b₂ : ℝ) (e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂) (h : |Real.exp x - Real.expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂) :

|Real.exp x - Real.expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

theorem Real.exp_approx_end' {n : ℕ} {x a b : ℝ} (m : ℕ) (e₁ : n + 1 = m) (rm : ℝ) (er : ↑m = rm) (h : |x| ≤ 1) (e : |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm)) :

|Real.exp x - Real.expNear n x a| ≤ |x| ^ n / ↑n.factorial * b

theorem Real.exp_1_approx_succ_eq {n : ℕ} {a₁ b₁ : ℝ} {m : ℕ} (en : n + 1 = m) {rm : ℝ} (er : ↑m = rm) (h : |Real.exp 1 - Real.expNear m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / ↑m.factorial * (b₁ * rm)) :

|Real.exp 1 - Real.expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁

theorem Real.exp_approx_start (x a b : ℝ) (h : |Real.exp x - Real.expNear 0 x a| ≤ |x| ^ 0 / ↑(Nat.factorial 0) * b) :

|Real.exp x - a| ≤ b

theorem Real.exp_bound_div_one_sub_of_interval' {x : ℝ} (h1 : 0 < x) (h2 : x < 1) :

Real.exp x < 1 / (1 - x)

theorem Real.exp_bound_div_one_sub_of_interval {x : ℝ} (h1 : 0 ≤ x) (h2 : x < 1) :

Real.exp x ≤ 1 / (1 - x)

theorem Real.add_one_lt_exp {x : ℝ} (hx : x ≠ 0) :

x + 1 < Real.exp x

theorem Real.add_one_le_exp (x : ℝ) :

x + 1 ≤ Real.exp x

theorem Real.one_sub_lt_exp_neg {x : ℝ} (hx : x ≠ 0) :

1 - x < Real.exp (-x)

theorem Real.one_sub_le_exp_neg (x : ℝ) :

1 - x ≤ Real.exp (-x)

theorem Real.one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ ↑n) :

(1 - t / ↑n) ^ n ≤ Real.exp (-t)

theorem Real.le_inv_mul_exp (x : ℝ) {c : ℝ} (hc : 0 < c) :

x ≤ c⁻¹ * Real.exp (c * x)

def Mathlib.Meta.Positivity.evalExp :

Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: Real.exp is always positive.

Instances For

@[simp]

theorem Complex.abs_exp_ofReal (x : ℝ) :

Complex.abs (Complex.exp ↑x) = Real.exp x