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

Instances For

instance instBotEReal :

Equations

instance instZeroEReal :

Equations

instance instOneEReal :

Equations

instance instNontrivialEReal :

Nontrivial EReal

Equations

instance instAddMonoidEReal :

AddMonoid EReal

Equations

instance instPartialOrderEReal :

PartialOrder EReal

Equations

instance instAddCommMonoidEReal :

AddCommMonoid EReal

Equations

instance instZeroLEOneClassEReal :

ZeroLEOneClass EReal

instance instSupSetEReal :

Equations

instance instInfSetEReal :

Equations

instance instCompleteLinearOrderEReal :

CompleteLinearOrder EReal

Equations

instance instLinearOrderEReal :

LinearOrder EReal

Equations

instance instIsOrderedAddMonoidEReal :

IsOrderedAddMonoid EReal

instance instAddCommMonoidWithOneEReal :

AddCommMonoidWithOne EReal

Equations

instance instDenselyOrderedEReal :

DenselyOrdered EReal

instance instCharZeroEReal :

def Real.toEReal :

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

Equations

Instances For

instance EReal.decidableLT :

DecidableLT EReal

Equations

instance EReal.instTop :

Equations

instance EReal.instCoeReal :

Equations

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

theorem EReal.coe_le_coe {x y : ℝ} :

x ≤ y → ↑x ≤ ↑y

Alias of the reverse direction of EReal.coe_le_coe_iff.

@[simp]

theorem EReal.coe_lt_coe_iff {x y : ℝ} :

↑x < ↑y ↔ x < y

theorem EReal.coe_lt_coe {x y : ℝ} :

x < y → ↑x < ↑y

Alias of the reverse direction of EReal.coe_lt_coe_iff.

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

@[simp]

theorem EReal.coe_natCast {n : ℕ} :

↑↑n = ↑n

def ENNReal.toEReal :

ENNReal → EReal

The canonical map from nonnegative extended reals to extended reals.

Equations

Instances For

instance EReal.hasCoeENNReal :

Coe ENNReal EReal

Equations

instance EReal.instInhabited :

Inhabited EReal

Equations

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

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

Instances For

instance EReal.instMul :

Equations

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

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_pos {x : EReal} (hx : 0 < x) (h'x : x ≠ ⊤) :

theorem EReal.toReal_neg {x : EReal} (hx : x < 0) (h'x : x ≠ ⊥) :

@[simp]

theorem EReal.toReal_image_Ioo_zero_top :

toReal '' Set.Ioo 0 ⊤ = Set.Ioi 0

@[simp]

theorem EReal.toReal_image_Ioo_bot_zero :

toReal '' Set.Ioo ⊥ 0 = Set.Iio 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

theorem EReal.coe_ennreal_pos_iff_ne_zero {x : ENNReal} :

0 < ↑x ↔ x ≠ 0

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

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.toENNReal_pos_iff {x : EReal} :

0 < x.toENNReal ↔ 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

Instances For

def Mathlib.Meta.Positivity.evalRealToEReal :

Extension for the positivity tactic: cast from ℝ to EReal.

Equations

Instances For

def Mathlib.Meta.Positivity.evalENNRealToEReal :

Extension for the positivity tactic: cast from ℝ≥0∞ to EReal.

Equations

Instances For

def Mathlib.Meta.Positivity.evalERealToReal :

Extension for the positivity tactic: projection from EReal to ℝ.

We prove that EReal.toReal x is nonnegative whenever x is nonnegative. Since EReal.toReal ⊤ = 0, we cannot prove a stronger statement, at least without relying on a tactic like finiteness.

Equations

Instances For

def Mathlib.Meta.Positivity.evalERealToENNReal :

Extension for the positivity tactic: projection from EReal to ℝ≥0∞.

We show that EReal.toENNReal x is positive whenever x is positive, and it is nonnegative otherwise. We cannot deduce any corollaries from x ≠ 0, since EReal.toENNReal x = 0 for x < 0.

Equations

Instances For