Documentation

Mathlib.Data.EReal.Basic

The extended real numbers #

This file defines EReal, ℝ with a top element ⊤ and a bottom element ⊥, implemented as WithBot (WithTop ℝ).

EReal is a CompleteLinearOrder, deduced by typeclass inference from the fact that WithBot (WithTop L) completes a conditionally complete linear order L.

Coercions from ℝ (called coe in lemmas) and from ℝ≥0∞ (coe_ennreal) are registered and their basic properties proved. The latter takes up most of the rest of this file.

Tags #

real, ereal, complete lattice

def EReal :

The type of extended real numbers [-∞, ∞], constructed as WithBot (WithTop ℝ).

Equations

EReal = WithBot (WithTop ℝ)

Instances For

instance instERealBot :

Equations

instERealBot = WithBot.bot

instance instERealZero :

Equations

instERealZero = WithBot.zero

instance instERealOne :

Equations

instERealOne = WithBot.one

instance instERealNontrivial :

Nontrivial EReal

Equations

instERealNontrivial = ⋯

instance instERealAddMonoid :

AddMonoid EReal

Equations

instERealAddMonoid = WithBot.addMonoid

instance instERealPartialOrder :

PartialOrder EReal

Equations

instERealPartialOrder = WithBot.partialOrder

instance instERealAddCommMonoid :

AddCommMonoid EReal

Equations

instERealAddCommMonoid = WithBot.addCommMonoid

instance instZeroLEOneClassEReal :

ZeroLEOneClass EReal

instance instSupSetEReal :

Equations

instSupSetEReal = inferInstanceAs (SupSet (WithBot (WithTop ℝ)))

instance instInfSetEReal :

Equations

instInfSetEReal = inferInstanceAs (InfSet (WithBot (WithTop ℝ)))

instance instCompleteLinearOrderEReal :

CompleteLinearOrder EReal

Equations

instCompleteLinearOrderEReal = inferInstanceAs (CompleteLinearOrder (WithBot (WithTop ℝ)))

instance instLinearOrderEReal :

LinearOrder EReal

Equations

instLinearOrderEReal = inferInstanceAs (LinearOrder (WithBot (WithTop ℝ)))

instance instIsOrderedAddMonoidEReal :

IsOrderedAddMonoid EReal

instance instAddCommMonoidWithOneEReal :

AddCommMonoidWithOne EReal

Equations

instAddCommMonoidWithOneEReal = inferInstanceAs (AddCommMonoidWithOne (WithBot (WithTop ℝ)))

instance instDenselyOrderedEReal :

DenselyOrdered EReal

instance instCharZeroEReal :

def Real.toEReal :

The canonical inclusion from reals to ereals. Registered as a coercion.

Equations

Real.toEReal = WithBot.some ∘ WithTop.some

Instances For

instance EReal.decidableLT :

DecidableLT EReal

Equations

EReal.decidableLT = WithBot.decidableLT

instance EReal.instTop :

Equations

EReal.instTop = { top := ↑⊤ }

instance EReal.instCoeReal :

Equations

EReal.instCoeReal = { coe := Real.toEReal }

theorem EReal.coe_strictMono :

StrictMono Real.toEReal

theorem EReal.coe_injective :

Function.Injective Real.toEReal

@[simp]

theorem EReal.coe_le_coe_iff {x y : ℝ} :

↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem EReal.coe_lt_coe_iff {x y : ℝ} :

↑x < ↑y ↔ x < y

@[simp]

theorem EReal.coe_eq_coe_iff {x y : ℝ} :

↑x = ↑y ↔ x = y

theorem EReal.coe_ne_coe_iff {x y : ℝ} :

↑x ≠ ↑y ↔ x ≠ y

def ENNReal.toEReal :

ENNReal → EReal

The canonical map from nonnegative extended reals to extended reals.

Equations

↑none = ⊤
↑(some x_1) = ↑↑x_1

Instances For

instance EReal.hasCoeENNReal :

Coe ENNReal EReal

Equations

EReal.hasCoeENNReal = { coe := ENNReal.toEReal }

instance EReal.instInhabited :

