Extended Nonnegative Real Exponential

We define exp as an extension of the exponential of a real to the extended reals EReal. The function takes values in the extended nonnegative reals ℝ≥0∞, with exp ⊥ = 0 and exp ⊤ = ⊤.

Main Definitions

• EReal.exp: The extension of the real exponential to EReal.

Main Results

• EReal.exp_strictMono: exp is increasing;
• EReal.exp_neg, EReal.exp_add: exp satisfies the identities exp (-x) = (exp x)⁻¹ and exp (x + y) = exp x * exp y.

Tags

ENNReal, EReal, exponential

Definition

noncomputable def EReal.exp : EReal → ENNReal

Exponential as a function from EReal to ℝ≥0∞.

Equations

• x.exp = match x with | none => 0 | some none => ⊤ | some (some x) => ENNReal.ofReal (Real.exp x)

@[simp]

theorem EReal.exp_bot : ⊥.exp = 0

@[simp]

theorem EReal.exp_zero : EReal.exp 0 = 1

@[simp]

theorem EReal.exp_top : ⊤.exp = ⊤

@[simp]

theorem EReal.exp_coe (x : ℝ) : (↑x).exp = ENNReal.ofReal (Real.exp x)

@[simp]

theorem EReal.exp_eq_zero_iff {x : EReal} : x.exp = 0 ↔ x = ⊥

@[simp]

theorem EReal.exp_eq_top_iff {x : EReal} : x.exp = ⊤ ↔ x = ⊤

Monotonicity

theorem EReal.exp_strictMono : StrictMono EReal.exp

theorem EReal.exp_monotone : Monotone EReal.exp

@[simp]

theorem EReal.exp_lt_exp_iff {a : EReal} {b : EReal} : a.exp < b.exp ↔ a < b

@[simp]

theorem EReal.zero_lt_exp_iff {a : EReal} : 0 < a.exp ↔ ⊥ < a

@[simp]

theorem EReal.exp_lt_top_iff {a : EReal} : a.exp < ⊤ ↔ a < ⊤

@[simp]

theorem EReal.exp_lt_one_iff {a : EReal} : a.exp < 1 ↔ a < 0

@[simp]

theorem EReal.one_lt_exp_iff {a : EReal} : 1 < a.exp ↔ 0 < a

@[simp]

theorem EReal.exp_le_exp_iff {a : EReal} {b : EReal} : a.exp ≤ b.exp ↔ a ≤ b

@[simp]

theorem EReal.exp_le_one_iff {a : EReal} : a.exp ≤ 1 ↔ a ≤ 0

@[simp]

theorem EReal.one_le_exp_iff {a : EReal} : 1 ≤ a.exp ↔ 0 ≤ a

Algebraic properties

theorem EReal.exp_neg (x : EReal) : (-x).exp = x.exp⁻¹

theorem EReal.exp_add (x : EReal) (y : EReal) : (x + y).exp = x.exp * y.exp