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
Instances For
    @[simp]
    theorem EReal.exp_bot :
    .exp = 0
    @[simp]
    @[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 #

    @[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