# Properties of the extended logarithm and exponential #

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

## Main DefinitionsP #

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

source
@[simp]
theorem EReal.log_exp (x : EReal) :
x.exp.log = x
source
@[simp]
theorem ENNReal.exp_log (x : ENNReal) :
x.log.exp = x
source
theorem EReal.exp_nmul (x : EReal) (n : ℕ) :
(↑n * x).exp = x.exp ^ n
source
theorem EReal.exp_mul (x : EReal) (y : ℝ) :
(x * ↑y).exp = x.exp ^ y
source
theorem EReal.ENNReal.rpow_eq_exp_mul_log (x : ENNReal) (y : ℝ) :
x ^ y = (↑y * x.log).exp
source
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 }

Instances For

source
@[simp]
theorem ENNReal.logOrderIso_apply (x : ENNReal) :
logOrderIso x = x.log
source
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

Instances For

source
@[simp]
theorem EReal.expOrderIso_apply (x : EReal) :
expOrderIso x = x.exp
source
@[simp]
theorem ENNReal.logOrderIso_symm :
logOrderIso.symm = EReal.expOrderIso
source
@[simp]
theorem EReal.expOrderIso_symm :
expOrderIso.symm = ENNReal.logOrderIso
source
noncomputable def ENNReal.logHomeomorph :
ENNReal ≃ₜ EReal

`log` as a homeomorphism.

Equations

- ENNReal.logHomeomorph = ENNReal.logOrderIso.toHomeomorph

Instances For

source
@[simp]
theorem ENNReal.logHomeomorph_apply (x : ENNReal) :
logHomeomorph x = x.log
source
noncomputable def EReal.expHomeomorph :
EReal ≃ₜ ENNReal

`exp` as a homeomorphism.

Equations

- EReal.expHomeomorph = EReal.expOrderIso.toHomeomorph

Instances For

source
@[simp]
theorem EReal.expHomeomorph_apply (x : EReal) :
expHomeomorph x = x.exp
source
@[simp]
theorem ENNReal.logHomeomorph_symm :
logHomeomorph.symm = EReal.expHomeomorph
source
@[simp]
theorem EReal.expHomeomorph_symm :
expHomeomorph.symm = ENNReal.logHomeomorph
source
theorem ENNReal.continuous_log :
Continuous log
source
theorem ENNReal.continuous_exp :
Continuous EReal.exp
source
theorem EReal.tendsto_exp_nhds_top_nhds_top :
Filter.Tendsto exp (nhds ⊤) (nhds ⊤)
source
theorem EReal.tendsto_exp_nhds_zero_nhds_one :
Filter.Tendsto exp (nhds 0) (nhds 1)
source
theorem EReal.tendsto_exp_nhds_bot_nhds_zero :
Filter.Tendsto exp (nhds ⊥) (nhds 0)
source
theorem ENNReal.tendsto_rpow_atTop_of_one_lt_base {b : ENNReal} (hb : 1 < b) :
Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atTop (nhds ⊤)
source
theorem ENNReal.tendsto_rpow_atTop_of_base_lt_one {b : ENNReal} (hb : b < 1) :
Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atTop (nhds 0)
source
theorem ENNReal.tendsto_rpow_atBot_of_one_lt_base {b : ENNReal} (hb : 1 < b) :
Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atBot (nhds 0)
source
theorem ENNReal.tendsto_rpow_atBot_of_base_lt_one {b : ENNReal} (hb : b < 1) :
Filter.Tendsto (fun (x : ℝ) => b ^ x) Filter.atBot (nhds ⊤)
source
theorem ENNReal.measurable_log :
Measurable log
source
theorem EReal.measurable_exp :
Measurable exp
source
theorem Measurable.ennreal_log {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ENNReal} (hf : Measurable f) :
Measurable fun (x : α) => (f x).log
source
theorem Measurable.ereal_exp {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → EReal} (hf : Measurable f) :
Measurable fun (x : α) => (f x).exp
source
instance instPolishSpaceEReal :
PolishSpace EReal