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 #

source
noncomputable def ENNReal.log (x : ENNReal) :
EReal

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
    source
    @[simp]
    theorem ENNReal.log_zero :
    log 0 = ⊥
    source
    @[simp]
    theorem ENNReal.log_one :
    log 1 = 0
    source
    @[simp]
    theorem ENNReal.log_top :
    ⊤.log = ⊤
    source
    @[simp]
    theorem ENNReal.log_ofReal (x : ℝ) :
    (ENNReal.ofReal x).log = if x ≤ 0 then ⊥ else ↑(Real.log x)
    source
    theorem ENNReal.log_ofReal_of_pos {x : ℝ} (hx : 0 < x) :
    (ENNReal.ofReal x).log = ↑(Real.log x)
    source
    theorem ENNReal.log_pos_real {x : ENNReal} (h : x ≠ 0) (h' : x ≠ ⊤) :
    x.log = ↑(Real.log x.toReal)
    source
    theorem ENNReal.log_pos_real' {x : ENNReal} (h : 0 < x.toReal) :
    x.log = ↑(Real.log x.toReal)
    source
    theorem ENNReal.log_of_nnreal {x : NNReal} (h : x ≠ 0) :
    (↑x).log = ↑(Real.log ↑x)

    Monotonicity #

    source
    theorem ENNReal.log_strictMono :
    StrictMono log
    source
    theorem ENNReal.log_monotone :
    Monotone log
    source
    theorem ENNReal.log_injective :
    Function.Injective log
    source
    theorem ENNReal.log_surjective :
    Function.Surjective log
    source
    theorem ENNReal.log_bijective :
    Function.Bijective log
    source
    @[simp]
    theorem ENNReal.log_eq_iff {x y : ENNReal} :
    x.log = y.log ↔ x = y
    source
    @[simp]
    theorem ENNReal.log_eq_bot_iff {x : ENNReal} :
    x.log = ⊥ ↔ x = 0
    source
    @[simp]
    theorem ENNReal.log_eq_one_iff {x : ENNReal} :
    x.log = 0 ↔ x = 1
    source
    @[simp]
    theorem ENNReal.log_eq_top_iff {x : ENNReal} :
    x.log = ⊤ ↔ x = ⊤
    source
    @[simp]
    theorem ENNReal.log_lt_log_iff {x y : ENNReal} :
    x.log < y.log ↔ x < y
    source
    @[simp]
    theorem ENNReal.bot_lt_log_iff {x : ENNReal} :
    ⊥ < x.log ↔ 0 < x
    source
    @[simp]
    theorem ENNReal.log_lt_top_iff {x : ENNReal} :
    x.log < ⊤ ↔ x < ⊤
    source
    @[simp]
    theorem ENNReal.log_lt_zero_iff {x : ENNReal} :
    x.log < 0 ↔ x < 1
    source
    @[simp]
    theorem ENNReal.zero_lt_log_iff {x : ENNReal} :
    0 < x.log ↔ 1 < x
    source
    @[simp]
    theorem ENNReal.log_le_log_iff {x y : ENNReal} :
    x.log ≤ y.log ↔ x ≤ y
    source
    @[simp]
    theorem ENNReal.log_le_zero_iff {x : ENNReal} :
    x.log ≤ 0 ↔ x ≤ 1
    source
    @[simp]
    theorem ENNReal.zero_le_log_iff {x : ENNReal} :
    0 ≤ x.log ↔ 1 ≤ x
    source
    theorem ENNReal.log_le_log {x y : ENNReal} (h : x ≤ y) :
    x.log ≤ y.log
    source
    theorem ENNReal.log_lt_log {x y : ENNReal} (h : x < y) :
    x.log < y.log

    Algebraic properties #

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