Inhabited EReal

Equations

EReal.instInhabited = { default := 0 }

@[simp]

theorem EReal.coe_zero :

↑0 = 0

@[simp]

theorem EReal.coe_one :

↑1 = 1

def EReal.rec {motive : EReal → Sort u_1} (bot : motive ⊥) (coe : (a : ℝ) → motive ↑a) (top : motive ⊤) (a : EReal) :

motive a

A recursor for EReal in terms of the coercion.

When working in term mode, note that pattern matching can be used directly.

Equations

EReal.rec bot coe top none = bot
EReal.rec bot coe top (some (some a)) = coe a
EReal.rec bot coe top (some none) = top

Instances For

theorem EReal.forall {p : EReal → Prop} :

(∀ (r : EReal), p r) ↔ p ⊥ ∧ p ⊤ ∧ ∀ (r : ℝ), p ↑r

theorem EReal.exists {p : EReal → Prop} :

(∃ (r : EReal), p r) ↔ p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p ↑r

def EReal.mul :

EReal → EReal → EReal

The multiplication on EReal. Our definition satisfies 0 * x = x * 0 = 0 for any x, and picks the only sensible value elsewhere.

Equations

EReal.mul none none = ⊤
EReal.mul none (some none) = ⊥
EReal.mul none (some (some y)) = if 0 < y then ⊥ else if y = 0 then 0 else ⊤
EReal.mul (some none) none = ⊥
EReal.mul (some none) (some none) = ⊤
EReal.mul (some none) (some (some y)) = if 0 < y then ⊤ else if y = 0 then 0 else ⊥
EReal.mul (some (some x_2)) (some none) = if 0 < x_2 then ⊤ else if x_2 = 0 then 0 else ⊥
EReal.mul (some (some x_2)) none = if 0 < x_2 then ⊥ else if x_2 = 0 then 0 else ⊤
EReal.mul (some (some x_2)) (some (some y)) = ↑(x_2 * y)

Instances For

instance EReal.instMul :

Equations

EReal.instMul = { mul := EReal.mul }

@[simp]

theorem EReal.coe_mul (x y : ℝ) :

↑(x * y) = ↑x * ↑y

theorem EReal.induction₂ {P : EReal → EReal → Prop} (top_top : P ⊤ ⊤) (top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x) (top_zero : P ⊤ 0) (top_neg : ∀ x < 0, P ⊤ ↑x) (top_bot : P ⊤ ⊥) (pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤) (pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥) (zero_top : P 0 ⊤) (coe_coe : ∀ (x y : ℝ), P ↑x ↑y) (zero_bot : P 0 ⊥) (neg_top : ∀ x < 0, P ↑x ⊤) (neg_bot : ∀ x < 0, P ↑x ⊥) (bot_top : P ⊥ ⊤) (bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x) (bot_zero : P ⊥ 0) (bot_neg : ∀ x < 0, P ⊥ ↑x) (bot_bot : P ⊥ ⊥) (x y : EReal) :

P x y

Induct on two EReals by performing case splits on the sign of one whenever the other is infinite.

theorem EReal.induction₂_symm {P : EReal → EReal → Prop} (symm : ∀ {x y : EReal}, P x y → P y x) (top_top : P ⊤ ⊤) (top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x) (top_zero : P ⊤ 0) (top_neg : ∀ x < 0, P ⊤ ↑x) (top_bot : P ⊤ ⊥) (pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥) (coe_coe : ∀ (x y : ℝ), P ↑x ↑y) (zero_bot : P 0 ⊥) (neg_bot : ∀ x < 0, P ↑x ⊥) (bot_bot : P ⊥ ⊥) (x y : EReal) :

P x y

Induct on two EReals by performing case splits on the sign of one whenever the other is infinite. This version eliminates some cases by assuming that the relation is symmetric.

theorem EReal.mul_comm (x y : EReal) :

x * y = y * x

theorem EReal.one_mul (x : EReal) :

1 * x = x

theorem EReal.zero_mul (x : EReal) :

0 * x = 0

instance EReal.instMulZeroOneClass :

MulZeroOneClass EReal

