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 : } (h : 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} :
(Finset.sum s fun (a : α) => f a) = Finset.sum s fun (a : α) => (f a)
@[simp]
theorem ENNReal.coe_finset_prod {α : Type u_1} {s : Finset α} {f : αNNReal} :
(Finset.prod s fun (a : α) => f a) = Finset.prod s fun (a : α) => (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

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

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.nat_cast_sub (m : ) (n : ) :
(m - n) = m - n
theorem ENNReal.sub_eq_of_eq_add {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ) :
a = c + ba - b = c
theorem ENNReal.eq_sub_of_add_eq {a : ENNReal} {b : ENNReal} {c : ENNReal} (hc : c ) :
a + c = ba = b - c
theorem ENNReal.sub_eq_of_eq_add_rev {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ) :
a = b + ca - b = c
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.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_lt_top {α : Type u_1} {s : Finset α} {f : αENNReal} (h : as, f a ) :
(Finset.prod s fun (a : α) => f a) <

A product of finite numbers is still finite

theorem ENNReal.sum_lt_top {α : Type u_1} {s : Finset α} {f : αENNReal} (h : as, f a ) :
(Finset.sum s fun (a : α) => f a) <

A sum of finite numbers is still finite

theorem ENNReal.sum_lt_top_iff {α : Type u_1} {s : Finset α} {f : αENNReal} :
(Finset.sum s fun (a : α) => f a) < as, f a <

A sum of finite numbers is still finite

theorem ENNReal.sum_eq_top_iff {α : Type u_1} {s : Finset α} {f : αENNReal} :
(Finset.sum s fun (x : α) => f x) = ∃ a ∈ s, f a =

A sum of numbers is infinite iff one of them is infinite

theorem ENNReal.lt_top_of_sum_ne_top {α : Type u_1} {s : Finset α} {f : αENNReal} (h : (Finset.sum s fun (x : α) => f x) ) {a : α} (ha : a s) :
f a <
theorem ENNReal.toNNReal_sum {α : Type u_1} {s : Finset α} {f : αENNReal} (hf : as, f a ) :
(Finset.sum s fun (a : α) => f a).toNNReal = Finset.sum s fun (a : α) => (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 ) :
(Finset.sum s fun (a : α) => f a).toReal = Finset.sum s fun (a : α) => (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 (Finset.sum s fun (i : α) => f i) = Finset.sum s fun (i : α) => 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) :
(Finset.sum s fun (i : α) => f i) < Finset.sum s fun (i : α) => g i
theorem ENNReal.exists_le_of_sum_le {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f : αENNReal} {g : αENNReal} (Hle : (Finset.sum s fun (i : α) => f i) Finset.sum s fun (i : α) => g i) :
∃ i ∈ s, 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 + ε₂)

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
  • =

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

Equations

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

Equations

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