# Documentation

Mathlib.Data.Real.ENNReal

# Extended non-negative reals #

We define ENNReal = ℝ≥0∞ := WithTop ℝ≥0 to be the type of extended nonnegative real numbers, i.e., the interval [0, +∞]. This type is used as the codomain of a MeasureTheory.Measure, and of the extended distance edist in an EMetricSpace. In this file we define some algebraic operations and a linear order on ℝ≥0∞ and prove basic properties of these operations, order, and conversions to/from ℝ, ℝ≥0, and ℕ.

## Main definitions #

• ℝ≥0∞: the extended nonnegative real numbers [0, ∞]; defined as WithTop ℝ≥0; it is equipped with the following structures:

• coercion from ℝ≥0 defined in the natural way;

• the natural structure of a complete dense linear order: ↑p ≤ ↑q ↔ p ≤ q and ∀ a, a ≤ ∞;

• a + b is defined so that ↑p + ↑q = ↑(p + q) for (p q : ℝ≥0) and a + ∞ = ∞ + a = ∞;

• a * b is defined so that ↑p * ↑q = ↑(p * q) for (p q : ℝ≥0), 0 * ∞ = ∞ * 0 = 0, and a * ∞ = ∞ * a = ∞ for a ≠ 0;

• a - b is defined as the minimal d such that a ≤ d + b; this way we have ↑p - ↑q = ↑(p - q), ∞ - ↑p = ∞, ↑p - ∞ = ∞ - ∞ = 0; note that there is no negation, only subtraction;

• a⁻¹ is defined as Inf {b | 1 ≤ a * b}. This way we have (↑p)⁻¹ = ↑(p⁻¹) for p : ℝ≥0, p ≠ 0, 0⁻¹ = ∞, and ∞⁻¹ = 0.

• a / b is defined as a * b⁻¹.

The addition and multiplication defined this way together with 0 = ↑0 and 1 = ↑1 turn ℝ≥0∞ into a canonically ordered commutative semiring of characteristic zero.

• Coercions to/from other types:

• coercion ℝ≥0 → ℝ≥0∞ is defined as Coe, so one can use (p : ℝ≥0) in a context that expects a : ℝ≥0∞, and Lean will apply coe automatically;

• ENNReal.toNNReal sends ↑p to p and ∞ to 0;

• ENNReal.toReal := coe ∘ ENNReal.toNNReal sends ↑p, p : ℝ≥0 to (↑p : ℝ) and ∞ to 0;

• ENNReal.ofReal := coe ∘ Real.toNNReal sends x : ℝ to ↑⟨max x 0, _⟩

