Documentation

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

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

@[simp]

theorem EReal.log_exp (x : EReal) :

@[simp]

theorem ENNReal.exp_log (x : ENNReal) :

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 EReal.ENNReal.rpow_eq_exp_mul_log (x : ENNReal) (y : ℝ) :

x ^ y = (↑y * x.log).exp

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

@[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

Instances For

@[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

Instances For

@[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

Instances For

@[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 :

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 :

theorem EReal.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