Equations

One or more equations did not get rendered due to their size.

Real coercion #

instance EReal.canLift :

CanLift EReal ℝ Real.toEReal fun (r : EReal) => r ≠ ⊤ ∧ r ≠ ⊥

def EReal.toReal :

The map from extended reals to reals sending infinities to zero.

Equations

Instances For

@[simp]

theorem EReal.toReal_top :

@[simp]

theorem EReal.toReal_bot :

@[simp]

theorem EReal.toReal_zero :

@[simp]

theorem EReal.toReal_one :

@[simp]

theorem EReal.toReal_coe (x : ℝ) :

(↑x).toReal = x

@[simp]

theorem EReal.bot_lt_coe (x : ℝ) :

⊥ < ↑x

@[simp]

theorem EReal.coe_ne_bot (x : ℝ) :

↑x ≠ ⊥

@[simp]

theorem EReal.bot_ne_coe (x : ℝ) :

⊥ ≠ ↑x

@[simp]

theorem EReal.coe_lt_top (x : ℝ) :

↑x < ⊤

@[simp]

theorem EReal.coe_ne_top (x : ℝ) :

↑x ≠ ⊤

@[simp]

theorem EReal.top_ne_coe (x : ℝ) :

⊤ ≠ ↑x

@[simp]

theorem EReal.bot_lt_zero :

@[simp]

theorem EReal.bot_ne_zero :

@[simp]

theorem EReal.zero_ne_bot :

@[simp]

theorem EReal.zero_lt_top :

@[simp]

theorem EReal.zero_ne_top :

@[simp]

theorem EReal.top_ne_zero :

theorem EReal.range_coe :

Set.range Real.toEReal = {⊥, ⊤}ᶜ

theorem EReal.range_coe_eq_Ioo :

Set.range Real.toEReal = Set.Ioo ⊥ ⊤

@[simp]

theorem EReal.coe_add (x y : ℝ) :

↑(x + y) = ↑x + ↑y

theorem EReal.coe_nsmul (n : ℕ) (x : ℝ) :

↑(n • x) = n • ↑x

@[simp]

theorem EReal.coe_eq_zero {x : ℝ} :

↑x = 0 ↔ x = 0

@[simp]

theorem EReal.coe_eq_one {x : ℝ} :

↑x = 1 ↔ x = 1

theorem EReal.coe_ne_zero {x : ℝ} :

↑x ≠ 0 ↔ x ≠ 0

theorem EReal.coe_ne_one {x : ℝ} :

↑x ≠ 1 ↔ x ≠ 1

@[simp]

theorem EReal.coe_nonneg {x : ℝ} :

0 ≤ ↑x ↔ 0 ≤ x

@[simp]

theorem EReal.coe_nonpos {x : ℝ} :

↑x ≤ 0 ↔ x ≤ 0

@[simp]

theorem EReal.coe_pos {x : ℝ} :

0 < ↑x ↔ 0 < x

@[simp]

theorem EReal.coe_neg' {x : ℝ} :

↑x < 0 ↔ x < 0

theorem EReal.toReal_eq_zero_iff {x : EReal} :

x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥

theorem EReal.toReal_ne_zero_iff {x : EReal} :

x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥

theorem EReal.toReal_eq_toReal {x y : EReal} (hx_top : x ≠ ⊤) (hx_bot : x ≠ ⊥) (hy_top : y ≠ ⊤) (hy_bot : y ≠ ⊥) :

x.toReal = y.toReal ↔ x = y

theorem EReal.toReal_nonneg {x : EReal} (hx : 0 ≤ x) :

theorem EReal.toReal_nonpos {x : EReal} (hx : x ≤ 0) :

theorem EReal.toReal_le_toReal {x y : EReal} (h : x ≤ y) (hx : x ≠ ⊥) (hy : y ≠ ⊤) :

x.toReal ≤ y.toReal

theorem EReal.coe_toReal {x : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) :

↑x.toReal = x

theorem EReal.le_coe_toReal {x : EReal} (h : x ≠ ⊤) :

x ≤ ↑x.toReal

