mathlib3 documentation

data.real.ereal

The extended reals [-∞, ∞]. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Addition and multiplication are problematic in the presence of ±∞, but negation has a natural definition and satisfies the usual properties.

An ad hoc addition is defined, for which ereal is an add_comm_monoid, 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 comm_monoid_with_zero. 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.

ereal is a complete_linear_order; this is deduced by type class inference from the fact that with_bot (with_top 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

@[protected, instance]

def ereal.nontrivial :

nontrivial ereal

@[protected, instance]

def ereal.zero_le_one_class :

zero_le_one_class ereal

@[protected, instance]

def ereal.has_zero :

@[protected, instance]

noncomputable def ereal.linear_ordered_add_comm_monoid :

linear_ordered_add_comm_monoid ereal

@[protected, instance]

noncomputable def ereal.has_Sup :

@[protected, instance]

def ereal.add_monoid :

add_monoid ereal

@[protected, instance]

noncomputable def ereal.has_Inf :

@[protected, instance]

def ereal.has_one :

@[protected, instance]

noncomputable def ereal.complete_linear_order :

complete_linear_order ereal

def ereal :

ereal : The type [-∞, ∞]

Equations

ereal = with_bot (with_top ℝ)

Instances for ereal

@[protected, instance]

def ereal.has_bot :

def real.to_ereal :

The canonical inclusion froms reals to ereals. Do not use directly: as this is registered as a coercion, use the coercion instead.

Equations

real.to_ereal = option.some ∘ option.some

@[protected, instance]

noncomputable def ereal.decidable_lt :

decidable_rel has_lt.lt

Equations

ereal.decidable_lt = with_bot.decidable_lt

@[protected, instance]

def ereal.has_top :

Equations

ereal.has_top = {top := option.some ⊤}

@[protected, instance]

def ereal.has_coe :

has_coe ℝ ereal

Equations

ereal.has_coe = {coe := real.to_ereal}

theorem ereal.coe_strict_mono :

strict_mono coe

theorem ereal.coe_injective :

function.injective coe

@[protected, simp, norm_cast]

theorem ereal.coe_le_coe_iff {x y : ℝ} :

↑x ≤ ↑y ↔ x ≤ y

@[protected, simp, norm_cast]

theorem ereal.coe_lt_coe_iff {x y : ℝ} :

↑x < ↑y ↔ x < y

@[protected, simp, norm_cast]

theorem ereal.coe_eq_coe_iff {x y : ℝ} :

↑x = ↑y ↔ x = y

@[protected]

theorem ereal.coe_ne_coe_iff {x y : ℝ} :

↑x ≠ ↑y ↔ x ≠ y

def ennreal.to_ereal :

ennreal → ereal

The canonical map from nonnegative extended reals to extended reals

Equations

ennreal.to_ereal (option.some x) = ↑(x.val)
⊤.to_ereal = ⊤

@[protected, instance]

def ereal.has_coe_ennreal :

has_coe ennreal ereal

Equations

ereal.has_coe_ennreal = {coe := ennreal.to_ereal}

@[protected, instance]

def ereal.inhabited :

inhabited ereal

Equations

ereal.inhabited = {default := 0}

@[simp, norm_cast]

theorem ereal.coe_zero :

↑0 = 0

@[simp, norm_cast]

theorem ereal.coe_one :

↑1 = 1

@[protected]

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.

A typical invocation looks like induction x using ereal.rec. Note that using induction directly will unfold ereal to option which is undesirable.

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

Equations

ereal.rec h_bot h_real h_top ↑a = h_real a
ereal.rec h_bot h_real h_top ⊤ = h_top
ereal.rec h_bot h_real h_top ⊥ = h_bot

@[protected]

noncomputable 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

↑x.mul ↑y = ↑(x * y)
↑x.mul ⊤ = ite (0 < x) ⊤ (ite (x = 0) 0 ⊥)
↑x.mul ⊥ = ite (0 < x) ⊥ (ite (x = 0) 0 ⊤)
⊤.mul ↑y = ite (0 < y) ⊤ (ite (y = 0) 0 ⊥)
⊤.mul ⊤ = ⊤
⊤.mul ⊥ = ⊥
⊥.mul ↑y = ite (0 < y) ⊥ (ite (y = 0) 0 ⊤)
⊥.mul ⊤ = ⊥
⊥.mul ⊥ = ⊤

@[protected, instance]

noncomputable def ereal.has_mul :

Equations

ereal.has_mul = {mul := ereal.mul}

theorem ereal.induction₂ {P : ereal → ereal → Prop} (top_top : P ⊤ ⊤) (top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x) (top_zero : P ⊤ 0) (top_neg : ∀ (x : ℝ), 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 : ℝ), x < 0 → P ↑x ⊤) (neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥) (bot_top : P ⊥ ⊤) (bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x) (bot_zero : P ⊥ 0) (bot_neg : ∀ (x : ℝ), 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.

ereal with its multiplication is a comm_monoid_with_zero. 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.

@[protected, instance]

noncomputable def ereal.mul_zero_one_class :

mul_zero_one_class ereal

Equations

ereal.mul_zero_one_class = {one := 1, mul := has_mul.mul ereal.has_mul, one_mul := ereal.mul_zero_one_class._proof_1, mul_one := ereal.mul_zero_one_class._proof_2, zero := 0, zero_mul := ereal.mul_zero_one_class._proof_3, mul_zero := ereal.mul_zero_one_class._proof_4}

Real coercion #

@[protected, instance]

def ereal.can_lift :

can_lift ereal ℝ coe (λ (r : ereal), r ≠ ⊤ ∧ r ≠ ⊥)

Equations

ereal.can_lift = {prf := ereal.can_lift._proof_1}

def ereal.to_real :

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

Equations

@[simp]

theorem ereal.to_real_top :

⊤.to_real = 0

@[simp]

theorem ereal.to_real_bot :

⊥.to_real = 0

@[simp]

theorem ereal.to_real_zero :

@[simp]

theorem ereal.to_real_one :

@[simp]

theorem ereal.to_real_coe (x : ℝ) :

↑x.to_real = x

@[simp]

theorem ereal.bot_lt_coe (x : ℝ) :

@[simp]

theorem ereal.coe_ne_bot (x : ℝ) :

@[simp]

theorem ereal.bot_ne_coe (x : ℝ) :

@[simp]

theorem ereal.coe_lt_top (x : ℝ) :

@[simp]

theorem ereal.coe_ne_top (x : ℝ) :

@[simp]

theorem ereal.top_ne_coe (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 :

@[simp, norm_cast]

theorem ereal.coe_add (x y : ℝ) :

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

@[simp, norm_cast]

theorem ereal.coe_mul (x y : ℝ) :

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

@[norm_cast]

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

↑(n • x) = n • ↑x

@[simp, norm_cast]

theorem ereal.coe_bit0 (x : ℝ) :

↑(bit0 x) = bit0 ↑x

@[simp, norm_cast]

theorem ereal.coe_bit1 (x : ℝ) :

↑(bit1 x) = bit1 ↑x

@[simp, norm_cast]

theorem ereal.coe_eq_zero {x : ℝ} :

↑x = 0 ↔ x = 0

@[simp, norm_cast]

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

@[protected, simp, norm_cast]

theorem ereal.coe_nonneg {x : ℝ} :

0 ≤ ↑x ↔ 0 ≤ x

@[protected, simp, norm_cast]

theorem ereal.coe_nonpos {x : ℝ} :

↑x ≤ 0 ↔ x ≤ 0

@[protected, simp, norm_cast]

theorem ereal.coe_pos {x : ℝ} :

0 < ↑x ↔ 0 < x

@[protected, simp, norm_cast]

theorem ereal.coe_neg' {x : ℝ} :

↑x < 0 ↔ x < 0

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

x.to_real ≤ y.to_real

theorem ereal.coe_to_real {x : ereal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) :

↑(x.to_real) = x

theorem ereal.le_coe_to_real {x : ereal} (h : x ≠ ⊤) :

x ≤ ↑(x.to_real)

theorem ereal.coe_to_real_le {x : ereal} (h : x ≠ ⊥) :

↑(x.to_real) ≤ 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

ennreal coercion #

@[simp]

theorem ereal.to_real_coe_ennreal {x : ennreal} :

↑x.to_real = x.to_real

@[simp]

theorem ereal.coe_ennreal_of_real {x : ℝ} :

↑(ennreal.of_real x) = linear_order.max ↑x 0

theorem ereal.coe_nnreal_eq_coe_real (x : nnreal) :

↑↑x = ↑↑x

@[simp, norm_cast]

theorem ereal.coe_ennreal_zero :

↑0 = 0

@[simp, norm_cast]

theorem ereal.coe_ennreal_one :

↑1 = 1

@[simp, norm_cast]

theorem ereal.coe_ennreal_top :

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

theorem ereal.coe_ennreal_strict_mono :

strict_mono coe

theorem ereal.coe_ennreal_injective :

function.injective coe

@[simp, norm_cast]

theorem ereal.coe_ennreal_le_coe_ennreal_iff {x y : ennreal} :

↑x ≤ ↑y ↔ x ≤ y

@[simp, norm_cast]

theorem ereal.coe_ennreal_lt_coe_ennreal_iff {x y : ennreal} :

↑x < ↑y ↔ x < y

@[simp, norm_cast]

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, norm_cast]

theorem ereal.coe_ennreal_eq_zero {x : ennreal} :

↑x = 0 ↔ x = 0

@[simp, norm_cast]

theorem ereal.coe_ennreal_eq_one {x : ennreal} :

↑x = 1 ↔ x = 1

@[norm_cast]

theorem ereal.coe_ennreal_ne_zero {x : ennreal} :

↑x ≠ 0 ↔ x ≠ 0

@[norm_cast]

theorem ereal.coe_ennreal_ne_one {x : ennreal} :

↑x ≠ 1 ↔ x ≠ 1

theorem ereal.coe_ennreal_nonneg (x : ennreal) :

@[simp, norm_cast]

theorem ereal.coe_ennreal_pos {x : ennreal} :

0 < ↑x ↔ 0 < x

@[simp]

theorem ereal.bot_lt_coe_ennreal (x : ennreal) :

@[simp]

theorem ereal.coe_ennreal_ne_bot (x : ennreal) :

@[simp, norm_cast]

theorem ereal.coe_ennreal_add (x y : ennreal) :

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

@[simp, norm_cast]

theorem ereal.coe_ennreal_mul (x y : ennreal) :

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

@[norm_cast]

theorem ereal.coe_ennreal_nsmul (n : ℕ) (x : ennreal) :

↑(n • x) = n • ↑x

@[simp, norm_cast]

theorem ereal.coe_ennreal_bit0 (x : ennreal) :

↑(bit0 x) = bit0 ↑x

@[simp, norm_cast]

theorem ereal.coe_ennreal_bit1 (x : ennreal) :

↑(bit1 x) = bit1 ↑x

Order #

theorem ereal.exists_rat_btwn_of_lt {a b : ereal} (hab : 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.ne_top_bot_equiv_real :

↥{⊥, ⊤}ᶜ ≃ ℝ

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

Equations

ereal.ne_top_bot_equiv_real = {to_fun := λ (x : ↥{⊥, ⊤}ᶜ), ↑x.to_real, inv_fun := λ (x : ℝ), ⟨↑x, _⟩, left_inv := ereal.ne_top_bot_equiv_real._proof_2, right_inv := ereal.ne_top_bot_equiv_real._proof_3}

Addition #

@[simp]

theorem ereal.add_bot (x : ereal) :

@[simp]

theorem ereal.bot_add (x : ereal) :

@[simp]

theorem ereal.top_add_top :

⊤ + ⊤ = ⊤

@[simp]

theorem ereal.top_add_coe (x : ℝ) :

⊤ + ↑x = ⊤

@[simp]

theorem ereal.coe_add_top (x : ℝ) :

↑x + ⊤ = ⊤

theorem ereal.to_real_add {x y : ereal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) :

(x + y).to_real = x.to_real + y.to_real

theorem ereal.add_lt_add_right_coe {x y : ereal} (h : x < y) (z : ℝ) :

x + ↑z < y + ↑z

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

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

@[simp]

theorem ereal.add_eq_bot_iff {x y : ereal} :

x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

@[simp]

theorem ereal.bot_lt_add_iff {x y : ereal} :

⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

theorem ereal.add_lt_top {x y : ereal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :

x + y < ⊤

Negation #

@[protected]

def ereal.neg :

ereal → ereal

negation on ereal

Equations

@[protected, instance]

def ereal.has_neg :

Equations

ereal.has_neg = {neg := ereal.neg}

@[protected, instance]

def ereal.sub_neg_zero_monoid :

sub_neg_zero_monoid ereal

Equations

ereal.sub_neg_zero_monoid = {add := add_monoid.add ereal.add_monoid, add_assoc := _, zero := add_monoid.zero ereal.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul ereal.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg ereal.has_neg, sub := sub_neg_monoid.sub._default add_monoid.add add_monoid.add_assoc add_monoid.zero add_monoid.zero_add add_monoid.add_zero add_monoid.nsmul add_monoid.nsmul_zero' add_monoid.nsmul_succ' has_neg.neg, sub_eq_add_neg := ereal.sub_neg_zero_monoid._proof_1, zsmul := sub_neg_monoid.zsmul._default add_monoid.add add_monoid.add_assoc add_monoid.zero add_monoid.zero_add add_monoid.add_zero add_monoid.nsmul add_monoid.nsmul_zero' add_monoid.nsmul_succ' has_neg.neg, zsmul_zero' := ereal.sub_neg_zero_monoid._proof_2, zsmul_succ' := ereal.sub_neg_zero_monoid._proof_3, zsmul_neg' := ereal.sub_neg_zero_monoid._proof_4, neg_zero := ereal.sub_neg_zero_monoid._proof_5}

@[protected, norm_cast]

theorem ereal.neg_def (x : ℝ) :

@[simp]

theorem ereal.neg_top :

@[simp]

theorem ereal.neg_bot :

@[simp, norm_cast]

theorem ereal.coe_neg (x : ℝ) :

@[simp, norm_cast]

theorem ereal.coe_sub (x y : ℝ) :

↑(x - y) = ↑x - ↑y

@[norm_cast]

theorem ereal.coe_zsmul (n : ℤ) (x : ℝ) :

↑(n • x) = n • ↑x

@[protected, instance]

def ereal.has_involutive_neg :

has_involutive_neg ereal

Equations

ereal.has_involutive_neg = {neg := has_neg.neg ereal.has_neg, neg_neg := ereal.has_involutive_neg._proof_1}

@[simp]

theorem ereal.to_real_neg {a : ereal} :

(-a).to_real = -a.to_real

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

@[protected]

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

-b ≤ a

if -a ≤ b then -b ≤ a on ereal.

@[protected]

theorem ereal.neg_le {a b : ereal} :

-a ≤ b ↔ -b ≤ a

-a ≤ b ↔ -b ≤ a on ereal.

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

b ≤ -a

a ≤ -b → b ≤ -a on ereal

@[simp]

theorem ereal.neg_le_neg_iff {a b : ereal} :

-a ≤ -b ↔ b ≤ a

def ereal.neg_order_iso :

ereal ≃o ereal ᵒᵈ

Negation as an order reversing isomorphism on ereal.

Equations

ereal.neg_order_iso = {to_equiv := {to_fun := λ (x : ereal), ⇑order_dual.to_dual (-x), inv_fun := λ (x : ereal ᵒᵈ), -⇑order_dual.of_dual x, left_inv := ereal.neg_order_iso._proof_1, right_inv := ereal.neg_order_iso._proof_2}, map_rel_iff' := ereal.neg_order_iso._proof_3}

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

-b < a

theorem ereal.neg_lt_iff_neg_lt {a b : ereal} :

-a < b ↔ -b < a

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 sub_neg_zero_monoid, because of this bad behavior.

@[simp]

theorem ereal.bot_sub (x : ereal) :

@[simp]

theorem ereal.sub_top (x : ereal) :

@[simp]

theorem ereal.top_sub_bot :

⊤ - ⊥ = ⊤

@[simp]

theorem ereal.top_sub_coe (x : ℝ) :

⊤ - ↑x = ⊤

@[simp]

theorem ereal.coe_sub_bot (x : ℝ) :

↑x - ⊥ = ⊤

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_to_nnreal_sub_coe_to_nnreal (x : ℝ) :

↑x = ↑(x.to_nnreal) - ↑((-x).to_nnreal)

theorem ereal.to_real_sub {x y : ereal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) :

(x - y).to_real = x.to_real - y.to_real

Multiplication #

@[protected]

theorem ereal.mul_comm (x y : ereal) :

x * y = y * x

@[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.mul_top_of_pos {x : ereal} (h : 0 < x) :

theorem ereal.mul_top_of_neg {x : ereal} (h : x < 0) :

theorem ereal.top_mul_of_pos {x : ereal} (h : 0 < x) :

theorem ereal.top_mul_of_neg {x : ereal} (h : x < 0) :

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_bot_of_pos {x : ereal} (h : 0 < x) :

theorem ereal.mul_bot_of_neg {x : ereal} (h : x < 0) :

theorem ereal.bot_mul_of_pos {x : ereal} (h : 0 < x) :

theorem ereal.bot_mul_of_neg {x : ereal} (h : x < 0) :

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.to_real_mul {x y : ereal} :

(x * y).to_real = x.to_real * y.to_real

@[protected]

theorem ereal.neg_mul (x y : ereal) :

-x * y = -(x * y)

@[protected, instance]

def ereal.has_distrib_neg :

has_distrib_neg ereal

Equations

ereal.has_distrib_neg = {neg := has_involutive_neg.neg ereal.has_involutive_neg, neg_neg := _, neg_mul := ereal.neg_mul, mul_neg := ereal.has_distrib_neg._proof_1}

Absolute value #

@[protected]

noncomputable def ereal.abs :

ereal → ennreal

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

Equations

@[simp]

theorem ereal.abs_top :

@[simp]

theorem ereal.abs_bot :

theorem ereal.abs_def (x : ℝ) :

↑x.abs = ennreal.of_real |x|

theorem ereal.abs_coe_lt_top (x : ℝ) :

@[simp]

theorem ereal.abs_eq_zero_iff {x : ereal} :

x.abs = 0 ↔ x = 0

@[simp]

theorem ereal.abs_zero :

0.abs = 0

@[simp]

theorem ereal.coe_abs (x : ℝ) :

↑(↑x.abs) = ↑|x|

@[simp]

theorem ereal.abs_mul (x y : ereal) :

(x * y).abs = x.abs * y.abs

Sign #

@[simp]

theorem ereal.sign_top :

⇑sign ⊤ = 1

@[simp]

theorem ereal.sign_bot :

⇑sign ⊥ = -1

@[simp]

theorem ereal.sign_coe (x : ℝ) :

⇑sign ↑x = ⇑sign x

@[simp]

theorem ereal.sign_mul (x y : ereal) :

⇑sign (x * y) = ⇑sign x * ⇑sign y

theorem ereal.sign_mul_abs (x : ereal) :

↑(⇑sign x) * ↑(x.abs) = x

theorem ereal.sign_eq_and_abs_eq_iff_eq {x y : ereal} :

x.abs = y.abs ∧ ⇑sign x = ⇑sign y ↔ x = y

theorem ereal.le_iff_sign {x y : ereal} :

x ≤ y ↔ ⇑sign x < ⇑sign y ∨ ⇑sign x = sign_type.neg ∧ ⇑sign y = sign_type.neg ∧ y.abs ≤ x.abs ∨ ⇑sign x = sign_type.zero ∧ ⇑sign y = sign_type.zero ∨ ⇑sign x = sign_type.pos ∧ ⇑sign y = sign_type.pos ∧ x.abs ≤ y.abs

@[protected, instance]

noncomputable def ereal.comm_monoid_with_zero :

comm_monoid_with_zero ereal

Equations

ereal.comm_monoid_with_zero = {mul := has_mul.mul ereal.has_mul, mul_assoc := ereal.comm_monoid_with_zero._proof_1, one := 1, one_mul := _, mul_one := _, npow := comm_monoid.npow._default 1 has_mul.mul mul_zero_one_class.one_mul mul_zero_one_class.mul_one, npow_zero' := ereal.comm_monoid_with_zero._proof_2, npow_succ' := ereal.comm_monoid_with_zero._proof_3, mul_comm := ereal.mul_comm, zero := 0, zero_mul := _, mul_zero := _}

@[protected, instance]

def ereal.pos_mul_mono :

pos_mul_mono ereal

@[protected, instance]

def ereal.mul_pos_mono :

mul_pos_mono ereal

@[protected, instance]

def ereal.pos_mul_reflect_lt :

pos_mul_reflect_lt ereal

@[protected, instance]

def ereal.mul_pos_reflect_lt :

mul_pos_reflect_lt ereal

@[simp, norm_cast]

theorem ereal.coe_pow (x : ℝ) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

@[simp, norm_cast]

theorem ereal.coe_ennreal_pow (x : ennreal) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

meta def tactic.positivity_coe_real_ereal :

expr → tactic tactic.positivity.strictness

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

meta def tactic.positivity_coe_ennreal_ereal :

expr → tactic tactic.positivity.strictness

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