Documentation

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Extended Nonnegative Real Logarithm #

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

Main Definitions #

Main Results #

Tags #

ENNReal, EReal, logarithm

Definition #

noncomputable def ENNReal.log (x : ENNReal) :

The logarithm function defined on the extended nonnegative reals ℝ≥0∞ to the extended reals EReal. Coincides with the usual logarithm function and with Real.log on positive reals, and takes values log 0 = ⊥ and log ⊤ = ⊤. Conventions about multiplication in ℝ≥0∞ and addition in EReal make the identity log (x * y) = log x + log y unconditional.

Equations
Instances For
    @[simp]
    @[simp]
    theorem ENNReal.log_top :
    .log =
    @[simp]
    theorem ENNReal.log_ofReal (x : ) :
    (ENNReal.ofReal x).log = if x 0 then else (Real.log x)
    theorem ENNReal.log_ofReal_of_pos {x : } (hx : 0 < x) :
    (ENNReal.ofReal x).log = (Real.log x)
    theorem ENNReal.log_pos_real {x : ENNReal} (h : x 0) (h' : x ) :
    x.log = (Real.log x.toReal)
    theorem ENNReal.log_pos_real' {x : ENNReal} (h : 0 < x.toReal) :
    x.log = (Real.log x.toReal)
    theorem ENNReal.log_of_nnreal {x : NNReal} (h : x 0) :
    (↑x).log = (Real.log x)

    Monotonicity #

    @[simp]
    theorem ENNReal.log_eq_iff {x : ENNReal} {y : ENNReal} :
    x.log = y.log x = y
    @[simp]
    theorem ENNReal.log_eq_bot_iff {x : ENNReal} :
    x.log = x = 0
    @[simp]
    theorem ENNReal.log_eq_one_iff {x : ENNReal} :
    x.log = 0 x = 1
    @[simp]
    theorem ENNReal.log_eq_top_iff {x : ENNReal} :
    x.log = x =
    @[simp]
    theorem ENNReal.log_lt_log_iff {x : ENNReal} {y : ENNReal} :
    x.log < y.log x < y
    @[simp]
    theorem ENNReal.bot_lt_log_iff {x : ENNReal} :
    < x.log 0 < x
    @[simp]
    theorem ENNReal.log_lt_top_iff {x : ENNReal} :
    x.log < x <
    @[simp]
    theorem ENNReal.log_lt_zero_iff {x : ENNReal} :
    x.log < 0 x < 1
    @[simp]
    theorem ENNReal.zero_lt_log_iff {x : ENNReal} :
    0 < x.log 1 < x
    @[simp]
    theorem ENNReal.log_le_log_iff {x : ENNReal} {y : ENNReal} :
    x.log y.log x y
    @[simp]
    theorem ENNReal.log_le_zero_iff {x : ENNReal} :
    x.log 0 x 1
    @[simp]
    theorem ENNReal.zero_le_log_iff {x : ENNReal} :
    0 x.log 1 x

    Algebraic properties #

    theorem ENNReal.log_mul_add {x : ENNReal} {y : ENNReal} :
    (x * y).log = x.log + y.log
    theorem ENNReal.log_pow {x : ENNReal} {n : } :
    (x ^ n).log = n * x.log
    theorem ENNReal.log_rpow {x : ENNReal} {y : } :
    (x ^ y).log = y * x.log
    theorem ENNReal.log_inv {x : ENNReal} :
    x⁻¹.log = -x.log