Properties of the extended logarithm and exponential

We prove that log and exp define order isomorphisms between ℝ≥0∞ and EReal.

Main Definitions

• ENNReal.logOrderIso: The order isomorphism between ℝ≥0∞ and EReal defined by log and exp.
• EReal.expOrderIso: The order isomorphism between EReal and ℝ≥0∞ defined by exp and log.
• ENNReal.logHomeomorph: log as a homeomorphism.
• EReal.expHomeomorph: exp as a homeomorphism.

Main Results

• EReal.log_exp, ENNReal.exp_log: log and exp are inverses of each other.
• EReal.exp_nmul, EReal.exp_mul: exp satisfies the identities exp (n * x) = (exp x) ^ n and exp (x * y) = (exp x) ^ y.
• EReal is a Polish space.

Tags

ENNReal, EReal, logarithm, exponential

@[simp]

theorem EReal.log_exp (x : EReal) : x.exp.log = x

@[simp]

theorem ENNReal.exp_log (x : ENNReal) : x.log.exp = x

theorem EReal.exp_nmul (x : EReal) (n : ℕ) : (↑n * x).exp = x.exp ^ n

theorem EReal.exp_mul (x : EReal) (y : ℝ) : (x * ↑y).exp = x.exp ^ y

theorem ENNReal.rpow_eq_exp_mul_log (x : ENNReal) (y : ℝ) : x ^ y = (↑y * x.log).exp

@[deprecated ENNReal.rpow_eq_exp_mul_log (since := "2026-07-15")]

theorem EReal.ENNReal.rpow_eq_exp_mul_log (x : ENNReal) (y : ℝ) : x ^ y = (↑y * x.log).exp

Alias of ENNReal.rpow_eq_exp_mul_log.

noncomputable def ENNReal.logOrderIso : ENNReal ≃o EReal

ENNReal.log and its inverse EReal.exp are an order isomorphism between ℝ≥0∞ and EReal.

Equations

• ENNReal.logOrderIso = { toFun := ENNReal.log, invFun := EReal.exp, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := @ENNReal.logOrderIso._proof_3 }

@[simp]

theorem ENNReal.logOrderIso_apply (x : ENNReal) : logOrderIso x = x.log

noncomputable def EReal.expOrderIso : EReal ≃o ENNReal

EReal.exp and its inverse ENNReal.log are an order isomorphism between EReal and ℝ≥0∞.

Equations

• EReal.expOrderIso = ENNReal.logOrderIso.symm

@[simp]

theorem EReal.expOrderIso_apply (x : EReal) : expOrderIso x = x.exp

@[simp]

theorem ENNReal.logOrderIso_symm : logOrderIso.symm = EReal.expOrderIso

@[simp]

theorem EReal.expOrderIso_symm : expOrderIso.symm = ENNReal.logOrderIso

noncomputable def ENNReal.logHomeomorph : ENNReal ≃ₜ EReal

log as a homeomorphism.

Equations

• ENNReal.logHomeomorph = ENNReal.logOrderIso.toHomeomorph

@[simp]

theorem ENNReal.logHomeomorph_apply (x : ENNReal) : logHomeomorph x = x.log

noncomputable def EReal.expHomeomorph : EReal ≃ₜ ENNReal

exp as a homeomorphism.

Equations

• EReal.expHomeomorph = EReal.expOrderIso.toHomeomorph

@[simp]

theorem EReal.expHomeomorph_apply (x : EReal) : expHomeomorph x = x.exp

@[simp]

theorem ENNReal.logHomeomorph_symm : logHomeomorph.symm = EReal.expHomeomorph

@[simp]

theorem EReal.expHomeomorph_symm : expHomeomorph.symm = ENNReal.logHomeomorph

theorem ENNReal.continuous_log : Continuous log

theorem ENNReal.continuous_exp : Continuous EReal.exp

theorem EReal.tendsto_exp_nhds_top_nhds_top : Filter.Tendsto exp (nhds ⊤) (nhds ⊤)

theorem EReal.tendsto_exp_nhds_zero_nhds_one : Filter.Tendsto exp (nhds 0) (nhds 1)

theorem EReal.tendsto_exp_nhds_bot_nhds_zero : Filter.Tendsto exp (nhds ⊥) (nhds 0)

theorem ENNReal.tendsto_rpow_atTop_of_one_lt_base {b : ENNReal} (hb : 1 < b) : Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atTop (nhds ⊤)

theorem ENNReal.tendsto_rpow_atTop_of_base_lt_one {b : ENNReal} (hb : b < 1) : Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atTop (nhds 0)

theorem ENNReal.tendsto_rpow_atBot_of_one_lt_base {b : ENNReal} (hb : 1 < b) : Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atBot (nhds 0)

theorem ENNReal.tendsto_rpow_atBot_of_base_lt_one {b : ENNReal} (hb : b < 1) : Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atBot (nhds ⊤)

theorem ENNReal.measurable_log : Measurable log

theorem EReal.measurable_exp : Measurable exp

theorem Measurable.ennreal_log {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ENNReal} (hf : Measurable f) : Measurable fun (x : α) => (f x).log

theorem Measurable.ereal_exp {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → EReal} (hf : Measurable f) : Measurable fun (x : α) => (f x).exp

instance instPolishSpaceEReal : PolishSpace EReal