theorem EReal.coe_toReal_le {x : EReal} (h : x ≠ ⊥) :

↑x.toReal ≤ x

theorem EReal.eq_top_iff_forall_lt (x : EReal) :

x = ⊤ ↔ ∀ (y : ℝ), ↑y < x

theorem EReal.eq_bot_iff_forall_lt (x : EReal) :

x = ⊥ ↔ ∀ (y : ℝ), x < ↑y

Intervals and coercion from reals #

theorem EReal.exists_between_coe_real {x z : EReal} (h : x < z) :

∃ (y : ℝ), x < ↑y ∧ ↑y < z

@[simp]

theorem EReal.image_coe_Icc (x y : ℝ) :

Real.toEReal '' Set.Icc x y = Set.Icc ↑x ↑y

@[simp]

theorem EReal.image_coe_Ico (x y : ℝ) :

Real.toEReal '' Set.Ico x y = Set.Ico ↑x ↑y

@[simp]

theorem EReal.image_coe_Ici (x : ℝ) :

Real.toEReal '' Set.Ici x = Set.Ico ↑x ⊤

@[simp]

theorem EReal.image_coe_Ioc (x y : ℝ) :

Real.toEReal '' Set.Ioc x y = Set.Ioc ↑x ↑y

@[simp]

theorem EReal.image_coe_Ioo (x y : ℝ) :

Real.toEReal '' Set.Ioo x y = Set.Ioo ↑x ↑y

@[simp]

theorem EReal.image_coe_Ioi (x : ℝ) :

Real.toEReal '' Set.Ioi x = Set.Ioo ↑x ⊤

@[simp]

theorem EReal.image_coe_Iic (x : ℝ) :

Real.toEReal '' Set.Iic x = Set.Ioc ⊥ ↑x

@[simp]

theorem EReal.image_coe_Iio (x : ℝ) :

Real.toEReal '' Set.Iio x = Set.Ioo ⊥ ↑x

@[simp]

theorem EReal.preimage_coe_Ici (x : ℝ) :

Real.toEReal ⁻¹' Set.Ici ↑x = Set.Ici x

@[simp]

theorem EReal.preimage_coe_Ioi (x : ℝ) :

Real.toEReal ⁻¹' Set.Ioi ↑x = Set.Ioi x

@[simp]

theorem EReal.preimage_coe_Ioi_bot :

Real.toEReal ⁻¹' Set.Ioi ⊥ = Set.univ

@[simp]

theorem EReal.preimage_coe_Iic (y : ℝ) :

Real.toEReal ⁻¹' Set.Iic ↑y = Set.Iic y

@[simp]

theorem EReal.preimage_coe_Iio (y : ℝ) :

Real.toEReal ⁻¹' Set.Iio ↑y = Set.Iio y

@[simp]

theorem EReal.preimage_coe_Iio_top :

Real.toEReal ⁻¹' Set.Iio ⊤ = Set.univ

@[simp]

theorem EReal.preimage_coe_Icc (x y : ℝ) :

Real.toEReal ⁻¹' Set.Icc ↑x ↑y = Set.Icc x y

@[simp]

theorem EReal.preimage_coe_Ico (x y : ℝ) :

Real.toEReal ⁻¹' Set.Ico ↑x ↑y = Set.Ico x y

@[simp]

theorem EReal.preimage_coe_Ioc (x y : ℝ) :

Real.toEReal ⁻¹' Set.Ioc ↑x ↑y = Set.Ioc x y

@[simp]

theorem EReal.preimage_coe_Ioo (x y : ℝ) :

Real.toEReal ⁻¹' Set.Ioo ↑x ↑y = Set.Ioo x y

@[simp]

theorem EReal.preimage_coe_Ico_top (x : ℝ) :

Real.toEReal ⁻¹' Set.Ico ↑x ⊤ = Set.Ici x

@[simp]

theorem EReal.preimage_coe_Ioo_top (x : ℝ) :

Real.toEReal ⁻¹' Set.Ioo ↑x ⊤ = Set.Ioi x

@[simp]

theorem EReal.preimage_coe_Ioc_bot (y : ℝ) :

