The extended reals [-∞, ∞].

This file defines EReal, the real numbers together with a top and bottom element, referred to as ⊤ and ⊥. It is implemented as WithBot (WithTop ℝ)

Addition and multiplication are problematic in the presence of ±∞, but negation has a natural definition and satisfies the usual properties, in particular it is an order reversing isomorphism

An ad hoc addition is defined, for which EReal is an AddCommMonoid, and even an ordered one (if a ≤ a' and b ≤ b' then a + b ≤ a' + b'). Note however that addition is badly behaved at (⊥, ⊤) and (⊤, ⊥) so this can not be upgraded to a group structure. Our choice is that ⊥ + ⊤ = ⊤ + ⊥ = ⊥, to make sure that the exponential and the logarithm between EReal and ℝ≥0∞ respect the operations (notice that the convention 0 * ∞ = 0 on ℝ≥0∞ is enforced by measure theory).

An ad hoc subtraction is then defined by x - y = x + (-y). It does not have nice properties, but it is sometimes convenient to have.

An ad hoc multiplication is defined, for which EReal is a CommMonoidWithZero. We make the choice that 0 * x = x * 0 = 0 for any x (while the other cases are defined non-ambiguously). This does not distribute with addition, as ⊥ = ⊥ + ⊤ = 1*⊥ + (-1)*⊥ ≠ (1 - 1) * ⊥ = 0 * ⊥ = 0. Distributivity x * (y + z) = x * y + x * z is recovered in the case where either 0 ≤ x < ⊤, see Ereal.left_distrib_of_nonneg_of_ne_top, or 0 ≤ y, z, see Ereal.left_distrib_of_nonneg (similarly for right distributivity).

EReal is a CompleteLinearOrder; this is deduced by type class inference from the fact that WithBot (WithTop L) is a complete linear order if L is a conditionally complete linear order.

Coercions from ℝ and from ℝ≥0∞ are registered, and their basic properties are proved. The main one is the real coercion, and is usually referred to just as coe (lemmas such as EReal.coe_add deal with this coercion). The one from ENNReal is usually called coe_ennreal in the EReal namespace.

We define an absolute value EReal.abs from EReal to ℝ≥0∞. Two elements of EReal coincide if and only if they have the same absolute value and the same sign.

Tags

real, ereal, complete lattice

def EReal : Type

ereal : The type [-∞, ∞]

Equations

• EReal = WithBot (WithTop ℝ)

instance instERealBot : Bot EReal

Equations

• instERealBot = WithBot.bot

instance instERealZero : Zero EReal

Equations

• instERealZero = WithBot.zero

instance instERealOne : One EReal

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 instZeroLEOneClassEReal : ZeroLEOneClass EReal

instance instSupSetEReal : SupSet EReal

Equations

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

instance instInfSetEReal : InfSet EReal

Equations

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

instance instCompleteLinearOrderEReal : CompleteLinearOrder EReal

Equations

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

instance instLinearOrderedAddCommMonoidEReal : LinearOrderedAddCommMonoid EReal

Equations

• instLinearOrderedAddCommMonoidEReal = inferInstanceAs (LinearOrderedAddCommMonoid (WithBot (WithTop ℝ)))

instance instAddCommMonoidWithOneEReal : AddCommMonoidWithOne EReal

Equations

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

instance instDenselyOrderedEReal : DenselyOrdered EReal

instance instCharZeroEReal : CharZero EReal

def Real.toEReal : ℝ → EReal

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

Equations

• Real.toEReal = some ∘ some

instance EReal.decidableLT : DecidableRel fun (x1 x2 : EReal) => x1 < x2

Equations

• EReal.decidableLT = WithBot.decidableLT

instance EReal.instTop : Top EReal

Equations

• EReal.instTop = { top := some ⊤ }

instance EReal.instCoeReal : Coe ℝ EReal

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

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 {C : EReal → Sort u_1} (h_bot : C ⊥) (h_real : (a : ℝ) → C ↑a) (h_top : C ⊤) (a : EReal) : C 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 h_bot h_real h_top none = h_bot
• EReal.rec h_bot h_real h_top (some (some a)) = h_real a
• EReal.rec h_bot h_real h_top (some none) = h_top

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)

instance EReal.instMul : Mul EReal

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.

EReal with its multiplication is a CommMonoidWithZero. However, the proof of associativity by hand is extremely painful (with 125 cases...). Instead, we will deduce it later on from the facts that the absolute value and the sign are multiplicative functions taking value in associative objects, and that they characterize an extended real number. For now, we only record more basic properties of multiplication.

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

• EReal.instMulZeroOneClass = MulZeroOneClass.mk EReal.zero_mul EReal.instMulZeroOneClass.proof_2

