# 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 #

source
noncomputable def EReal.exp :
EReal → ENNReal

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

Equations

- EReal.exp none = 0
- EReal.exp (some none) = ⊤
- EReal.exp (some (some x_1)) = ENNReal.ofReal (Real.exp x_1)

Instances For

source
@[simp]
theorem EReal.exp_bot :
⊥.exp = 0
source
@[simp]
theorem EReal.exp_zero :
exp 0 = 1
source
@[simp]
theorem EReal.exp_top :
⊤.exp = ⊤
source
@[simp]
theorem EReal.exp_coe (x : ℝ) :
(↑x).exp = ENNReal.ofReal (Real.exp x)
source
@[simp]
theorem EReal.exp_eq_zero_iff {x : EReal} :
x.exp = 0 ↔ x = ⊥
source
@[simp]
theorem EReal.exp_eq_top_iff {x : EReal} :
x.exp = ⊤ ↔ x = ⊤

### Monotonicity #

source
theorem EReal.exp_strictMono :
StrictMono exp
source
theorem EReal.exp_monotone :
Monotone exp
source
@[simp]
theorem EReal.exp_lt_exp_iff {a b : EReal} :
a.exp < b.exp ↔ a < b
source
@[simp]
theorem EReal.zero_lt_exp_iff {a : EReal} :
0 < a.exp ↔ ⊥ < a
source
@[simp]
theorem EReal.exp_lt_top_iff {a : EReal} :
a.exp < ⊤ ↔ a < ⊤
source
@[simp]
theorem EReal.exp_lt_one_iff {a : EReal} :
a.exp < 1 ↔ a < 0
source
@[simp]
theorem EReal.one_lt_exp_iff {a : EReal} :
1 < a.exp ↔ 0 < a
source
@[simp]
theorem EReal.exp_le_exp_iff {a b : EReal} :
a.exp ≤ b.exp ↔ a ≤ b
source
@[simp]
theorem EReal.exp_le_one_iff {a : EReal} :
a.exp ≤ 1 ↔ a ≤ 0
source
@[simp]
theorem EReal.one_le_exp_iff {a : EReal} :
1 ≤ a.exp ↔ 0 ≤ a
source
@[deprecated EReal.exp_monotone (since := "2025-10-20")]
theorem EReal.exp_le_exp {a b : EReal} (h : a ≤ b) :
a.exp ≤ b.exp
source
@[deprecated EReal.exp_strictMono (since := "2025-10-20")]
theorem EReal.exp_lt_exp {a b : EReal} (h : a < b) :
a.exp < b.exp

### Algebraic properties #

source
theorem EReal.exp_neg (x : EReal) :
(-x).exp = x.exp⁻¹
source
theorem EReal.exp_add (x y : EReal) :
(x + y).exp = x.exp * y.exp