Real.toEReal ⁻¹' Set.Ioc ⊥ ↑y = Set.Iic y

@[simp]

theorem EReal.preimage_coe_Ioo_bot (y : ℝ) :

Real.toEReal ⁻¹' Set.Ioo ⊥ ↑y = Set.Iio y

@[simp]

theorem EReal.preimage_coe_Ioo_bot_top :

Real.toEReal ⁻¹' Set.Ioo ⊥ ⊤ = Set.univ

ennreal coercion #

@[simp]

theorem EReal.toReal_coe_ennreal {x : ENNReal} :

(↑x).toReal = x.toReal

@[simp]

theorem EReal.coe_ennreal_ofReal {x : ℝ} :

↑(ENNReal.ofReal x) = ↑(max x 0)

theorem EReal.coe_ennreal_toReal {x : ENNReal} (hx : x ≠ ⊤) :

↑x.toReal = ↑x

theorem EReal.coe_nnreal_eq_coe_real (x : NNReal) :

↑↑x = ↑↑x

@[simp]

theorem EReal.coe_ennreal_zero :

↑0 = 0

@[simp]

theorem EReal.coe_ennreal_one :

↑1 = 1

@[simp]

theorem EReal.coe_ennreal_top :

theorem EReal.coe_ennreal_strictMono :

StrictMono ENNReal.toEReal

theorem EReal.coe_ennreal_injective :

Function.Injective ENNReal.toEReal

@[simp]

theorem EReal.coe_ennreal_eq_top_iff {x : ENNReal} :

↑x = ⊤ ↔ x = ⊤

theorem EReal.coe_nnreal_ne_top (x : NNReal) :

↑↑x ≠ ⊤

@[simp]

theorem EReal.coe_nnreal_lt_top (x : NNReal) :

↑↑x < ⊤

@[simp]

theorem EReal.coe_ennreal_le_coe_ennreal_iff {x y : ENNReal} :

↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem EReal.coe_ennreal_lt_coe_ennreal_iff {x y : ENNReal} :

↑x < ↑y ↔ x < y

@[simp]

theorem EReal.coe_ennreal_eq_coe_ennreal_iff {x y : ENNReal} :

↑x = ↑y ↔ x = y

theorem EReal.coe_ennreal_ne_coe_ennreal_iff {x y : ENNReal} :

↑x ≠ ↑y ↔ x ≠ y

@[simp]

theorem EReal.coe_ennreal_eq_zero {x : ENNReal} :

↑x = 0 ↔ x = 0

@[simp]

theorem EReal.coe_ennreal_eq_one {x : ENNReal} :

↑x = 1 ↔ x = 1

theorem EReal.coe_ennreal_ne_zero {x : ENNReal} :

↑x ≠ 0 ↔ x ≠ 0

theorem EReal.coe_ennreal_ne_one {x : ENNReal} :

↑x ≠ 1 ↔ x ≠ 1

theorem EReal.coe_ennreal_nonneg (x : ENNReal) :

0 ≤ ↑x

@[simp]

theorem EReal.range_coe_ennreal :

Set.range ENNReal.toEReal = Set.Ici 0

instance EReal.instCanLiftENNRealToERealLeOfNat :

CanLift EReal ENNReal ENNReal.toEReal fun (x : EReal) => 0 ≤ x

@[simp]

theorem EReal.coe_ennreal_pos {x : ENNReal} :

0 < ↑x ↔ 0 < x

@[simp]

theorem EReal.bot_lt_coe_ennreal (x : ENNReal) :

⊥ < ↑x

@[simp]

theorem EReal.coe_ennreal_ne_bot (x : ENNReal) :

↑x ≠ ⊥

@[simp]

theorem EReal.coe_ennreal_add (x y : ENNReal) :

↑(x + y) = ↑x + ↑y

@[simp]

theorem EReal.coe_ennreal_mul (x y : ENNReal) :

↑(x * y) = ↑x * ↑y

theorem EReal.coe_ennreal_nsmul (n : ℕ) (x : ENNReal) :

↑(n • x) = n • ↑x

toENNReal #

