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∞
andEReal
defined bylog
andexp
.EReal.expOrderIso
: The order isomorphism betweenEReal
andℝ≥0∞
defined byexp
andlog
.ENNReal.logHomeomorph
:log
as a homeomorphism.EReal.expHomeomorph
:exp
as a homeomorphism.
Main Results #
EReal.log_exp
,ENNReal.exp_log
:log
andexp
are inverses of each other.EReal.exp_nmul
,EReal.exp_mul
:exp
satisfies the identitiesexp (n * x) = (exp x) ^ n
andexp (x * y) = (exp x) ^ y
.EReal
is a Polish space.
Tags #
ENNReal, EReal, logarithm, exponential
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
EReal.exp
and its inverse ENNReal.log
are an order isomorphism between EReal
and
ℝ≥0∞
.
Equations
Instances For
log
as a homeomorphism.
Instances For
exp
as a homeomorphism.
Instances For
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
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