Real coercion

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

def EReal.toReal : EReal → ℝ

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

Equations

• EReal.toReal none = 0
• EReal.toReal (some none) = 0
• EReal.toReal (some (some x_1)) = x_1

@[simp]

theorem EReal.toReal_top : ⊤.toReal = 0

@[simp]

theorem EReal.toReal_bot : ⊥.toReal = 0

@[simp]

theorem EReal.toReal_zero : EReal.toReal 0 = 0

@[simp]

theorem EReal.toReal_one : EReal.toReal 1 = 1

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

@[simp]

theorem EReal.bot_ne_zero : ⊥ ≠ 0

@[simp]

theorem EReal.zero_ne_bot : 0 ≠ ⊥

@[simp]

theorem EReal.zero_lt_top : 0 < ⊤

@[simp]

theorem EReal.zero_ne_top : 0 ≠ ⊤

@[simp]

theorem EReal.top_ne_zero : ⊤ ≠ 0

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) : 0 ≤ x.toReal

theorem EReal.toReal_nonpos {x : EReal} (hx : x ≤ 0) : x.toReal ≤ 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) = ↑(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) : ENNReal

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

Equations

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

@[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 : EReal.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 = 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

Order

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.

Addition

@[simp]

theorem EReal.add_bot (x : EReal) : x + ⊥ = ⊥

@[simp]

theorem EReal.bot_add (x : EReal) : ⊥ + x = ⊥

@[simp]

theorem EReal.add_eq_bot_iff {x y : EReal} : x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

theorem EReal.add_ne_bot_iff {x y : EReal} : x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

@[simp]

theorem EReal.bot_lt_add_iff {x y : EReal} : ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

@[simp]

theorem EReal.top_add_top : ⊤ + ⊤ = ⊤

@[simp]

theorem EReal.top_add_coe (x : ℝ) : ⊤ + ↑x = ⊤

@[simp]

theorem EReal.top_add_of_ne_bot {x : EReal} (h : x ≠ ⊥) : ⊤ + x = ⊤

For any extended real number x which is not ⊥, the sum of ⊤ and x is equal to ⊤.

theorem EReal.top_add_iff_ne_bot {x : EReal} : ⊤ + x = ⊤ ↔ x ≠ ⊥

For any extended real number x, the sum of ⊤ and x is equal to ⊤ if and only if x is not ⊥.

@[simp]

theorem EReal.add_top_of_ne_bot {x : EReal} (h : x ≠ ⊥) : x + ⊤ = ⊤

For any extended real number x which is not ⊥, the sum of x and ⊤ is equal to ⊤.

theorem EReal.add_top_iff_ne_bot {x : EReal} : x + ⊤ = ⊤ ↔ x ≠ ⊥

For any extended real number x, the sum of x and ⊤ is equal to ⊤ if and only if x is not ⊥.

theorem EReal.add_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

For any two extended real numbers a and b, if both a and b are greater than 0, then their sum is also greater than 0.

@[simp]

theorem EReal.coe_add_top (x : ℝ) : ↑x + ⊤ = ⊤

theorem EReal.toReal_add {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) : (x + y).toReal = x.toReal + y.toReal

theorem EReal.toENNReal_add {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) : (x + y).toENNReal = x.toENNReal + y.toENNReal

theorem EReal.toENNReal_add_le {x y : EReal} : (x + y).toENNReal ≤ x.toENNReal + y.toENNReal

theorem EReal.addLECancellable_coe (x : ℝ) : AddLECancellable ↑x

theorem EReal.add_lt_add_right_coe {x y : EReal} (h : x < y) (z : ℝ) : x + ↑z < y + ↑z

theorem EReal.add_lt_add_left_coe {x y : EReal} (h : x < y) (z : ℝ) : ↑z + x < ↑z + y

theorem EReal.add_lt_add {x y z t : EReal} (h1 : x < y) (h2 : z < t) : x + z < y + t

theorem EReal.add_lt_add_of_lt_of_le' {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hbot : t ≠ ⊥) (htop : t = ⊤ → z = ⊤ → x = ⊥) : x + z < y + t

theorem EReal.add_lt_add_of_lt_of_le {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hz : z ≠ ⊥) (ht : t ≠ ⊤) : x + z < y + t

See also EReal.add_lt_add_of_lt_of_le' for a version with weaker but less convenient assumptions.

theorem EReal.add_lt_top {x y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x + y < ⊤

theorem EReal.add_ne_top {x y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x + y ≠ ⊤

theorem EReal.add_ne_top_iff_ne_top₂ {x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

theorem EReal.add_ne_top_iff_ne_top_left {x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) : x + y ≠ ⊤ ↔ x ≠ ⊤

theorem EReal.add_ne_top_iff_ne_top_right {x y : EReal} (hx : x ≠ ⊥) (hx' : x ≠ ⊤) : x + y ≠ ⊤ ↔ y ≠ ⊤

theorem EReal.add_ne_top_iff_of_ne_bot {x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

theorem EReal.add_ne_top_iff_of_ne_bot_of_ne_top {x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) : x + y ≠ ⊤ ↔ x ≠ ⊤

instance EReal.instLinearOrderedAddCommMonoidWithTopOrderDual : LinearOrderedAddCommMonoidWithTop ERealᵒᵈ

We do not have a notion of LinearOrderedAddCommMonoidWithBot but we can at least make the order dual of the extended reals into a LinearOrderedAddCommMonoidWithTop.

Equations

• EReal.instLinearOrderedAddCommMonoidWithTopOrderDual = LinearOrderedAddCommMonoidWithTop.mk EReal.instLinearOrderedAddCommMonoidWithTopOrderDual.proof_2

Negation

def EReal.neg : EReal → EReal

negation on EReal

Equations

• EReal.neg none = ⊤
• EReal.neg (some none) = ⊥
• EReal.neg (some (some x_1)) = ↑(-x_1)

instance EReal.instNeg : Neg EReal

Equations

• EReal.instNeg = { neg := EReal.neg }

instance EReal.instSubNegZeroMonoid : SubNegZeroMonoid EReal

Equations

• EReal.instSubNegZeroMonoid = SubNegZeroMonoid.mk EReal.instSubNegZeroMonoid.proof_5

@[simp]

theorem EReal.neg_top : -⊤ = ⊥

@[simp]

theorem EReal.neg_bot : -⊥ = ⊤

@[simp]

theorem EReal.coe_neg (x : ℝ) : ↑(-x) = -↑x

@[simp]

theorem EReal.coe_sub (x y : ℝ) : ↑(x - y) = ↑x - ↑y

theorem EReal.coe_zsmul (n : ℤ) (x : ℝ) : ↑(n • x) = n • ↑x

instance EReal.instInvolutiveNeg : InvolutiveNeg EReal

Equations

• EReal.instInvolutiveNeg = InvolutiveNeg.mk EReal.instInvolutiveNeg.proof_1

@[simp]

theorem EReal.toReal_neg {a : EReal} : (-a).toReal = -a.toReal

@[simp]

theorem EReal.neg_eq_top_iff {x : EReal} : -x = ⊤ ↔ x = ⊥

@[simp]

theorem EReal.neg_eq_bot_iff {x : EReal} : -x = ⊥ ↔ x = ⊤

@[simp]

theorem EReal.neg_eq_zero_iff {x : EReal} : -x = 0 ↔ x = 0

theorem EReal.neg_strictAnti : StrictAnti fun (x : EReal) => -x

@[simp]

theorem EReal.neg_le_neg_iff {a b : EReal} : -a ≤ -b ↔ b ≤ a

@[simp]

theorem EReal.neg_lt_neg_iff {a b : EReal} : -a < -b ↔ b < a

theorem EReal.neg_le {a b : EReal} : -a ≤ b ↔ -b ≤ a

-a ≤ b if and only if -b ≤ a on EReal.

theorem EReal.neg_le_of_neg_le {a b : EReal} (h : -a ≤ b) : -b ≤ a

If -a ≤ b then -b ≤ a on EReal.

theorem EReal.le_neg {a b : EReal} : a ≤ -b ↔ b ≤ -a

a ≤ -b if and only if b ≤ -a on EReal.

theorem EReal.le_neg_of_le_neg {a b : EReal} (h : a ≤ -b) : b ≤ -a

If a ≤ -b then b ≤ -a on EReal.

theorem EReal.neg_lt_comm {a b : EReal} : -a < b ↔ -b < a

-a < b if and only if -b < a on EReal.

@[deprecated EReal.neg_lt_comm (since := "2024-11-19")]

theorem EReal.neg_lt_iff_neg_lt {a b : EReal} : -a < b ↔ -b < a

Alias of EReal.neg_lt_comm.

---

-a < b if and only if -b < a on EReal.

theorem EReal.neg_lt_of_neg_lt {a b : EReal} (h : -a < b) : -b < a

If -a < b then -b < a on EReal.

theorem EReal.lt_neg_comm {a b : EReal} : a < -b ↔ b < -a

-a < b if and only if -b < a on EReal.

theorem EReal.lt_neg_of_lt_neg {a b : EReal} (h : a < -b) : b < -a

If a < -b then b < -a on EReal.

def EReal.negOrderIso : EReal ≃o ERealᵒᵈ

Negation as an order reversing isomorphism on EReal.

Equations

• EReal.negOrderIso = { toFun := fun (x : EReal) => OrderDual.toDual (-x), invFun := fun (x : ERealᵒᵈ) => -OrderDual.ofDual x, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem EReal.neg_add {x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊤) (h2 : x ≠ ⊤ ∨ y ≠ ⊥) : -(x + y) = -x - y

theorem EReal.neg_sub {x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊥) (h2 : x ≠ ⊤ ∨ y ≠ ⊤) : -(x - y) = -x + y

Subtraction

Subtraction on EReal is defined by x - y = x + (-y). Since addition is badly behaved at some points, so is subtraction. There is no standard algebraic typeclass involving subtraction that is registered on EReal, beyond SubNegZeroMonoid, because of this bad behavior.

@[simp]

theorem EReal.bot_sub (x : EReal) : ⊥ - x = ⊥

@[simp]

theorem EReal.sub_top (x : EReal) : x - ⊤ = ⊥

@[simp]

theorem EReal.top_sub_bot : ⊤ - ⊥ = ⊤

@[simp]

theorem EReal.top_sub_coe (x : ℝ) : ⊤ - ↑x = ⊤

@[simp]

theorem EReal.coe_sub_bot (x : ℝ) : ↑x - ⊥ = ⊤

@[simp]

theorem EReal.sub_bot {x : EReal} (h : x ≠ ⊥) : x - ⊥ = ⊤

@[simp]

theorem EReal.top_sub {x : EReal} (hx : x ≠ ⊤) : ⊤ - x = ⊤

@[simp]

theorem EReal.sub_self {x : EReal} (h_top : x ≠ ⊤) (h_bot : x ≠ ⊥) : x - x = 0

theorem EReal.sub_self_le_zero {x : EReal} : x - x ≤ 0

theorem EReal.sub_nonneg {x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) : 0 ≤ x - y ↔ y ≤ x

theorem EReal.sub_nonpos {x y : EReal} : x - y ≤ 0 ↔ x ≤ y

theorem EReal.sub_pos {x y : EReal} : 0 < x - y ↔ y < x

theorem EReal.sub_neg {x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) : x - y < 0 ↔ x < y

theorem EReal.sub_le_sub {x y z t : EReal} (h : x ≤ y) (h' : t ≤ z) : x - z ≤ y - t

theorem EReal.sub_lt_sub_of_lt_of_le {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hz : z ≠ ⊥) (ht : t ≠ ⊤) : x - t < y - z

theorem EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal (x : ℝ) : ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

theorem EReal.toReal_sub {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) : (x - y).toReal = x.toReal - y.toReal

theorem EReal.toENNReal_sub {x y : EReal} (hy : 0 ≤ y) : (x - y).toENNReal = x.toENNReal - y.toENNReal

theorem EReal.add_sub_cancel_right {a : EReal} {b : ℝ} : a + ↑b - ↑b = a

theorem EReal.add_sub_cancel_left {a : EReal} {b : ℝ} : ↑b + a - ↑b = a

theorem EReal.sub_add_cancel {a : EReal} {b : ℝ} : a - ↑b + ↑b = a

theorem EReal.sub_add_cancel_right {a : EReal} {b : ℝ} : ↑b - (a + ↑b) = -a

theorem EReal.sub_add_cancel_left {a : EReal} {b : ℝ} : ↑b - (↑b + a) = -a

theorem EReal.le_sub_iff_add_le {a b c : EReal} (hb : b ≠ ⊥ ∨ c ≠ ⊥) (ht : b ≠ ⊤ ∨ c ≠ ⊤) : a ≤ c - b ↔ a + b ≤ c

theorem EReal.sub_le_iff_le_add {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) : a - b ≤ c ↔ a ≤ c + b

theorem EReal.lt_sub_iff_add_lt {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) : c < a - b ↔ c + b < a

theorem EReal.sub_le_of_le_add {a b c : EReal} (h : a ≤ b + c) : a - c ≤ b

theorem EReal.sub_le_of_le_add' {a b c : EReal} (h : a ≤ b + c) : a - b ≤ c

See also EReal.sub_le_of_le_add.

theorem EReal.add_le_of_le_sub {a b c : EReal} (h : a ≤ b - c) : a + c ≤ b

theorem EReal.sub_lt_iff {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊥) (h₂ : b ≠ ⊤ ∨ c ≠ ⊤) : c - b < a ↔ c < a + b

theorem EReal.add_lt_of_lt_sub {a b c : EReal} (h : a < b - c) : a + c < b

theorem EReal.sub_lt_of_lt_add {a b c : EReal} (h : a < b + c) : a - c < b

theorem EReal.sub_lt_of_lt_add' {a b c : EReal} (h : a < b + c) : a - b < c

See also EReal.sub_lt_of_lt_add.

Addition and order

theorem EReal.le_of_forall_lt_iff_le {x y : EReal} : (∀ (z : ℝ), x < ↑z → y ≤ ↑z) ↔ y ≤ x

theorem EReal.ge_of_forall_gt_iff_ge {x y : EReal} : (∀ (z : ℝ), ↑z < y → ↑z ≤ x) ↔ y ≤ x

theorem EReal.add_le_of_forall_lt {a b c : EReal} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) : a + b ≤ c

theorem EReal.le_add_of_forall_gt {a b c : EReal} (h₁ : a ≠ ⊥ ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ b ≠ ⊥) (h : ∀ a' > a, ∀ b' > b, c ≤ a' + b') : c ≤ a + b

@[deprecated EReal.add_le_of_forall_lt (since := "2024-11-19")]

theorem EReal.top_add_le_of_forall_add_le {a b c : EReal} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) : a + b ≤ c

Alias of EReal.add_le_of_forall_lt.

@[deprecated EReal.add_le_of_forall_lt (since := "2024-11-19")]

theorem EReal.add_le_of_forall_add_le {a b c : EReal} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) : a + b ≤ c

Alias of EReal.add_le_of_forall_lt.

@[deprecated EReal.le_add_of_forall_gt (since := "2024-11-19")]

theorem EReal.le_add_of_forall_le_add {a b c : EReal} (h₁ : a ≠ ⊥ ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ b ≠ ⊥) (h : ∀ a' > a, ∀ b' > b, c ≤ a' + b') : c ≤ a + b

Alias of EReal.le_add_of_forall_gt.

theorem ENNReal.toEReal_sub {x y : ENNReal} (hy_top : y ≠ ⊤) (h_le : y ≤ x) : ↑(x - y) = ↑x - ↑y

Multiplication

@[simp]

theorem EReal.top_mul_top : ⊤ * ⊤ = ⊤

@[simp]

theorem EReal.top_mul_bot : ⊤ * ⊥ = ⊥

@[simp]

theorem EReal.bot_mul_top : ⊥ * ⊤ = ⊥

@[simp]

theorem EReal.bot_mul_bot : ⊥ * ⊥ = ⊤

theorem EReal.coe_mul_top_of_pos {x : ℝ} (h : 0 < x) : ↑x * ⊤ = ⊤

theorem EReal.coe_mul_top_of_neg {x : ℝ} (h : x < 0) : ↑x * ⊤ = ⊥

theorem EReal.top_mul_coe_of_pos {x : ℝ} (h : 0 < x) : ⊤ * ↑x = ⊤

theorem EReal.top_mul_coe_of_neg {x : ℝ} (h : x < 0) : ⊤ * ↑x = ⊥

theorem EReal.mul_top_of_pos {x : EReal} : 0 < x → x * ⊤ = ⊤

theorem EReal.mul_top_of_neg {x : EReal} : x < 0 → x * ⊤ = ⊥

theorem EReal.top_mul_of_pos {x : EReal} (h : 0 < x) : ⊤ * x = ⊤

theorem EReal.top_mul_of_neg {x : EReal} (h : x < 0) : ⊤ * x = ⊥

theorem EReal.top_mul_coe_ennreal {x : ENNReal} (hx : x ≠ 0) : ⊤ * ↑x = ⊤

theorem EReal.coe_ennreal_mul_top {x : ENNReal} (hx : x ≠ 0) : ↑x * ⊤ = ⊤

theorem EReal.coe_mul_bot_of_pos {x : ℝ} (h : 0 < x) : ↑x * ⊥ = ⊥

theorem EReal.coe_mul_bot_of_neg {x : ℝ} (h : x < 0) : ↑x * ⊥ = ⊤

theorem EReal.bot_mul_coe_of_pos {x : ℝ} (h : 0 < x) : ⊥ * ↑x = ⊥

theorem EReal.bot_mul_coe_of_neg {x : ℝ} (h : x < 0) : ⊥ * ↑x = ⊤

theorem EReal.mul_bot_of_pos {x : EReal} : 0 < x → x * ⊥ = ⊥

theorem EReal.mul_bot_of_neg {x : EReal} : x < 0 → x * ⊥ = ⊤

theorem EReal.bot_mul_of_pos {x : EReal} (h : 0 < x) : ⊥ * x = ⊥

theorem EReal.bot_mul_of_neg {x : EReal} (h : x < 0) : ⊥ * x = ⊤

theorem EReal.toReal_mul {x y : EReal} : (x * y).toReal = x.toReal * y.toReal

instance EReal.instNoZeroDivisors : NoZeroDivisors EReal

theorem EReal.mul_pos_iff {a b : EReal} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

theorem EReal.mul_nonneg_iff {a b : EReal} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem EReal.mul_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a * b

The product of two positive extended real numbers is positive.

theorem EReal.induction₂_neg_left {P : EReal → EReal → Prop} (neg_left : ∀ {x y : EReal}, P x y → P (-x) y) (top_top : P ⊤ ⊤) (top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x) (top_zero : P ⊤ 0) (top_neg : ∀ x < 0, P ⊤ ↑x) (top_bot : P ⊤ ⊥) (zero_top : P 0 ⊤) (zero_bot : P 0 ⊥) (pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤) (pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥) (coe_coe : ∀ (x y : ℝ), P ↑x ↑y) (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 P x y implies P (-x) y for all x, y.

theorem EReal.induction₂_symm_neg {P : EReal → EReal → Prop} (symm : ∀ {x y : EReal}, P x y → P y x) (neg_left : ∀ {x y : EReal}, P x y → P (-x) y) (top_top : P ⊤ ⊤) (top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x) (top_zero : P ⊤ 0) (coe_coe : ∀ (x y : ℝ), P ↑x ↑y) (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 P is symmetric and P x y implies P (-x) y for all x, y.

theorem EReal.neg_mul (x y : EReal) : -x * y = -(x * y)

instance EReal.instHasDistribNeg : HasDistribNeg EReal

Equations

• EReal.instHasDistribNeg = HasDistribNeg.mk EReal.neg_mul EReal.instHasDistribNeg.proof_1

theorem EReal.mul_neg_iff {a b : EReal} : a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

theorem EReal.mul_nonpos_iff {a b : EReal} : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

theorem EReal.mul_eq_top (a b : EReal) : a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤

theorem EReal.mul_ne_top (a b : EReal) : a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

theorem EReal.mul_eq_bot (a b : EReal) : a * b = ⊥ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

theorem EReal.mul_ne_bot (a b : EReal) : a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

theorem EReal.toENNReal_mul {x y : EReal} (hx : 0 ≤ x) : (x * y).toENNReal = x.toENNReal * y.toENNReal

EReal.toENNReal is multiplicative. For the version with the nonnegativity hypothesis on the second variable, see EReal.toENNReal_mul'.

theorem EReal.toENNReal_mul' {x y : EReal} (hy : 0 ≤ y) : (x * y).toENNReal = x.toENNReal * y.toENNReal

EReal.toENNReal is multiplicative. For the version with the nonnegativity hypothesis on the first variable, see EReal.toENNReal_mul.

theorem EReal.right_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a + b) * c = a * c + b * c

theorem EReal.left_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) : c * (a + b) = c * a + c * b

theorem EReal.left_distrib_of_nonneg_of_ne_top {x : EReal} (hx_nonneg : 0 ≤ x) (hx_ne_top : x ≠ ⊤) (y z : EReal) : x * (y + z) = x * y + x * z

theorem EReal.right_distrib_of_nonneg_of_ne_top {x : EReal} (hx_nonneg : 0 ≤ x) (hx_ne_top : x ≠ ⊤) (y z : EReal) : (y + z) * x = y * x + z * x

@[simp]

theorem EReal.nsmul_eq_mul (n : ℕ) (x : EReal) : n • x = ↑n * x

Absolute value

def EReal.abs : EReal → ENNReal

The absolute value from EReal to ℝ≥0∞, mapping ⊥ and ⊤ to ⊤ and a real x to |x|.

Equations

• EReal.abs none = ⊤
• EReal.abs (some none) = ⊤
• EReal.abs (some (some x_1)) = ENNReal.ofReal |x_1|

@[simp]

theorem EReal.abs_top : ⊤.abs = ⊤

@[simp]

theorem EReal.abs_bot : ⊥.abs = ⊤

theorem EReal.abs_def (x : ℝ) : (↑x).abs = ENNReal.ofReal |x|

theorem EReal.abs_coe_lt_top (x : ℝ) : (↑x).abs < ⊤

@[simp]

theorem EReal.abs_eq_zero_iff {x : EReal} : x.abs = 0 ↔ x = 0

@[simp]

theorem EReal.abs_zero : EReal.abs 0 = 0

@[simp]

theorem EReal.coe_abs (x : ℝ) : ↑(↑x).abs = ↑|x|

@[simp]

theorem EReal.abs_neg (x : EReal) : (-x).abs = x.abs

@[simp]

theorem EReal.abs_mul (x y : EReal) : (x * y).abs = x.abs * y.abs

Sign

theorem EReal.sign_top : SignType.sign ⊤ = 1

theorem EReal.sign_bot : SignType.sign ⊥ = -1

@[simp]

theorem EReal.sign_coe (x : ℝ) : SignType.sign ↑x = SignType.sign x

@[simp]

theorem EReal.coe_coe_sign (x : SignType) : ↑↑x = ↑x

@[simp]

theorem EReal.sign_neg (x : EReal) : SignType.sign (-x) = -SignType.sign x

@[simp]

theorem EReal.sign_mul (x y : EReal) : SignType.sign (x * y) = SignType.sign x * SignType.sign y

@[simp]

theorem EReal.sign_mul_abs (x : EReal) : ↑(SignType.sign x) * ↑x.abs = x

@[simp]

theorem EReal.abs_mul_sign (x : EReal) : ↑x.abs * ↑(SignType.sign x) = x

theorem EReal.sign_eq_and_abs_eq_iff_eq {x y : EReal} : x.abs = y.abs ∧ SignType.sign x = SignType.sign y ↔ x = y

theorem EReal.le_iff_sign {x y : EReal} : x ≤ y ↔ SignType.sign x < SignType.sign y ∨ SignType.sign x = SignType.neg ∧ SignType.sign y = SignType.neg ∧ y.abs ≤ x.abs ∨ SignType.sign x = SignType.zero ∧ SignType.sign y = SignType.zero ∨ SignType.sign x = SignType.pos ∧ SignType.sign y = SignType.pos ∧ x.abs ≤ y.abs

instance EReal.instCommMonoidWithZero : CommMonoidWithZero EReal

Equations

• EReal.instCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯

instance EReal.instPosMulMono : PosMulMono EReal

instance EReal.instMulPosMono : MulPosMono EReal

instance EReal.instPosMulReflectLT : PosMulReflectLT EReal

instance EReal.instMulPosReflectLT : MulPosReflectLT EReal

@[simp]

theorem EReal.coe_pow (x : ℝ) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

@[simp]

theorem EReal.coe_ennreal_pow (x : ENNReal) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

Min and Max

theorem EReal.min_neg_neg (x y : EReal) : -x ⊓ -y = -(x ⊔ y)

theorem EReal.max_neg_neg (x y : EReal) : -x ⊔ -y = -(x ⊓ y)

Inverse

def EReal.inv : EReal → EReal

Multiplicative inverse of an EReal. We choose 0⁻¹ = 0 to guarantee several good properties, for instance (a * b)⁻¹ = a⁻¹ * b⁻¹.

Equations

• EReal.inv none = 0
• EReal.inv (some none) = 0
• EReal.inv (some (some x_1)) = ↑x_1⁻¹

instance EReal.instInv : Inv EReal

Equations

• EReal.instInv = { inv := EReal.inv }

noncomputable instance EReal.instDivInvMonoid : DivInvMonoid EReal

Equations

• EReal.instDivInvMonoid = DivInvMonoid.mk EReal.instDivInvMonoid.proof_1 zpowRec EReal.instDivInvMonoid.proof_2 EReal.instDivInvMonoid.proof_3 EReal.instDivInvMonoid.proof_4

@[simp]

theorem EReal.inv_bot : ⊥⁻¹ = 0

@[simp]

theorem EReal.inv_top : ⊤⁻¹ = 0

theorem EReal.coe_inv (x : ℝ) : ↑x⁻¹ = (↑x)⁻¹

@[simp]

theorem EReal.inv_zero : 0⁻¹ = 0

noncomputable instance EReal.instDivInvOneMonoid : DivInvOneMonoid EReal

Equations

• EReal.instDivInvOneMonoid = DivInvOneMonoid.mk EReal.instDivInvOneMonoid.proof_1

theorem EReal.inv_neg (a : EReal) : (-a)⁻¹ = -a⁻¹

theorem EReal.inv_inv {a : EReal} (h : a ≠ ⊥) (h' : a ≠ ⊤) : a⁻¹⁻¹ = a

theorem EReal.mul_inv (a b : EReal) : (a * b)⁻¹ = a⁻¹ * b⁻¹

Inversion and Absolute Value

theorem EReal.sign_mul_inv_abs (a : EReal) : ↑(SignType.sign a) * (↑a.abs)⁻¹ = a⁻¹

theorem EReal.sign_mul_inv_abs' (a : EReal) : ↑(SignType.sign a) * ↑a.abs⁻¹ = a⁻¹

Inversion and Positivity

theorem EReal.inv_nonneg_of_nonneg {a : EReal} (h : 0 ≤ a) : 0 ≤ a⁻¹

theorem EReal.inv_nonpos_of_nonpos {a : EReal} (h : a ≤ 0) : a⁻¹ ≤ 0

theorem EReal.inv_pos_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : 0 < a⁻¹

theorem EReal.inv_neg_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : a⁻¹ < 0

Division

theorem EReal.div_eq_inv_mul (a b : EReal) : a / b = b⁻¹ * a

theorem EReal.coe_div (a b : ℝ) : ↑(a / b) = ↑a / ↑b

theorem EReal.natCast_div_le (m n : ℕ) : ↑(m / n) ≤ ↑m / ↑n

@[simp]

theorem EReal.div_bot {a : EReal} : a / ⊥ = 0

@[simp]

theorem EReal.div_top {a : EReal} : a / ⊤ = 0

@[simp]

theorem EReal.div_zero {a : EReal} : a / 0 = 0

@[simp]

theorem EReal.zero_div {a : EReal} : 0 / a = 0

theorem EReal.top_div_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : ⊤ / a = ⊤

theorem EReal.top_div_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : ⊤ / a = ⊥

theorem EReal.bot_div_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : ⊥ / a = ⊥

theorem EReal.bot_div_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : ⊥ / a = ⊤

Division and Multiplication

theorem EReal.div_self {a : EReal} (h₁ : a ≠ ⊥) (h₂ : a ≠ ⊤) (h₃ : a ≠ 0) : a / a = 1

theorem EReal.mul_div (a b c : EReal) : a * (b / c) = a * b / c

theorem EReal.mul_div_right (a b c : EReal) : a / b * c = a * c / b

theorem EReal.div_div (a b c : EReal) : a / b / c = a / (b * c)

theorem EReal.div_mul_cancel {a b : EReal} (h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : a / b * b = a

theorem EReal.mul_div_cancel {a b : EReal} (h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : b * (a / b) = a

theorem EReal.mul_div_mul_cancel {a b c : EReal} (h₁ : c ≠ ⊥) (h₂ : c ≠ ⊤) (h₃ : c ≠ 0) : a * c / (b * c) = a / b

Division Distributivity

theorem EReal.div_right_distrib_of_nonneg {a b c : EReal} (h : 0 ≤ a) (h' : 0 ≤ b) : (a + b) / c = a / c + b / c

Division and Order

theorem EReal.monotone_div_right_of_nonneg {b : EReal} (h : 0 ≤ b) : Monotone fun (a : EReal) => a / b

theorem EReal.div_le_div_right_of_nonneg {a a' b : EReal} (h : 0 ≤ b) (h' : a ≤ a') : a / b ≤ a' / b

theorem EReal.strictMono_div_right_of_pos {b : EReal} (h : 0 < b) (h' : b ≠ ⊤) : StrictMono fun (a : EReal) => a / b

theorem EReal.div_lt_div_right_of_pos {a a' b : EReal} (h₁ : 0 < b) (h₂ : b ≠ ⊤) (h₃ : a < a') : a / b < a' / b

theorem EReal.antitone_div_right_of_nonpos {b : EReal} (h : b ≤ 0) : Antitone fun (a : EReal) => a / b

theorem EReal.div_le_div_right_of_nonpos {a a' b : EReal} (h : b ≤ 0) (h' : a ≤ a') : a' / b ≤ a / b

theorem EReal.strictAnti_div_right_of_neg {b : EReal} (h : b < 0) (h' : b ≠ ⊥) : StrictAnti fun (a : EReal) => a / b

theorem EReal.div_lt_div_right_of_neg {a a' b : EReal} (h₁ : b < 0) (h₂ : b ≠ ⊥) (h₃ : a < a') : a' / b < a / b

theorem EReal.le_div_iff_mul_le {a b c : EReal} (h : b > 0) (h' : b ≠ ⊤) : a ≤ c / b ↔ a * b ≤ c

theorem EReal.div_le_iff_le_mul {a b c : EReal} (h : 0 < b) (h' : b ≠ ⊤) : a / b ≤ c ↔ a ≤ b * c

theorem EReal.div_nonneg {a b : EReal} (h : 0 ≤ a) (h' : 0 ≤ b) : 0 ≤ a / b

theorem EReal.div_nonpos_of_nonpos_of_nonneg {a b : EReal} (h : a ≤ 0) (h' : 0 ≤ b) : a / b ≤ 0

theorem EReal.div_nonpos_of_nonneg_of_nonpos {a b : EReal} (h : 0 ≤ a) (h' : b ≤ 0) : a / b ≤ 0

theorem EReal.div_nonneg_of_nonpos_of_nonpos {a b : EReal} (h : a ≤ 0) (h' : b ≤ 0) : 0 ≤ a / b