Documentation

Mathlib.Data.ENNReal.Operations

Properties of addition, multiplication and subtraction on extended non-negative real numbers #

In this file we prove elementary properties of algebraic operations on ℝ≥0∞, including addition, multiplication, natural powers and truncated subtraction, as well as how these interact with the order structure on ℝ≥0∞. Notably excluded from this list are inversion and division, the definitions and properties of which can be found in Data.ENNReal.Inv.

Note: the definitions of the operations included in this file can be found in Data.ENNReal.Basic.

theorem ENNReal.mul_lt_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (ac : a < c) (bd : b < d) :
a * b < c * d
theorem ENNReal.mul_left_mono {a : ENNReal} :
Monotone fun (x : ENNReal) => a * x
theorem ENNReal.mul_right_mono {a : ENNReal} :
Monotone fun (x : ENNReal) => x * a
theorem ENNReal.pow_strictMono {n : } :
n 0StrictMono fun (x : ENNReal) => x ^ n
theorem ENNReal.pow_lt_pow_left {a : ENNReal} {b : ENNReal} (h : a < b) {n : } (hn : n 0) :
a ^ n < b ^ n
theorem ENNReal.max_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} :
max a b * c = max (a * c) (b * c)
theorem ENNReal.mul_max {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a * max b c = max (a * b) (a * c)
theorem ENNReal.mul_left_strictMono {a : ENNReal} (h0 : a 0) (hinf : a ) :
StrictMono fun (x : ENNReal) => a * x
theorem ENNReal.mul_lt_mul_left' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a 0) (hinf : a ) (bc : b < c) :
a * b < a * c
theorem ENNReal.mul_lt_mul_right' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a 0) (hinf : a ) (bc : b < c) :
b * a < c * a
theorem ENNReal.mul_eq_mul_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a 0) (hinf : a ) :
a * b = a * c b = c
theorem ENNReal.mul_eq_mul_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :
c 0c (a * c = b * c a = b)
theorem ENNReal.mul_le_mul_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a 0) (hinf : a ) :
a * b a * c b c
theorem ENNReal.mul_le_mul_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :
c 0c (a * c b * c a b)
theorem ENNReal.mul_lt_mul_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a 0) (hinf : a ) :
a * b < a * c b < c
theorem ENNReal.mul_lt_mul_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :
c 0c (a * c < b * c a < b)
theorem ENNReal.pow_pos {a : ENNReal} :
0 < a∀ (n : ), 0 < a ^ n
theorem ENNReal.pow_ne_zero {a : ENNReal} :
a 0∀ (n : ), a ^ n 0
theorem ENNReal.le_of_add_le_add_left {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a a + b a + cb c
theorem ENNReal.le_of_add_le_add_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a b + a c + ab c
theorem ENNReal.add_lt_add_left {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a b < ca + b < a + c
theorem ENNReal.add_lt_add_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a b < cb + a < c + a
theorem ENNReal.add_le_add_iff_left {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a (a + b a + c b c)
theorem ENNReal.add_le_add_iff_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a (b + a c + a b c)
theorem ENNReal.add_lt_add_iff_left {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a (a + b < a + c b < c)
theorem ENNReal.add_lt_add_iff_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a (b + a < c + a b < c)
theorem ENNReal.add_lt_add_of_le_of_lt {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} :
a a bc < da + c < b + d
theorem ENNReal.add_lt_add_of_lt_of_le {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} :
c a < bc da + c < b + d
theorem ENNReal.lt_add_right {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b 0) :
a < a + b
@[simp]
theorem ENNReal.add_eq_top {a : ENNReal} {b : ENNReal} :
a + b = a = b =
@[simp]
theorem ENNReal.add_lt_top {a : ENNReal} {b : ENNReal} :
a + b < a < b <
theorem ENNReal.toNNReal_add {r₁ : ENNReal} {r₂ : ENNReal} (h₁ : r₁ ) (h₂ : r₂ ) :
(r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal
theorem ENNReal.mul_top' {a : ENNReal} :
a * = if a = 0 then 0 else
@[simp]
theorem ENNReal.mul_top {a : ENNReal} (h : a 0) :
theorem ENNReal.top_mul' {a : ENNReal} :
* a = if a = 0 then 0 else
@[simp]
theorem ENNReal.top_mul {a : ENNReal} (h : a 0) :
theorem ENNReal.top_pow {n : } (n_pos : 0 < n) :
theorem ENNReal.mul_eq_top {a : ENNReal} {b : ENNReal} :
a * b = a 0 b = a = b 0
theorem ENNReal.mul_lt_top {a : ENNReal} {b : ENNReal} :
a < b < a * b <
theorem ENNReal.mul_ne_top {a : ENNReal} {b : ENNReal} :
a b a * b
theorem ENNReal.lt_top_of_mul_ne_top_left {a : ENNReal} {b : ENNReal} (h : a * b ) (hb : b 0) :
a <
theorem ENNReal.lt_top_of_mul_ne_top_right {a : ENNReal} {b : ENNReal} (h : a * b ) (ha : a 0) :
b <
theorem ENNReal.mul_lt_top_iff {a : ENNReal} {b : ENNReal} :
a * b < a < b < a = 0 b = 0
theorem ENNReal.mul_pos_iff {a : ENNReal} {b : ENNReal} :
0 < a * b 0 < a 0 < b
theorem ENNReal.mul_pos {a : ENNReal} {b : ENNReal} (ha : a 0) (hb : b 0) :
0 < a * b
@[simp]
theorem ENNReal.pow_eq_top_iff {a : ENNReal} {n : } :
a ^ n = a = n 0
theorem ENNReal.pow_eq_top {a : ENNReal} (n : ) (h : a ^ n = ) :
a =
theorem ENNReal.pow_ne_top {a : ENNReal} (h : a ) {n : } :
a ^ n
theorem ENNReal.pow_lt_top {a : ENNReal} :
a < ∀ (n : ), a ^ n <
@[simp]
theorem ENNReal.coe_finset_sum {α : Type u_1} {s : Finset α} {f : αNNReal} :
(∑ as, f a) = as, (f a)
@[simp]
theorem ENNReal.coe_finset_prod {α : Type u_1} {s : Finset α} {f : αNNReal} :
(∏ as, f a) = as, (f a)
theorem ENNReal.add_lt_add {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (ac : a < c) (bd : b < d) :
a + b < c + d
@[simp]

An element a is AddLECancellable if a + b ≤ a + c implies b ≤ c for all b and c. This is true in ℝ≥0∞ for all elements except .

This lemma has an abbreviated name because it is used frequently.

This lemma has an abbreviated name because it is used frequently.

theorem ENNReal.cancel_of_lt' {a : ENNReal} {b : ENNReal} (h : a < b) :

This lemma has an abbreviated name because it is used frequently.

This lemma has an abbreviated name because it is used frequently.

theorem ENNReal.add_right_inj {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ) :
a + b = a + c b = c
theorem ENNReal.add_left_inj {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ) :
b + a = c + a b = c
theorem ENNReal.sub_eq_sInf {a : ENNReal} {b : ENNReal} :
a - b = sInf {d : ENNReal | a d + b}
@[simp]
theorem ENNReal.coe_sub {r : NNReal} {p : NNReal} :
(r - p) = r - p

This is a special case of WithTop.coe_sub in the ENNReal namespace

@[simp]
theorem ENNReal.top_sub_coe {r : NNReal} :
- r =

This is a special case of WithTop.top_sub_coe in the ENNReal namespace

@[simp]
theorem ENNReal.top_sub {a : ENNReal} (ha : a ) :
theorem ENNReal.sub_top {a : ENNReal} :
a - = 0

This is a special case of WithTop.sub_top in the ENNReal namespace

@[simp]
theorem ENNReal.sub_eq_top_iff {a : ENNReal} {b : ENNReal} :
a - b = a = b
theorem ENNReal.sub_ne_top {a : ENNReal} {b : ENNReal} (ha : a ) :
a - b
@[simp]
theorem ENNReal.natCast_sub (m : ) (n : ) :
(m - n) = m - n
@[deprecated ENNReal.natCast_sub]
theorem ENNReal.nat_cast_sub (m : ) (n : ) :
(m - n) = m - n

Alias of ENNReal.natCast_sub.

theorem ENNReal.sub_eq_of_eq_add {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ) :
a = c + ba - b = c

See ENNReal.sub_eq_of_eq_add' for a version assuming that a = c + b itself is finite rather than b.

theorem ENNReal.sub_eq_of_eq_add' {a : ENNReal} {b : ENNReal} {c : ENNReal} (ha : a ) :
a = c + ba - b = c

Weaker version of ENNReal.sub_eq_of_eq_add assuming that a = c + b itself is finite rather han b.

theorem ENNReal.eq_sub_of_add_eq {a : ENNReal} {b : ENNReal} {c : ENNReal} (hc : c ) :
a + c = ba = b - c

See ENNReal.eq_sub_of_add_eq' for a version assuming that b = a + c itself is finite rather than c.

theorem ENNReal.eq_sub_of_add_eq' {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ) :
a + c = ba = b - c

Weaker version of ENNReal.eq_sub_of_add_eq assuming that b = a + c itself is finite rather than c.

theorem ENNReal.sub_eq_of_eq_add_rev {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ) :
a = b + ca - b = c

See ENNReal.sub_eq_of_eq_add_rev' for a version assuming that a = b + c itself is finite rather than b.

theorem ENNReal.sub_eq_of_eq_add_rev' {a : ENNReal} {b : ENNReal} {c : ENNReal} (ha : a ) :
a = b + ca - b = c

Weaker version of ENNReal.sub_eq_of_eq_add_rev assuming that a = b + c itself is finite rather than b.

@[deprecated ENNReal.sub_eq_of_eq_add]
theorem ENNReal.sub_eq_of_add_eq {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ) (hc : a + b = c) :
c - b = a
@[simp]
theorem ENNReal.add_sub_cancel_left {a : ENNReal} {b : ENNReal} (ha : a ) :
a + b - a = b
@[simp]
theorem ENNReal.add_sub_cancel_right {a : ENNReal} {b : ENNReal} (hb : b ) :
a + b - b = a
theorem ENNReal.sub_add_eq_add_sub {a : ENNReal} {b : ENNReal} {c : ENNReal} (hab : b a) (b_ne_top : b ) :
a - b + c = a + c - b
theorem ENNReal.lt_add_of_sub_lt_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a b ) :
a - b < ca < b + c
theorem ENNReal.lt_add_of_sub_lt_right {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a c ) :
a - c < ba < b + c
theorem ENNReal.le_sub_of_add_le_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (ha : a ) :
a + b cb c - a
theorem ENNReal.le_sub_of_add_le_right {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ) :
a + b ca c - b
theorem ENNReal.sub_lt_of_lt_add {a : ENNReal} {b : ENNReal} {c : ENNReal} (hac : c a) (h : a < b + c) :
a - c < b
theorem ENNReal.sub_lt_iff_lt_right {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ) (hab : b a) :
a - b < c a < c + b
theorem ENNReal.sub_lt_self {a : ENNReal} {b : ENNReal} (ha : a ) (ha₀ : a 0) (hb : b 0) :
a - b < a
theorem ENNReal.sub_lt_self_iff {a : ENNReal} {b : ENNReal} (ha : a ) :
a - b < a 0 < a 0 < b
theorem ENNReal.sub_lt_of_sub_lt {a : ENNReal} {b : ENNReal} {c : ENNReal} (h₂ : c a) (h₃ : a b ) (h₁ : a - b < c) :
a - c < b
theorem ENNReal.sub_sub_cancel {a : ENNReal} {b : ENNReal} (h : a ) (h2 : b a) :
a - (a - b) = b
theorem ENNReal.sub_right_inj {a : ENNReal} {b : ENNReal} {c : ENNReal} (ha : a ) (hb : b a) (hc : c a) :
a - b = a - c b = c
theorem ENNReal.sub_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : 0 < bb < ac ) :
(a - b) * c = a * c - b * c
theorem ENNReal.mul_sub {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : 0 < cc < ba ) :
a * (b - c) = a * b - a * c
theorem ENNReal.sub_le_sub_iff_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : c a) (h' : a ) :
a - b a - c c b
theorem ENNReal.prod_ne_top {α : Type u_1} {s : Finset α} {f : αENNReal} (h : as, f a ) :
as, f a

A product of finite numbers is still finite.

theorem ENNReal.prod_lt_top {α : Type u_1} {s : Finset α} {f : αENNReal} (h : as, f a < ) :
as, f a <

A product of finite numbers is still finite.

@[simp]
theorem ENNReal.sum_eq_top {α : Type u_1} {s : Finset α} {f : αENNReal} :
xs, f x = as, f a =

A sum is infinite iff one of the summands is infinite.

theorem ENNReal.sum_ne_top {α : Type u_1} {s : Finset α} {f : αENNReal} :
as, f a as, f a

A sum is finite iff all summands are finite.

@[simp]
theorem ENNReal.sum_lt_top {α : Type u_1} {s : Finset α} {f : αENNReal} :
as, f a < as, f a <

A sum is finite iff all summands are finite.

@[deprecated ENNReal.sum_lt_top]
theorem ENNReal.sum_lt_top_iff {α : Type u_1} {s : Finset α} {f : αENNReal} :
as, f a < as, f a <

Alias of ENNReal.sum_lt_top.


A sum is finite iff all summands are finite.

theorem ENNReal.lt_top_of_sum_ne_top {α : Type u_1} {s : Finset α} {f : αENNReal} (h : xs, f x ) {a : α} (ha : a s) :
f a <
theorem ENNReal.toNNReal_sum {α : Type u_1} {s : Finset α} {f : αENNReal} (hf : as, f a ) :
(∑ as, f a).toNNReal = as, (f a).toNNReal

Seeing ℝ≥0∞ as ℝ≥0 does not change their sum, unless one of the ℝ≥0∞ is infinity

theorem ENNReal.toReal_sum {α : Type u_1} {s : Finset α} {f : αENNReal} (hf : as, f a ) :
(∑ as, f a).toReal = as, (f a).toReal

seeing ℝ≥0∞ as Real does not change their sum, unless one of the ℝ≥0∞ is infinity

theorem ENNReal.ofReal_sum_of_nonneg {α : Type u_1} {s : Finset α} {f : α} (hf : is, 0 f i) :
ENNReal.ofReal (∑ is, f i) = is, ENNReal.ofReal (f i)
theorem ENNReal.sum_lt_sum_of_nonempty {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f : αENNReal} {g : αENNReal} (Hlt : is, f i < g i) :
is, f i < is, g i
theorem ENNReal.exists_le_of_sum_le {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f : αENNReal} {g : αENNReal} (Hle : is, f i is, g i) :
is, f i g i
theorem ENNReal.mem_Iio_self_add {x : ENNReal} {ε : ENNReal} :
x ε 0x Set.Iio (x + ε)
theorem ENNReal.mem_Ioo_self_sub_add {x : ENNReal} {ε₁ : ENNReal} {ε₂ : ENNReal} :
x x 0ε₁ 0ε₂ 0x Set.Ioo (x - ε₁) (x + ε₂)
noncomputable instance ENNReal.instMulActionNNReal {M : Type u_1} [MulAction ENNReal M] :

A MulAction over ℝ≥0∞ restricts to a MulAction over ℝ≥0.

Equations
theorem ENNReal.smul_def {M : Type u_1} [MulAction ENNReal M] (c : NNReal) (x : M) :
c x = c x
Equations
  • =
Equations
  • =
Equations
  • =

A DistribMulAction over ℝ≥0∞ restricts to a DistribMulAction over ℝ≥0.

Equations
noncomputable instance ENNReal.instModuleNNReal {M : Type u_1} [AddCommMonoid M] [Module ENNReal M] :

A Module over ℝ≥0∞ restricts to a Module over ℝ≥0.

Equations
noncomputable instance ENNReal.instAlgebraNNReal {A : Type u_1} [Semiring A] [Algebra ENNReal A] :

An Algebra over ℝ≥0∞ restricts to an Algebra over ℝ≥0.

Equations
theorem ENNReal.coe_smul {R : Type u_1} (r : R) (s : NNReal) [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal NNReal] [IsScalarTower R NNReal ENNReal] :
(r s) = r s
theorem ENNReal.smul_top {R : Type u_1} [Zero R] [SMulWithZero R ENNReal] [IsScalarTower R ENNReal ENNReal] [NoZeroSMulDivisors R ENNReal] [DecidableEq R] (c : R) :
c = if c = 0 then 0 else
theorem ENNReal.nnreal_smul_lt_top {x : NNReal} {y : ENNReal} (hy : y < ) :
x y <
theorem ENNReal.nnreal_smul_ne_top {x : NNReal} {y : ENNReal} (hy : y ) :
x y
theorem ENNReal.nnreal_smul_ne_top_iff {x : NNReal} {y : ENNReal} (hx : x 0) :
theorem ENNReal.nnreal_smul_lt_top_iff {x : NNReal} {y : ENNReal} (hx : x 0) :
x y < y <