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

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_1 }

@[simp]

theorem ENNReal.logOrderIso_apply (x : ENNReal) : 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) : EReal.expOrderIso x = x.exp

@[simp]

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

@[simp]

theorem EReal.expOrderIso_symm : EReal.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) : 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) : EReal.expHomeomorph x = x.exp

@[simp]

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

@[simp]

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

theorem ENNReal.continuous_log : Continuous ENNReal.log

theorem ENNReal.continuous_exp : Continuous EReal.exp

theorem ENNReal.measurable_log : Measurable ENNReal.log

theorem EReal.measurable_exp : Measurable EReal.exp

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

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

instance instPolishSpaceEReal : PolishSpace EReal

Equations

• instPolishSpaceEReal = ⋯