Documentation

Mathlib.Analysis.SpecialFunctions.Log.ERealExp

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 #

Main Results #

Tags #

ENNReal, EReal, exponential

Definition #

noncomputable def EReal.exp :

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

Equations
@[simp]
theorem EReal.exp_bot :
@[simp]
theorem EReal.exp_zero :
exp 0 = 1
@[simp]
@[simp]
theorem EReal.exp_coe (x : ) :
@[simp]
theorem EReal.exp_eq_zero_iff {x : EReal} :
x.exp = 0 x =
@[simp]
theorem EReal.exp_eq_top_iff {x : EReal} :

Monotonicity #

@[simp]
theorem EReal.exp_lt_exp_iff {a 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} :
@[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 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) :
theorem EReal.exp_add (x y : EReal) :
(x + y).exp = x.exp * y.exp