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

- `ENNReal.log`: The extension of the real logarithm to `ℝ≥0∞`.

## Main Results #

- `ENNReal.log_strictMono`: `log` is increasing;
- `ENNReal.log_injective`, `ENNReal.log_surjective`, `ENNReal.log_bijective`: `log` is injective, surjective, and bijective;
- `ENNReal.log_mul_add`, `ENNReal.log_pow`, `ENNReal.log_rpow`: `log` satisfies the identities `log (x * y) = log x + log y` and `log (x ^ y) = y * log x` (with either `y ∈ ℕ` or `y ∈ ℝ`).

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

- x.log = if x = 0 then ⊥ else if x = ⊤ then ⊤ else ↑(Real.log x.toReal)

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