• ENNReal.neTopEquivNNReal is an equivalence between {a : ℝ≥0∞ // a ≠ 0} and ℝ≥0.

## Implementation notes #

We define a CanLift ℝ≥0∞ ℝ≥0 instance, so one of the ways to prove theorems about an ℝ≥0∞ number a is to consider the cases a = ∞ and a ≠ ∞, and use the tactic lift a to ℝ≥0 using ha in the second case. This instance is even more useful if one already has ha : a ≠ ∞ in the context, or if we have (f : α → ℝ≥0∞) (hf : ∀ x, f x ≠ ∞).

## Notations #

• ℝ≥0∞: the type of the extended nonnegative real numbers;
• ℝ≥0: the type of nonnegative real numbers [0, ∞); defined in data.real.nnreal;
• ∞: a localized notation in ℝ≥0∞ for ⊤ : ℝ≥0∞.

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Instances For

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Instances For

Notation for infinity as an ENNReal number.

Instances For
noncomputable instance ENNReal.instSub :
instance ENNReal.covariantClass_mul_le :
CovariantClass ENNReal ENNReal (fun x x_1 => x * x_1) fun x x_1 => x x_1
instance ENNReal.covariantClass_add_le :
CovariantClass ENNReal ENNReal (fun x x_1 => x + x_1) fun x x_1 => x x_1
@[match_pattern]

Coercion from ℝ≥0 to ℝ≥0∞.

Instances For
def ENNReal.recTopCoe {C : ENNRealSort u_3} (top : C ) (coe : (x : NNReal) → C x) (x : ENNReal) :
C x

A version of WithTop.recTopCoe that uses ENNReal.some.

Instances For
@[simp]
theorem ENNReal.none_eq_top :
none =
@[simp]
theorem ENNReal.some_eq_coe (a : NNReal) :
some a = a
@[simp]
theorem ENNReal.some_eq_coe' (a : NNReal) :
a = a

toNNReal x returns x if it is real, otherwise 0.

Instances For

toReal x returns x if it is real, 0 otherwise.

Instances For
noncomputable def ENNReal.ofReal (r : ) :

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

Instances For
@[simp]
@[simp]
theorem ENNReal.coe_toNNReal {a : ENNReal} :
a ↑() = a
@[simp]
theorem ENNReal.ofReal_toReal {a : ENNReal} (h : a ) :
@[simp]
theorem ENNReal.toReal_ofReal {r : } (h : 0 r) :
theorem ENNReal.coe_nnreal_eq (r : NNReal) :
r =
theorem ENNReal.ofReal_eq_coe_nnreal {x : } (h : 0 x) :
= { val := x, property := h }
@[simp]
theorem ENNReal.ofReal_coe_nnreal {p : NNReal} :
= p
@[simp]
theorem ENNReal.coe_zero :
0 = 0
@[simp]
theorem ENNReal.coe_one :
1 = 1
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem ENNReal.coe_toReal (r : NNReal) :
= r
@[simp]
@[simp]
@[simp]
@[simp]
theorem ENNReal.forall_ennreal {p : } :
((a : ENNReal) → p a) ((r : NNReal) → p r) p
theorem ENNReal.forall_ne_top {p : } :
((a : ENNReal) → a p a) (r : NNReal) → p r
theorem ENNReal.exists_ne_top' {p : } :
(a x, p a) r, p r
theorem ENNReal.exists_ne_top {p : } :
(a, a p a) r, p r
@[simp]
theorem ENNReal.coe_ne_top {r : NNReal} :
r
@[simp]
theorem ENNReal.top_ne_coe {r : NNReal} :
r
@[simp]
theorem ENNReal.coe_lt_top {r : NNReal} :
r <
@[simp]
theorem ENNReal.ofReal_ne_top {r : } :
@[simp]
theorem ENNReal.ofReal_lt_top {r : } :
@[simp]
theorem ENNReal.top_ne_ofReal {r : } :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem ENNReal.coe_eq_coe {r : NNReal} {q : NNReal} :
r = q r = q
@[simp]
theorem ENNReal.coe_le_coe {r : NNReal} {q : NNReal} :
r q r q
@[simp]
theorem ENNReal.coe_lt_coe {r : NNReal} {q : NNReal} :
r < q r < q
@[simp]
theorem ENNReal.coe_eq_zero {r : NNReal} :
r = 0 r = 0
@[simp]
theorem ENNReal.zero_eq_coe {r : NNReal} :
0 = r 0 = r
@[simp]
theorem ENNReal.coe_eq_one {r : NNReal} :
r = 1 r = 1
@[simp]
theorem ENNReal.one_eq_coe {r : NNReal} :
1 = r 1 = r
@[simp]
theorem ENNReal.coe_pos {r : NNReal} :
0 < r 0 < r
theorem ENNReal.coe_ne_zero {r : NNReal} :
r 0 r 0
@[simp]
theorem ENNReal.coe_add {r : NNReal} {p : NNReal} :
↑(r + p) = r + p
@[simp]
theorem ENNReal.coe_mul {r : NNReal} {p : NNReal} :
↑(r * p) = r * p
@[simp]
theorem ENNReal.coe_ofNat (n : ) [] :
↑() =
theorem ENNReal.coe_two :
2 = 2
theorem ENNReal.toNNReal_eq_toNNReal_iff (x : ENNReal) (y : ENNReal) :
x = y x = 0 y = x = y = 0
theorem ENNReal.toReal_eq_toReal_iff (x : ENNReal) (y : ENNReal) :
x = y x = 0 y = x = y = 0
theorem ENNReal.toNNReal_eq_toNNReal_iff' {x : ENNReal} {y : ENNReal} (hx : x ) (hy : y ) :
x = y
theorem ENNReal.toReal_eq_toReal_iff' {x : ENNReal} {y : ENNReal} (hx : x ) (hy : y ) :
x = y
@[simp]
theorem ENNReal.one_lt_two :
1 < 2

(1 : ℝ≥0∞) ≤ 1, recorded as a Fact for use with Lp spaces.

(1 : ℝ≥0∞) ≤ 2, recorded as a Fact for use with Lp spaces.

(1 : ℝ≥0∞) ≤ ∞, recorded as a Fact for use with Lp spaces.

The set of numbers in ℝ≥0∞ that are not equal to ∞ is equivalent to ℝ≥0.

Instances For
theorem ENNReal.cinfi_ne_top {α : Type u_1} [] (f : ENNRealα) :
⨅ (x : { x // x }), f x = ⨅ (x : NNReal), f x
theorem ENNReal.iInf_ne_top {α : Type u_1} [] (f : ENNRealα) :
⨅ (x : ENNReal) (_ : x ), f x = ⨅ (x : NNReal), f x
theorem ENNReal.csupr_ne_top {α : Type u_1} [] (f : ENNRealα) :
⨆ (x : { x // x }), f x = ⨆ (x : NNReal), f x
theorem ENNReal.iSup_ne_top {α : Type u_1} [] (f : ENNRealα) :
⨆ (x : ENNReal) (_ : x ), f x = ⨆ (x : NNReal), f x
theorem ENNReal.iInf_ennreal {α : Type u_3} [] {f : ENNRealα} :
⨅ (n : ENNReal), f n = (⨅ (n : NNReal), f n) f
theorem ENNReal.iSup_ennreal {α : Type u_3} [] {f : ENNRealα} :
⨆ (n : ENNReal), f n = (⨆ (n : NNReal), f n) f

Coercion ℝ≥0 → ℝ≥0∞ as a RingHom.

Instances For
@[simp]

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

theorem ENNReal.smul_def {M : Type u_3} [] (c : NNReal) (x : M) :
c x = c x
instance ENNReal.smulCommClass_left {M : Type u_3} {N : Type u_4} [] [SMul M N] [] :
instance ENNReal.smulCommClass_right {M : Type u_3} {N : Type u_4} [] [SMul M N] [] :

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

noncomputable instance ENNReal.instModuleNNRealInstNNRealSemiring {M : Type u_3} [] [] :

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

noncomputable instance ENNReal.instAlgebraNNRealInstNNRealCommSemiring {A : Type u_3} [] [] :

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

theorem ENNReal.coe_smul {R : Type u_3} (r : R) (s : NNReal) [] [] :
↑(r s) = r s
@[simp]
theorem ENNReal.coe_indicator {α : Type u_3} (s : Set α) (f : αNNReal) (a : α) :
↑() = Set.indicator s (fun x => ↑(f x)) a
@[simp]
theorem ENNReal.coe_pow {r : NNReal} (n : ) :
↑(r ^ n) = r ^ n
@[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₂ ) :
ENNReal.toNNReal (r₁ + r₂) =
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.smul_top {R : Type u_3} [Zero R] [] [] (c : R) :
c = if c = 0 then 0 else
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 : } {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 : } {f : αNNReal} :
↑(Finset.prod s fun a => f a) = Finset.prod s fun a => ↑(f a)
@[simp]
theorem ENNReal.one_le_coe_iff {r : NNReal} :
1 r 1 r
@[simp]
theorem ENNReal.coe_le_one_iff {r : NNReal} :
r 1 r 1
@[simp]
theorem ENNReal.coe_lt_one_iff {p : NNReal} :
p < 1 p < 1
@[simp]
theorem ENNReal.one_lt_coe_iff {p : NNReal} :
1 < p 1 < p
@[simp]
theorem ENNReal.coe_nat (n : ) :
n = n
@[simp]
theorem ENNReal.ofReal_coe_nat (n : ) :
= n
@[simp]
theorem ENNReal.ofReal_ofNat (n : ) [] :
@[simp]
theorem ENNReal.nat_ne_top (n : ) :
n
@[simp]
theorem ENNReal.top_ne_nat (n : ) :
n
@[simp]
@[simp]
theorem ENNReal.toNNReal_nat (n : ) :
= n
@[simp]
theorem ENNReal.toReal_nat (n : ) :
= n
@[simp]
theorem ENNReal.toReal_ofNat (n : ) [] :
theorem ENNReal.le_coe_iff {a : ENNReal} {r : NNReal} :
a r p, a = p p r
theorem ENNReal.coe_le_iff {a : ENNReal} {r : NNReal} :
r a ∀ (p : NNReal), a = pr p
theorem ENNReal.lt_iff_exists_coe {a : ENNReal} {b : ENNReal} :
a < b p, a = p p < b
theorem ENNReal.toReal_le_coe_of_le_coe {a : ENNReal} {b : NNReal} (h : a b) :
b
@[simp]
theorem ENNReal.coe_finset_sup {α : Type u_1} {s : } {f : αNNReal} :
↑() = Finset.sup s fun x => ↑(f x)
@[simp]
theorem ENNReal.max_eq_zero_iff {a : ENNReal} {b : ENNReal} :
max a b = 0 a = 0 b = 0
@[simp]
theorem ENNReal.sup_eq_max {a : ENNReal} {b : ENNReal} :
a b = max 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
instance ENNReal.contravariantClass_add_lt :
ContravariantClass ENNReal ENNReal (fun x x_1 => x + x_1) fun x x_1 => x < x_1
theorem ENNReal.lt_add_right {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b 0) :
a < a + b
theorem ENNReal.lt_iff_exists_rat_btwn {a : ENNReal} {b : ENNReal} :
a < b q, 0 q a < ↑() ↑() < b
theorem ENNReal.lt_iff_exists_real_btwn {a : ENNReal} {b : ENNReal} :
a < b r, 0 r
theorem ENNReal.lt_iff_exists_nnreal_btwn {a : ENNReal} {b : ENNReal} :
a < b r, a < r r < b
theorem ENNReal.lt_iff_exists_add_pos_lt {a : ENNReal} {b : ENNReal} :
a < b r, 0 < r a + r < b
theorem ENNReal.le_of_forall_pos_le_add {a : ENNReal} {b : ENNReal} (h : ∀ (ε : NNReal), 0 < εb < a b + ε) :
a b
theorem ENNReal.coe_nat_lt_coe {r : NNReal} {n : } :
n < r n < r
theorem ENNReal.coe_lt_coe_nat {r : NNReal} {n : } :
r < n r < n
theorem ENNReal.exists_nat_gt {r : ENNReal} (h : r ) :
n, r < n
@[simp]
theorem ENNReal.iUnion_Iio_coe_nat :
⋃ (n : ), Set.Iio n = {}
@[simp]
theorem ENNReal.iUnion_Iic_coe_nat :
⋃ (n : ), Set.Iic n = {}
@[simp]
theorem ENNReal.iUnion_Ioc_coe_nat {a : ENNReal} :
⋃ (n : ), Set.Ioc a n = \ {}
@[simp]
theorem ENNReal.iUnion_Ioo_coe_nat {a : ENNReal} :
⋃ (n : ), Set.Ioo a n = \ {}
@[simp]
theorem ENNReal.iUnion_Icc_coe_nat {a : ENNReal} :
⋃ (n : ), Set.Icc a n = \ {}
@[simp]
theorem ENNReal.iUnion_Ico_coe_nat {a : ENNReal} :
⋃ (n : ), Set.Ico a n = \ {}
@[simp]
theorem ENNReal.iInter_Ici_coe_nat :
⋂ (n : ), Set.Ici n = {}
@[simp]
theorem ENNReal.iInter_Ioi_coe_nat :
⋂ (n : ), Set.Ioi n = {}
theorem ENNReal.add_lt_add {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (ac : a < c) (bd : b < d) :
a + b < c + d
@[simp]
theorem ENNReal.coe_min {r : NNReal} {p : NNReal} :
↑(min r p) = min r p
@[simp]
theorem ENNReal.coe_max {r : NNReal} {p : NNReal} :
↑(max r p) = max r p
theorem ENNReal.le_of_top_imp_top_of_toNNReal_le {a : ENNReal} {b : ENNReal} (h : a = b = ) (h_nnreal : a b ) :
a b
@[simp]
theorem ENNReal.abs_toReal {x : ENNReal} :
theorem ENNReal.coe_sSup {s : } :
↑(sSup s) = ⨆ (a : NNReal) (_ : a s), a
theorem ENNReal.coe_sInf {s : } :
↑(sInf s) = ⨅ (a : NNReal) (_ : a s), a
theorem ENNReal.coe_iSup {ι : Sort u_4} {f : ιNNReal} (hf : ) :
↑(iSup f) = ⨆ (a : ι), ↑(f a)
theorem ENNReal.coe_iInf {ι : Sort u_4} [] (f : ιNNReal) :
↑(iInf f) = ⨅ (a : ι), ↑(f a)
theorem ENNReal.coe_mem_upperBounds {r : NNReal} {s : } :
r r
theorem ENNReal.iSup_coe_eq_top {ι : Sort u_3} {f : ιNNReal} :
⨆ (i : ι), ↑(f i) = ¬
theorem ENNReal.iSup_coe_lt_top {ι : Sort u_3} {f : ιNNReal} :
⨆ (i : ι), ↑(f i) <
theorem ENNReal.iInf_coe_eq_top {ι : Sort u_3} {f : ιNNReal} :
⨅ (i : ι), ↑(f i) =
theorem ENNReal.iInf_coe_lt_top {ι : Sort u_3} {f : ιNNReal} :
⨅ (i : ι), ↑(f i) <
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 => a * x
theorem ENNReal.mul_right_mono {a : ENNReal} :
Monotone fun x => x * a
theorem ENNReal.pow_strictMono {n : } :
n 0StrictMono fun x => x ^ n
theorem ENNReal.pow_lt_pow_of_lt_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 => 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)

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 ∞.

theorem ENNReal.cancel_of_ne {a : ENNReal} (h : a ) :

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

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

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.

theorem ENNReal.cancel_coe {a : NNReal} :

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 | 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.prod_lt_top {α : Type u_1} {s : } {f : αENNReal} (h : ∀ (a : α), a sf 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 : } {f : αENNReal} (h : ∀ (a : α), a sf 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 : } {f : αENNReal} :
(Finset.sum s fun a => f a) < ∀ (a : α), a sf a <

A sum of finite numbers is still finite

theorem ENNReal.sum_eq_top_iff {α : Type u_1} {s : } {f : αENNReal} :
(Finset.sum s fun x => f x) = a, 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 : } {f : αENNReal} (h : (Finset.sum s fun x => f x) ) {a : α} (ha : a s) :
f a <
theorem ENNReal.toNNReal_sum {α : Type u_1} {s : } {f : αENNReal} (hf : ∀ (a : α), a sf a ) :
ENNReal.toNNReal (Finset.sum s fun a => f a) = Finset.sum s fun a => ENNReal.toNNReal (f a)

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

theorem ENNReal.toReal_sum {α : Type u_1} {s : } {f : αENNReal} (hf : ∀ (a : α), a sf a ) :
ENNReal.toReal (Finset.sum s fun a => f a) = Finset.sum s fun a => ENNReal.toReal (f a)

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 : } {f : α} (hf : ∀ (i : α), i s0 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 : } (hs : ) {f : αENNReal} {g : αENNReal} (Hlt : ∀ (i : α), i sf 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 : } (hs : ) {f : αENNReal} {g : αENNReal} (Hle : (Finset.sum s fun i => f i) Finset.sum s fun i => g i) :
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 + ε₂)
theorem ENNReal.div_eq_inv_mul {a : ENNReal} {b : ENNReal} :
a / b = b⁻¹ * a
@[simp]
@[simp]
theorem ENNReal.inv_top :
= 0
theorem ENNReal.coe_inv_le {r : NNReal} :
r⁻¹ (r)⁻¹
@[simp]
theorem ENNReal.coe_inv {r : NNReal} (hr : r 0) :
r⁻¹ = (r)⁻¹
@[simp]
theorem ENNReal.coe_div {r : NNReal} {p : NNReal} (hr : r 0) :
↑(p / r) = p / r
theorem ENNReal.div_zero {a : ENNReal} (h : a 0) :
a / 0 =
theorem ENNReal.inv_pow {a : ENNReal} {n : } :
(a ^ n)⁻¹ = a⁻¹ ^ n
theorem ENNReal.mul_inv_cancel {a : ENNReal} (h0 : a 0) (ht : a ) :
a * a⁻¹ = 1
theorem ENNReal.inv_mul_cancel {a : ENNReal} (h0 : a 0) (ht : a ) :
a⁻¹ * a = 1
theorem ENNReal.div_mul_cancel {a : ENNReal} {b : ENNReal} (h0 : a 0) (hI : a ) :
b / a * a = b
theorem ENNReal.mul_div_cancel' {a : ENNReal} {b : ENNReal} (h0 : a 0) (hI : a ) :
a * (b / a) = b
theorem ENNReal.mul_comm_div {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a / b * c = a * (c / b)
theorem ENNReal.mul_div_right_comm {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a * b / c = a / c * b
@[simp]
theorem ENNReal.inv_eq_top {a : ENNReal} :
a⁻¹ = a = 0
@[simp]
theorem ENNReal.inv_lt_top {x : ENNReal} :
x⁻¹ < 0 < x
theorem ENNReal.div_lt_top {x : ENNReal} {y : ENNReal} (h1 : x ) (h2 : y 0) :
x / y <
@[simp]
theorem ENNReal.inv_eq_zero {a : ENNReal} :
a⁻¹ = 0 a =
theorem ENNReal.div_pos {a : ENNReal} {b : ENNReal} (ha : a 0) (hb : b ) :
0 < a / b
theorem ENNReal.mul_inv {a : ENNReal} {b : ENNReal} (ha : a 0 b ) (hb : a b 0) :
(a * b)⁻¹ = a⁻¹ * b⁻¹
theorem ENNReal.mul_div_mul_left {c : ENNReal} (a : ENNReal) (b : ENNReal) (hc : c 0) (hc' : c ) :
c * a / (c * b) = a / b
theorem ENNReal.mul_div_mul_right {c : ENNReal} (a : ENNReal) (b : ENNReal) (hc : c 0) (hc' : c ) :
a * c / (b * c) = a / b
theorem ENNReal.sub_div {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : 0 < bb < ac 0) :
(a - b) / c = a / c - b / c
@[simp]
theorem ENNReal.inv_pos {a : ENNReal} :
@[simp]
theorem ENNReal.inv_lt_inv {a : ENNReal} {b : ENNReal} :
a⁻¹ < b⁻¹ b < a
@[simp]
theorem ENNReal.inv_le_inv {a : ENNReal} {b : ENNReal} :
theorem ENNReal.inv_le_inv' {a : ENNReal} {b : ENNReal} (h : a b) :
theorem ENNReal.inv_lt_inv' {a : ENNReal} {b : ENNReal} (h : a < b) :
@[simp]
theorem ENNReal.inv_le_one {a : ENNReal} :
a⁻¹ 1 1 a
@[simp]
theorem ENNReal.inv_lt_one {a : ENNReal} :
a⁻¹ < 1 1 < a
@[simp]
theorem ENNReal.one_lt_inv {a : ENNReal} :
1 < a⁻¹ a < 1
@[simp]
theorem OrderIso.invENNReal_apply :
∀ (a : ENNReal), = (OrderDual.toDual a)⁻¹

The inverse map fun x ↦ x⁻¹ is an order isomorphism between ℝ≥0∞ and its OrderDual

Instances For
@[simp]
theorem OrderIso.invENNReal_symm_apply (a : ) :
= (OrderDual.ofDual a)⁻¹
@[simp]
theorem ENNReal.div_top {a : ENNReal} :
a / = 0
theorem ENNReal.top_div {a : ENNReal} :
/ a = if a = then 0 else
@[simp]
theorem ENNReal.top_div_coe {p : NNReal} :
/ p =
@[simp]
theorem ENNReal.zero_div {a : ENNReal} :
0 / a = 0
theorem ENNReal.div_eq_top {a : ENNReal} {b : ENNReal} :
a / b = a 0 b = 0 a = b
theorem ENNReal.le_div_iff_mul_le {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : b 0 c 0) (ht : b c ) :
a c / b a * b c
theorem ENNReal.div_le_iff_le_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb0 : b 0 c ) (hbt : b c 0) :
a / b c a c * b
theorem ENNReal.lt_div_iff_mul_lt {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb0 : b 0 c ) (hbt : b c 0) :
c < a / b c * b < a
theorem ENNReal.div_le_of_le_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a b * c) :
a / c b
theorem ENNReal.div_le_of_le_mul' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a b * c) :
a / b c
theorem ENNReal.mul_le_of_le_div {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a b / c) :
a * c b
theorem ENNReal.mul_le_of_le_div' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a b / c) :
c * a b
theorem ENNReal.div_lt_iff {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : b 0 c 0) (ht : b c ) :
c / b < a c < a * b
theorem ENNReal.mul_lt_of_lt_div {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a < b / c) :
a * c < b
theorem ENNReal.mul_lt_of_lt_div' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a < b / c) :
c * a < b
theorem ENNReal.div_lt_of_lt_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a < b * c) :
a / c < b
theorem ENNReal.div_lt_of_lt_mul' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a < b * c) :
a / b < c
theorem ENNReal.inv_le_iff_le_mul {a : ENNReal} {b : ENNReal} (h₁ : b = a 0) (h₂ : a = b 0) :
a⁻¹ b 1 a * b
@[simp]
theorem ENNReal.le_inv_iff_mul_le {a : ENNReal} {b : ENNReal} :
a b⁻¹ a * b 1
theorem ENNReal.div_le_div {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (hab : a b) (hdc : d c) :
a / c b / d
theorem ENNReal.div_le_div_left {a : ENNReal} {b : ENNReal} (h : a b) (c : ENNReal) :
c / b c / a
theorem ENNReal.div_le_div_right {a : ENNReal} {b : ENNReal} (h : a b) (c : ENNReal) :
a / c b / c
theorem ENNReal.eq_inv_of_mul_eq_one_left {a : ENNReal} {b : ENNReal} (h : a * b = 1) :
a = b⁻¹
theorem ENNReal.mul_le_iff_le_inv {a : ENNReal} {b : ENNReal} {r : ENNReal} (hr₀ : r 0) (hr₁ : r ) :
r * a b a r⁻¹ * b
theorem ENNReal.le_inv_smul_iff {a : ENNReal} {b : ENNReal} {r : NNReal} (hr₀ : r 0) :
a r⁻¹ b r a b

A variant of le_inv_smul_iff that holds for ENNReal.

theorem ENNReal.inv_smul_le_iff {a : ENNReal} {b : ENNReal} {r : NNReal} (hr₀ : r 0) :
r⁻¹ a b a r b

A variant of inv_smul_le_iff that holds for ENNReal.

theorem ENNReal.le_of_forall_nnreal_lt {x : ENNReal} {y : ENNReal} (h : ∀ (r : NNReal), r < xr y) :
x y
theorem ENNReal.le_of_forall_pos_nnreal_lt {x : ENNReal} {y : ENNReal} (h : ∀ (r : NNReal), 0 < rr < xr y) :
x y
theorem ENNReal.eq_top_of_forall_nnreal_le {x : ENNReal} (h : ∀ (r : NNReal), r x) :
x =
theorem ENNReal.add_div {a : ENNReal} {b : ENNReal} {c : ENNReal} :
(a + b) / c = a / c + b / c
theorem ENNReal.div_add_div_same {a : ENNReal} {b : ENNReal} {c : ENNReal} :
a / c + b / c = (a + b) / c
theorem ENNReal.div_self {a : ENNReal} (h0 : a 0) (hI : a ) :
a / a = 1
theorem ENNReal.mul_div_le {a : ENNReal} {b : ENNReal} :
a * (b / a) b
theorem ENNReal.eq_div_iff {a : ENNReal} {b : ENNReal} {c : ENNReal} (ha : a 0) (ha' : a ) :
b = c / a a * b = c
theorem ENNReal.div_eq_div_iff {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (ha : a 0) (ha' : a ) (hb : b 0) (hb' : b ) :
c / b = d / a a * c = b * d
theorem ENNReal.div_eq_one_iff {a : ENNReal} {b : ENNReal} (hb₀ : b 0) (hb₁ : b ) :
a / b = 1 a = b
@[simp]
theorem ENNReal.add_halves (a : ENNReal) :
a / 2 + a / 2 = a
@[simp]
theorem ENNReal.add_thirds (a : ENNReal) :
a / 3 + a / 3 + a / 3 = a
@[simp]
theorem ENNReal.div_eq_zero_iff {a : ENNReal} {b : ENNReal} :
a / b = 0 a = 0 b =
@[simp]
theorem ENNReal.div_pos_iff {a : ENNReal} {b : ENNReal} :
0 < a / b a 0 b
theorem ENNReal.half_pos {a : ENNReal} (h : a 0) :
0 < a / 2
theorem ENNReal.half_lt_self {a : ENNReal} (hz : a 0) (ht : a ) :
a / 2 < a
theorem ENNReal.sub_half {a : ENNReal} (h : a ) :
a - a / 2 = a / 2

The birational order isomorphism between ℝ≥0∞ and the unit interval Set.Iic (1 : ℝ≥0∞).

Instances For
@[simp]
@[simp]
theorem ENNReal.orderIsoIicCoe_apply_coe (a : NNReal) :
∀ (a : ↑(Set.Iic a)), ↑(↑() a) =
def ENNReal.orderIsoIicCoe (a : NNReal) :
↑(Set.Iic a) ≃o ↑()

Order isomorphism between an initial interval in ℝ≥0∞ and an initial interval in ℝ≥0.

Instances For
@[simp]
theorem ENNReal.orderIsoIicCoe_symm_apply_coe (a : NNReal) (b : ↑()) :
↑(↑() b) = b

An order isomorphism between the extended nonnegative real numbers and the unit interval.

Instances For
theorem ENNReal.exists_inv_nat_lt {a : ENNReal} (h : a 0) :
n, (n)⁻¹ < a
theorem ENNReal.exists_nat_pos_mul_gt {a : ENNReal} {b : ENNReal} (ha : a 0) (hb : b ) :
n, n > 0 b < n * a
theorem ENNReal.exists_nat_mul_gt {a : ENNReal} {b : ENNReal} (ha : a 0) (hb : b ) :
n, b < n * a
theorem ENNReal.exists_nat_pos_inv_mul_lt {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b 0) :
n, n > 0 (n)⁻¹ * a < b
theorem ENNReal.exists_nnreal_pos_mul_lt {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b 0) :
n, n > 0 n * a < b
theorem ENNReal.exists_inv_two_pow_lt {a : ENNReal} (ha : a 0) :
n, 2⁻¹ ^ n < a
@[simp]
theorem ENNReal.coe_zpow {r : NNReal} (hr : r 0) (n : ) :
↑(r ^ n) = r ^ n
theorem ENNReal.zpow_pos {a : ENNReal} (ha : a 0) (h'a : a ) (n : ) :
0 < a ^ n
theorem ENNReal.zpow_lt_top {a : ENNReal} (ha : a 0) (h'a : a ) (n : ) :
a ^ n <
theorem ENNReal.exists_mem_Ico_zpow {x : ENNReal} {y : ENNReal} (hx : x 0) (h'x : x ) (hy : 1 < y) (h'y : y ) :
n, x Set.Ico (y ^ n) (y ^ (n + 1))
theorem ENNReal.exists_mem_Ioc_zpow {x : ENNReal} {y : ENNReal} (hx : x 0) (h'x : x ) (hy : 1 < y) (h'y : y ) :
n, x Set.Ioc (y ^ n) (y ^ (n + 1))
theorem ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow {y : ENNReal} (hy : 1 < y) (h'y : y ) :
= ⋃ (n : ), Set.Ico (y ^ n) (y ^ (n + 1))
theorem ENNReal.zpow_le_of_le {x : ENNReal} (hx : 1 x) {a : } {b : } (h : a b) :
x ^ a x ^ b
theorem ENNReal.monotone_zpow {x : ENNReal} (hx : 1 x) :
Monotone fun x => x ^ x
theorem ENNReal.zpow_add {x : ENNReal} (hx : x 0) (h'x : x ) (m : ) (n : ) :
x ^ (m + n) = x ^ m * x ^ n
theorem ENNReal.toReal_add {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b ) :
theorem ENNReal.toReal_sub_of_le {a : ENNReal} {b : ENNReal} (h : b a) (ha : a ) :
theorem ENNReal.le_toReal_sub {a : ENNReal} {b : ENNReal} (hb : b ) :
theorem ENNReal.ofReal_add {p : } {q : } (hp : 0 p) (hq : 0 q) :
@[simp]
theorem ENNReal.toReal_le_toReal {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b ) :
a b
theorem ENNReal.toReal_mono {a : ENNReal} {b : ENNReal} (hb : b ) (h : a b) :
theorem ENNReal.toReal_mono' {a : ENNReal} {b : ENNReal} (h : a b) (ht : b = a = ) :
@[simp]
theorem ENNReal.toReal_lt_toReal {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b ) :
a < b
theorem ENNReal.toReal_strict_mono {a : ENNReal} {b : ENNReal} (hb : b ) (h : a < b) :
theorem ENNReal.toNNReal_mono {a : ENNReal} {b : ENNReal} (hb : b ) (h : a b) :
theorem ENNReal.toReal_le_add' {a : ENNReal} {b : ENNReal} {c : ENNReal} (hle : a b + c) (hb : b = a = ) (hc : c = a = ) :

If a ≤ b + c and a = ∞ whenever b = ∞ or c = ∞, then ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c. This lemma is useful to transfer triangle-like inequalities from ENNReals to Reals.

theorem ENNReal.toReal_le_add {a : ENNReal} {b : ENNReal} {c : ENNReal} (hle : a b + c) (hb : b ) (hc : c ) :

If a ≤ b + c, b ≠ ∞, and c ≠ ∞, then ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c. This lemma is useful to transfer triangle-like inequalities from ENNReals to Reals.

@[simp]
theorem ENNReal.toNNReal_le_toNNReal {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b ) :
a b
theorem ENNReal.toNNReal_strict_mono {a : ENNReal} {b : ENNReal} (hb : b ) (h : a < b) :
@[simp]
theorem ENNReal.toNNReal_lt_toNNReal {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b ) :
a < b
theorem ENNReal.toReal_max {a : ENNReal} {b : ENNReal} (hr : a ) (hp : b ) :
ENNReal.toReal (max a b) = max () ()
theorem ENNReal.toReal_min {a : ENNReal} {b : ENNReal} (hr : a ) (hp : b ) :
ENNReal.toReal (min a b) = min () ()
theorem ENNReal.toReal_sup {a : ENNReal} {b : ENNReal} :
a b ENNReal.toReal (a b) =
theorem ENNReal.toReal_inf {a : ENNReal} {b : ENNReal} :
a b ENNReal.toReal (a b) =
theorem ENNReal.toNNReal_pos {a : ENNReal} (ha₀ : a 0) (ha_top : a ) :
theorem ENNReal.toReal_pos {a : ENNReal} (ha₀ : a 0) (ha_top : a ) :
theorem ENNReal.ofReal_le_ofReal {p : } {q : } (h : p q) :
theorem ENNReal.ofReal_le_of_le_toReal {a : } {b : ENNReal} (h : ) :
@[simp]
theorem ENNReal.ofReal_le_ofReal_iff {p : } {q : } (h : 0 q) :
p q
@[simp]
theorem ENNReal.ofReal_eq_ofReal_iff {p : } {q : } (hp : 0 p) (hq : 0 q) :
p = q
@[simp]
theorem ENNReal.ofReal_lt_ofReal_iff {p : } {q : } (h : 0 < q) :
p < q
theorem ENNReal.ofReal_lt_ofReal_iff_of_nonneg {p : } {q : } (hp : 0 p) :
p < q
@[simp]
theorem ENNReal.ofReal_pos {p : } :
0 < p
@[simp]
theorem ENNReal.ofReal_eq_zero {p : } :
p 0
@[simp]
theorem ENNReal.zero_eq_ofReal {p : } :
p 0
theorem ENNReal.ofReal_of_nonpos {p : } :
p 0

Alias of the reverse direction of ENNReal.ofReal_eq_zero.

theorem ENNReal.ofReal_sub (p : ) {q : } (hq : 0 q) :
theorem ENNReal.ofReal_lt_iff_lt_toReal {a : } {b : ENNReal} (ha : 0 a) (hb : b ) :
theorem ENNReal.ofReal_lt_coe_iff {a : } {b : NNReal} (ha : 0 a) :
< b a < b
theorem ENNReal.le_ofReal_iff_toReal_le {a : ENNReal} {b : } (ha : a ) (hb : 0 b) :
theorem ENNReal.toReal_le_of_le_ofReal {a : ENNReal} {b : } (hb : 0 b) (h : ) :
theorem ENNReal.toReal_lt_of_lt_ofReal {a : ENNReal} {b : } (h : ) :
theorem ENNReal.ofReal_mul {p : } {q : } (hp : 0 p) :
theorem ENNReal.ofReal_mul' {p : } {q : } (hq : 0 q) :
theorem ENNReal.ofReal_pow {p : } (hp : 0 p) (n : ) :
theorem ENNReal.ofReal_inv_of_pos {x : } (hx : 0 < x) :
theorem ENNReal.ofReal_div_of_pos {x : } {y : } (hy : 0 < y) :
@[simp]
@[simp]

ENNReal.toNNReal as a MonoidHom.

Instances For
@[simp]
theorem ENNReal.toNNReal_pow (a : ENNReal) (n : ) :
@[simp]
theorem ENNReal.toNNReal_prod {ι : Type u_3} {s : } {f : ιENNReal} :
ENNReal.toNNReal (Finset.prod s fun i => f i) = Finset.prod s fun i => ENNReal.toNNReal (f i)

ENNReal.toReal as a MonoidHom.

Instances For
@[simp]
theorem ENNReal.toReal_mul {a : ENNReal} {b : ENNReal} :
@[simp]
theorem ENNReal.toReal_pow (a : ENNReal) (n : ) :
@[simp]
theorem ENNReal.toReal_prod {ι : Type u_3} {s : } {f : ιENNReal} :
ENNReal.toReal (Finset.prod s fun i => f i) = Finset.prod s fun i => ENNReal.toReal (f i)
theorem ENNReal.toReal_ofReal_mul (c : ) (a : ENNReal) (h : 0 c) :
=
theorem ENNReal.toReal_eq_toReal {a : ENNReal} {b : ENNReal} (ha : a ) (hb : b ) :
a = b
theorem ENNReal.trichotomy (p : ENNReal) :
p = 0 p =
theorem ENNReal.trichotomy₂ {p : ENNReal} {q : ENNReal} (hpq : p q) :
p = 0 q = 0 p = 0 q = p = 0 p = q = q =
theorem ENNReal.dichotomy (p : ENNReal) [Fact (1 p)] :
p =
theorem ENNReal.ofReal_prod_of_nonneg {α : Type u_1} {s : } {f : α} (hf : ∀ (i : α), i s0 f i) :
ENNReal.ofReal (Finset.prod s fun i => f i) = Finset.prod s fun i => ENNReal.ofReal (f i)
theorem ENNReal.toNNReal_iInf {ι : Sort u_3} {f : ιENNReal} (hf : ∀ (i : ι), f i ) :
= ⨅ (i : ι), ENNReal.toNNReal (f i)
theorem ENNReal.toNNReal_sInf (s : ) (hs : ∀ (r : ENNReal), r sr ) :
=
theorem ENNReal.toNNReal_iSup {ι : Sort u_3} {f : ιENNReal} (hf : ∀ (i : ι), f i ) :
= ⨆ (i : ι), ENNReal.toNNReal (f i)
theorem ENNReal.toNNReal_sSup (s : ) (hs : ∀ (r : ENNReal), r sr ) :
=
theorem ENNReal.toReal_iInf {ι : Sort u_3} {f : ιENNReal} (hf : ∀ (i : ι), f i ) :
= ⨅ (i : ι), ENNReal.toReal (f i)
theorem ENNReal.toReal_sInf (s : ) (hf : ∀ (r : ENNReal), r sr ) :
= sInf ()
theorem ENNReal.toReal_iSup {ι : Sort u_3} {f : ιENNReal} (hf : ∀ (i : ι), f i ) :
= ⨆ (i : ι), ENNReal.toReal (f i)
theorem ENNReal.toReal_sSup (s : ) (hf : ∀ (r : ENNReal), r sr ) :
= sSup ()
theorem ENNReal.iInf_add {a : ENNReal} {ι : Sort u_3} {f : ιENNReal} :
iInf f + a = ⨅ (i : ι), f i + a
theorem ENNReal.iSup_sub {a : ENNReal} {ι : Sort u_3} {f : ιENNReal} :
(⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a
theorem ENNReal.sub_iInf {a : ENNReal} {ι : Sort u_3} {f : ιENNReal} :
a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i
theorem ENNReal.sInf_add {a : ENNReal} {s : } :
sInf s + a = ⨅ (b : ENNReal) (_ : b s), b + a
theorem ENNReal.add_iInf {ι : Sort u_3} {f : ιENNReal} {a : ENNReal} :
a + iInf f = ⨅ (b : ι), a + f b
theorem ENNReal.iInf_add_iInf {ι : Sort u_3} {f : ιENNReal} {g : ιENNReal} (h : ∀ (i j : ι), k, f k + g k f i + g j) :
iInf f + iInf g = ⨅ (a : ι), f a + g a
theorem ENNReal.iInf_sum {α : Type u_1} {ι : Sort u_3} {f : ιαENNReal} {s : } [] (h : ∀ (t : ) (i j : ι), k, ∀ (a : α), a tf k a f i a f k a f j a) :
(⨅ (i : ι), Finset.sum s fun a => f i a) = Finset.sum s fun a => ⨅ (i : ι), f i a
theorem ENNReal.iInf_mul_of_ne {ι : Sort u_4} {f : ιENNReal} {x : ENNReal} (h0 : x 0) (h : x ) :
iInf f * x = ⨅ (i : ι), f i * x

If x ≠ 0 and x ≠ ∞, then right multiplication by x maps infimum to infimum. See also ENNReal.iInf_mul that assumes [Nonempty ι] but does not require x ≠ 0.

theorem ENNReal.iInf_mul {ι : Sort u_4} [] {f : ιENNReal} {x : ENNReal} (h : x ) :
iInf f * x = ⨅ (i : ι), f i * x

If x ≠ ∞, then right multiplication by x maps infimum over a nonempty type to infimum. See also ENNReal.iInf_mul_of_ne that assumes x ≠ 0 but does not require [Nonempty ι].

theorem ENNReal.mul_iInf {ι : Sort u_4} [] {f : ιENNReal} {x : ENNReal} (h : x ) :
x * iInf f = ⨅ (i : ι), x * f i

If x ≠ ∞, then left multiplication by x maps infimum over a nonempty type to infimum. See also ENNReal.mul_iInf_of_ne that assumes x ≠ 0 but does not require [Nonempty ι].

theorem ENNReal.mul_iInf_of_ne {ι : Sort u_4} {f : ιENNReal} {x : ENNReal} (h0 : x 0) (h : x ) :
x * iInf f = ⨅ (i : ι), x * f i

If x ≠ 0 and x ≠ ∞, then left multiplication by x maps infimum to infimum. See also ENNReal.mul_iInf that assumes [Nonempty ι] but does not require x ≠ 0.

supr_mul, mul_supr and variants are in Topology.Instances.ENNReal.

@[simp]
theorem ENNReal.iSup_eq_zero {ι : Sort u_3} {f : ιENNReal} :
⨆ (i : ι), f i = 0 ∀ (i : ι), f i = 0
@[simp]
theorem ENNReal.iSup_zero_eq_zero {ι : Sort u_3} :
⨆ (x : ι), 0 = 0
theorem ENNReal.sup_eq_zero {a : ENNReal} {b : ENNReal} :
a b = 0 a = 0 b = 0
theorem ENNReal.iSup_coe_nat :
⨆ (n : ), n =

Extension for the positivity tactic: ENNReal.toReal.

Instances For

Extension for the positivity tactic: ENNReal.toReal.

Instances For

Extension for the positivity tactic: ENNReal.some.

Instances For