noncomputable def EReal.toENNReal (x : EReal) :

x.toENNReal returns x if it is nonnegative, 0 otherwise.

Equations

x.toENNReal = if x = ⊤ then ⊤ else ENNReal.ofReal x.toReal

Instances For

@[simp]

theorem EReal.toENNReal_top :

⊤.toENNReal = ⊤

@[simp]

theorem EReal.toENNReal_of_ne_top {x : EReal} (hx : x ≠ ⊤) :

x.toENNReal = ENNReal.ofReal x.toReal

@[simp]

theorem EReal.toENNReal_eq_top_iff {x : EReal} :

x.toENNReal = ⊤ ↔ x = ⊤

theorem EReal.toENNReal_ne_top_iff {x : EReal} :

x.toENNReal ≠ ⊤ ↔ x ≠ ⊤

@[simp]

theorem EReal.toENNReal_of_nonpos {x : EReal} (hx : x ≤ 0) :

x.toENNReal = 0

theorem EReal.toENNReal_bot :

⊥.toENNReal = 0

theorem EReal.toENNReal_zero :

toENNReal 0 = 0

theorem EReal.toENNReal_eq_zero_iff {x : EReal} :

x.toENNReal = 0 ↔ x ≤ 0

theorem EReal.toENNReal_ne_zero_iff {x : EReal} :

x.toENNReal ≠ 0 ↔ 0 < x

@[simp]

theorem EReal.coe_toENNReal {x : EReal} (hx : 0 ≤ x) :

↑x.toENNReal = x

theorem EReal.coe_toENNReal_eq_max {x : EReal} :

↑x.toENNReal = max 0 x

@[simp]

theorem EReal.toENNReal_coe {x : ENNReal} :

(↑x).toENNReal = x

@[simp]

theorem EReal.real_coe_toENNReal (x : ℝ) :

(↑x).toENNReal = ENNReal.ofReal x

@[simp]

theorem EReal.toReal_toENNReal {x : EReal} (hx : 0 ≤ x) :

x.toENNReal.toReal = x.toReal

theorem EReal.toENNReal_eq_toENNReal {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) :

x.toENNReal = y.toENNReal ↔ x = y

theorem EReal.toENNReal_le_toENNReal {x y : EReal} (h : x ≤ y) :

x.toENNReal ≤ y.toENNReal

theorem EReal.toENNReal_lt_toENNReal {x y : EReal} (hx : 0 ≤ x) (hxy : x < y) :

x.toENNReal < y.toENNReal

nat coercion #

theorem EReal.coe_coe_eq_natCast (n : ℕ) :

↑↑n = ↑n

theorem EReal.natCast_ne_bot (n : ℕ) :

↑n ≠ ⊥

theorem EReal.natCast_ne_top (n : ℕ) :

↑n ≠ ⊤

theorem EReal.natCast_eq_iff {m n : ℕ} :

↑m = ↑n ↔ m = n

theorem EReal.natCast_ne_iff {m n : ℕ} :

↑m ≠ ↑n ↔ m ≠ n

theorem EReal.natCast_le_iff {m n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

theorem EReal.natCast_lt_iff {m n : ℕ} :

↑m < ↑n ↔ m < n

@[simp]

theorem EReal.natCast_mul (m n : ℕ) :

↑(m * n) = ↑m * ↑n

Miscellaneous lemmas #

theorem EReal.exists_rat_btwn_of_lt {a b : EReal} :

a < b → ∃ (x : ℚ), a < ↑↑x ∧ ↑↑x < b

theorem EReal.lt_iff_exists_rat_btwn {a b : EReal} :

a < b ↔ ∃ (x : ℚ), a < ↑↑x ∧ ↑↑x < b

theorem EReal.lt_iff_exists_real_btwn {a b : EReal} :

a < b ↔ ∃ (x : ℝ), a < ↑x ∧ ↑x < b

def EReal.neTopBotEquivReal :

↑{⊥, ⊤}ᶜ ≃ ℝ

The set of numbers in EReal that are not equal to ±∞ is equivalent to ℝ.

Equations

One or more equations did not get rendered due to their size.

Instances For