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∞.
• ENNReal.log_orderIso, ENNReal.log_equiv: log seen respectively as an order isomorphism and an homeomorphism.

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 satisfy the identities log (x * y) = log x + log y and log (x ^ y) = y * log x (with either y ∈ ℕ or y ∈ ℝ).

TODO

• Define exp on EReal and prove its basic properties.

Tags

ENNReal, EReal, logarithm

Definition

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)

@[simp]

theorem ENNReal.log_zero : ENNReal.log 0 = ⊥

@[simp]

theorem ENNReal.log_one : ENNReal.log 1 = 0

@[simp]

theorem ENNReal.log_top : ⊤.log = ⊤

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

theorem ENNReal.log_strictMono : StrictMono ENNReal.log

theorem ENNReal.log_monotone : Monotone ENNReal.log

theorem ENNReal.log_injective : Function.Injective ENNReal.log

theorem ENNReal.log_surjective : Function.Surjective ENNReal.log

theorem ENNReal.log_bijective : Function.Bijective ENNReal.log

noncomputable def ENNReal.log_orderIso : ENNReal ≃o EReal

log as an order isomorphism.

Equations

• ENNReal.log_orderIso = StrictMono.orderIsoOfSurjective ENNReal.log ENNReal.log_strictMono ENNReal.log_surjective

@[simp]

theorem ENNReal.log_orderIso_apply (x : ENNReal) : ENNReal.log_orderIso x = x.log

@[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_iff_lt {x : ENNReal} {y : ENNReal} : x.log < y.log ↔ x < y

@[simp]

theorem ENNReal.log_bot_lt_iff {x : ENNReal} : ⊥ < x.log ↔ 0 < x

@[simp]

theorem ENNReal.log_lt_top_iff {x : ENNReal} : x.log < ⊤ ↔ x < ⊤

@[simp]

theorem ENNReal.log_lt_one_iff {x : ENNReal} : x.log < 0 ↔ x < 1

@[simp]

theorem ENNReal.log_one_lt_iff {x : ENNReal} : 0 < x.log ↔ 1 < x

@[simp]

theorem ENNReal.log_le_iff_le {x : ENNReal} {y : ENNReal} : x.log ≤ y.log ↔ x ≤ y

@[simp]

theorem ENNReal.log_le_one_iff (x : ENNReal) : x.log ≤ 0 ↔ x ≤ 1

@[simp]

theorem ENNReal.log_one_le_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

Topological properties

noncomputable def ENNReal.log_homeomorph : ENNReal ≃ₜ EReal

log as a homeomorphism.

Equations

• ENNReal.log_homeomorph = ENNReal.log_orderIso.toHomeomorph

@[simp]

theorem ENNReal.log_homeomorph_apply (x : ENNReal) : ENNReal.log_homeomorph x = x.log

theorem ENNReal.log_continuous : Continuous ENNReal.log