Documentation

Mathlib.Data.ENNReal.Real

Maps between real and extended non-negative real numbers #

This file focuses on the functions ENNReal.toReal : ℝ≥0∞ → ℝ and ENNReal.ofReal : ℝ → ℝ≥0∞ which were defined in Data.ENNReal.Basic. It collects all the basic results of the interactions between these functions and the algebraic and lattice operations, although a few may appear in earlier files.

This file provides a positivity extension for ENNReal.ofReal.

Main theorems #

trichotomy (p : ℝ≥0∞) : p = 0 ∨ p = ∞ ∨ 0 < p.toReal: often used for WithLp and lp
dichotomy (p : ℝ≥0∞) [Fact (1 ≤ p)] : p = ∞ ∨ 1 ≤ p.toReal: often used for WithLp and lp
toNNReal_iInf through toReal_sSup: these declarations allow for easy conversions between indexed or set infima and suprema in ℝ, ℝ≥0 and ℝ≥0∞. This is especially useful because ℝ≥0∞ is a complete lattice.

theorem ENNReal.toReal_add {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toReal (a + b) = ENNReal.toReal a + ENNReal.toReal b

theorem ENNReal.toReal_sub_of_le {a : ENNReal} {b : ENNReal} (h : b ≤ a) (ha : a ≠ ⊤) :

ENNReal.toReal (a - b) = ENNReal.toReal a - ENNReal.toReal b

theorem ENNReal.le_toReal_sub {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) :

ENNReal.toReal a - ENNReal.toReal b ≤ ENNReal.toReal (a - b)

theorem ENNReal.toReal_add_le {a : ENNReal} {b : ENNReal} :

ENNReal.toReal (a + b) ≤ ENNReal.toReal a + ENNReal.toReal b

theorem ENNReal.ofReal_add {p : ℝ} {q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :

ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q

theorem ENNReal.ofReal_add_le {p : ℝ} {q : ℝ} :

ENNReal.ofReal (p + q) ≤ ENNReal.ofReal p + ENNReal.ofReal q

@[simp]

theorem ENNReal.toReal_le_toReal {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toReal a ≤ ENNReal.toReal b ↔ a ≤ b

theorem ENNReal.toReal_mono {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (h : a ≤ b) :

ENNReal.toReal a ≤ ENNReal.toReal b

theorem ENNReal.toReal_mono' {a : ENNReal} {b : ENNReal} (h : a ≤ b) (ht : b = ⊤ → a = ⊤) :

ENNReal.toReal a ≤ ENNReal.toReal b

@[simp]

theorem ENNReal.toReal_lt_toReal {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toReal a < ENNReal.toReal b ↔ a < b

theorem ENNReal.toReal_strict_mono {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (h : a < b) :

ENNReal.toReal a < ENNReal.toReal b

theorem ENNReal.toNNReal_mono {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (h : a ≤ b) :

ENNReal.toNNReal a ≤ ENNReal.toNNReal b

theorem ENNReal.toReal_le_add' {a : ENNReal} {b : ENNReal} {c : ENNReal} (hle : a ≤ b + c) (hb : b = ⊤ → a = ⊤) (hc : c = ⊤ → a = ⊤) :

ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c

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 ≠ ⊤) :

ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal 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 ≠ ⊤) :

ENNReal.toNNReal a ≤ ENNReal.toNNReal b ↔ a ≤ b

theorem ENNReal.toNNReal_strict_mono {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (h : a < b) :

ENNReal.toNNReal a < ENNReal.toNNReal b

@[simp]

theorem ENNReal.toNNReal_lt_toNNReal {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toNNReal a < ENNReal.toNNReal b ↔ a < b

theorem ENNReal.toReal_max {a : ENNReal} {b : ENNReal} (hr : a ≠ ⊤) (hp : b ≠ ⊤) :

ENNReal.toReal (max a b) = max (ENNReal.toReal a) (ENNReal.toReal b)

theorem ENNReal.toReal_min {a : ENNReal} {b : ENNReal} (hr : a ≠ ⊤) (hp : b ≠ ⊤) :

ENNReal.toReal (min a b) = min (ENNReal.toReal a) (ENNReal.toReal b)

theorem ENNReal.toReal_sup {a : ENNReal} {b : ENNReal} :

a ≠ ⊤ → b ≠ ⊤ → ENNReal.toReal (a ⊔ b) = ENNReal.toReal a ⊔ ENNReal.toReal b

theorem ENNReal.toReal_inf {a : ENNReal} {b : ENNReal} :

a ≠ ⊤ → b ≠ ⊤ → ENNReal.toReal (a ⊓ b) = ENNReal.toReal a ⊓ ENNReal.toReal b

theorem ENNReal.toNNReal_pos_iff {a : ENNReal} :

0 < ENNReal.toNNReal a ↔ 0 < a ∧ a < ⊤

theorem ENNReal.toNNReal_pos {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :

0 < ENNReal.toNNReal a

theorem ENNReal.toReal_pos_iff {a : ENNReal} :

0 < ENNReal.toReal a ↔ 0 < a ∧ a < ⊤

theorem ENNReal.toReal_pos {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :

0 < ENNReal.toReal a

theorem ENNReal.ofReal_le_ofReal {p : ℝ} {q : ℝ} (h : p ≤ q) :

ENNReal.ofReal p ≤ ENNReal.ofReal q

theorem ENNReal.ofReal_le_of_le_toReal {a : ℝ} {b : ENNReal} (h : a ≤ ENNReal.toReal b) :

ENNReal.ofReal a ≤ b

@[simp]

theorem ENNReal.ofReal_le_ofReal_iff {p : ℝ} {q : ℝ} (h : 0 ≤ q) :

ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q

theorem ENNReal.ofReal_le_ofReal_iff' {p : ℝ} {q : ℝ} :

ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q ∨ p ≤ 0

theorem ENNReal.ofReal_lt_ofReal_iff' {p : ℝ} {q : ℝ} :

ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q ∧ 0 < q

@[simp]

theorem ENNReal.ofReal_eq_ofReal_iff {p : ℝ} {q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :

ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q

@[simp]

theorem ENNReal.ofReal_lt_ofReal_iff {p : ℝ} {q : ℝ} (h : 0 < q) :

ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

theorem ENNReal.ofReal_lt_ofReal_iff_of_nonneg {p : ℝ} {q : ℝ} (hp : 0 ≤ p) :

ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

@[simp]

theorem ENNReal.ofReal_pos {p : ℝ} :

0 < ENNReal.ofReal p ↔ 0 < p

@[simp]

theorem ENNReal.ofReal_eq_zero {p : ℝ} :

ENNReal.ofReal p = 0 ↔ p ≤ 0

@[simp]

theorem ENNReal.zero_eq_ofReal {p : ℝ} :

0 = ENNReal.ofReal p ↔ p ≤ 0

theorem ENNReal.ofReal_of_nonpos {p : ℝ} :

p ≤ 0 → ENNReal.ofReal p = 0

Alias of the reverse direction of ENNReal.ofReal_eq_zero.

@[simp]

theorem ENNReal.ofReal_lt_nat_cast {p : ℝ} {n : ℕ} (hn : n ≠ 0) :

ENNReal.ofReal p < ↑n ↔ p < ↑n

@[simp]

theorem ENNReal.ofReal_lt_one {p : ℝ} :

ENNReal.ofReal p < 1 ↔ p < 1

@[simp]

theorem ENNReal.ofReal_lt_ofNat {p : ℝ} {n : ℕ} [h : Nat.AtLeastTwo n] :

ENNReal.ofReal p < OfNat.ofNat n ↔ p < OfNat.ofNat n

@[simp]

theorem ENNReal.nat_cast_le_ofReal {n : ℕ} {p : ℝ} (hn : n ≠ 0) :

↑n ≤ ENNReal.ofReal p ↔ ↑n ≤ p

@[simp]

theorem ENNReal.one_le_ofReal {p : ℝ} :

1 ≤ ENNReal.ofReal p ↔ 1 ≤ p

@[simp]

theorem ENNReal.ofNat_le_ofReal {n : ℕ} [h : Nat.AtLeastTwo n] {p : ℝ} :

OfNat.ofNat n ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p

@[simp]

theorem ENNReal.ofReal_le_nat_cast {r : ℝ} {n : ℕ} :

ENNReal.ofReal r ≤ ↑n ↔ r ≤ ↑n

@[simp]

theorem ENNReal.ofReal_le_one {r : ℝ} :

ENNReal.ofReal r ≤ 1 ↔ r ≤ 1

@[simp]

theorem ENNReal.ofReal_le_ofNat {r : ℝ} {n : ℕ} [Nat.AtLeastTwo n] :

ENNReal.ofReal r ≤ OfNat.ofNat n ↔ r ≤ OfNat.ofNat n

@[simp]

theorem ENNReal.nat_cast_lt_ofReal {n : ℕ} {r : ℝ} :

↑n < ENNReal.ofReal r ↔ ↑n < r

@[simp]

theorem ENNReal.one_lt_ofReal {r : ℝ} :

1 < ENNReal.ofReal r ↔ 1 < r

@[simp]

theorem ENNReal.ofNat_lt_ofReal {n : ℕ} [Nat.AtLeastTwo n] {r : ℝ} :

OfNat.ofNat n < ENNReal.ofReal r ↔ OfNat.ofNat n < r

@[simp]

theorem ENNReal.ofReal_eq_nat_cast {r : ℝ} {n : ℕ} (h : n ≠ 0) :

ENNReal.ofReal r = ↑n ↔ r = ↑n

@[simp]

theorem ENNReal.ofReal_eq_one {r : ℝ} :

ENNReal.ofReal r = 1 ↔ r = 1

@[simp]

theorem ENNReal.ofReal_eq_ofNat {r : ℝ} {n : ℕ} [h : Nat.AtLeastTwo n] :

ENNReal.ofReal r = OfNat.ofNat n ↔ r = OfNat.ofNat n

theorem ENNReal.ofReal_sub (p : ℝ) {q : ℝ} (hq : 0 ≤ q) :

ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

theorem ENNReal.ofReal_le_iff_le_toReal {a : ℝ} {b : ENNReal} (hb : b ≠ ⊤) :

ENNReal.ofReal a ≤ b ↔ a ≤ ENNReal.toReal b

theorem ENNReal.ofReal_lt_iff_lt_toReal {a : ℝ} {b : ENNReal} (ha : 0 ≤ a) (hb : b ≠ ⊤) :

ENNReal.ofReal a < b ↔ a < ENNReal.toReal b

theorem ENNReal.ofReal_lt_coe_iff {a : ℝ} {b : NNReal} (ha : 0 ≤ a) :

ENNReal.ofReal a < ↑b ↔ a < ↑b

theorem ENNReal.le_ofReal_iff_toReal_le {a : ENNReal} {b : ℝ} (ha : a ≠ ⊤) (hb : 0 ≤ b) :

a ≤ ENNReal.ofReal b ↔ ENNReal.toReal a ≤ b

theorem ENNReal.toReal_le_of_le_ofReal {a : ENNReal} {b : ℝ} (hb : 0 ≤ b) (h : a ≤ ENNReal.ofReal b) :

ENNReal.toReal a ≤ b

theorem ENNReal.lt_ofReal_iff_toReal_lt {a : ENNReal} {b : ℝ} (ha : a ≠ ⊤) :

a < ENNReal.ofReal b ↔ ENNReal.toReal a < b

theorem ENNReal.toReal_lt_of_lt_ofReal {a : ENNReal} {b : ℝ} (h : a < ENNReal.ofReal b) :

ENNReal.toReal a < b

theorem ENNReal.ofReal_mul {p : ℝ} {q : ℝ} (hp : 0 ≤ p) :

ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

theorem ENNReal.ofReal_mul' {p : ℝ} {q : ℝ} (hq : 0 ≤ q) :

ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

theorem ENNReal.ofReal_pow {p : ℝ} (hp : 0 ≤ p) (n : ℕ) :

ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n

theorem ENNReal.ofReal_nsmul {x : ℝ} {n : ℕ} :

ENNReal.ofReal (n • x) = n • ENNReal.ofReal x

theorem ENNReal.ofReal_inv_of_pos {x : ℝ} (hx : 0 < x) :

(ENNReal.ofReal x)⁻¹ = ENNReal.ofReal x⁻¹

theorem ENNReal.ofReal_div_of_pos {x : ℝ} {y : ℝ} (hy : 0 < y) :

ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y

@[simp]

theorem ENNReal.toNNReal_mul {a : ENNReal} {b : ENNReal} :

ENNReal.toNNReal (a * b) = ENNReal.toNNReal a * ENNReal.toNNReal b

theorem ENNReal.toNNReal_mul_top (a : ENNReal) :

ENNReal.toNNReal (a * ⊤) = 0

theorem ENNReal.toNNReal_top_mul (a : ENNReal) :

ENNReal.toNNReal (⊤ * a) = 0

@[simp]

theorem ENNReal.smul_toNNReal (a : NNReal) (b : ENNReal) :

ENNReal.toNNReal (a • b) = a * ENNReal.toNNReal b

def ENNReal.toNNRealHom :

ENNReal →* NNReal

ENNReal.toNNReal as a MonoidHom.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ENNReal.toNNReal_pow (a : ENNReal) (n : ℕ) :

ENNReal.toNNReal (a ^ n) = ENNReal.toNNReal a ^ n

@[simp]

theorem ENNReal.toNNReal_prod {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal} :

ENNReal.toNNReal (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => ENNReal.toNNReal (f i)

def ENNReal.toRealHom :

ENNReal →* ℝ

ENNReal.toReal as a MonoidHom.

Equations

ENNReal.toRealHom = MonoidHom.comp (↑NNReal.toRealHom) ENNReal.toNNRealHom

Instances For

@[simp]

theorem ENNReal.toReal_mul {a : ENNReal} {b : ENNReal} :

ENNReal.toReal (a * b) = ENNReal.toReal a * ENNReal.toReal b

theorem ENNReal.toReal_nsmul (a : ENNReal) (n : ℕ) :

ENNReal.toReal (n • a) = n • ENNReal.toReal a

@[simp]

theorem ENNReal.toReal_pow (a : ENNReal) (n : ℕ) :

ENNReal.toReal (a ^ n) = ENNReal.toReal a ^ n

@[simp]

theorem ENNReal.toReal_prod {ι : Type u_1} {s : Finset ι} {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) :

ENNReal.toReal (ENNReal.ofReal c * a) = c * ENNReal.toReal a

theorem ENNReal.toReal_mul_top (a : ENNReal) :

ENNReal.toReal (a * ⊤) = 0

theorem ENNReal.toReal_top_mul (a : ENNReal) :

ENNReal.toReal (⊤ * a) = 0

theorem ENNReal.toReal_eq_toReal {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toReal a = ENNReal.toReal b ↔ a = b

theorem ENNReal.toReal_smul (r : NNReal) (s : ENNReal) :

ENNReal.toReal (r • s) = r • ENNReal.toReal s

theorem ENNReal.trichotomy (p : ENNReal) :

p = 0 ∨ p = ⊤ ∨ 0 < ENNReal.toReal p

theorem ENNReal.trichotomy₂ {p : ENNReal} {q : ENNReal} (hpq : p ≤ q) :

p = 0 ∧ q = 0 ∨ p = 0 ∧ q = ⊤ ∨ p = 0 ∧ 0 < ENNReal.toReal q ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < ENNReal.toReal p ∧ q = ⊤ ∨ 0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q

theorem ENNReal.dichotomy (p : ENNReal) [Fact (1 ≤ p)] :

p = ⊤ ∨ 1 ≤ ENNReal.toReal p

theorem ENNReal.toReal_pos_iff_ne_top (p : ENNReal) [Fact (1 ≤ p)] :

0 < ENNReal.toReal p ↔ p ≠ ⊤

theorem ENNReal.toNNReal_inv (a : ENNReal) :

ENNReal.toNNReal a⁻¹ = (ENNReal.toNNReal a)⁻¹

theorem ENNReal.toNNReal_div (a : ENNReal) (b : ENNReal) :

ENNReal.toNNReal (a / b) = ENNReal.toNNReal a / ENNReal.toNNReal b

theorem ENNReal.toReal_inv (a : ENNReal) :

ENNReal.toReal a⁻¹ = (ENNReal.toReal a)⁻¹

theorem ENNReal.toReal_div (a : ENNReal) (b : ENNReal) :

ENNReal.toReal (a / b) = ENNReal.toReal a / ENNReal.toReal b

theorem ENNReal.ofReal_prod_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℝ} (hf : ∀ i ∈ s, 0 ≤ 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_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

ENNReal.toNNReal (iInf f) = ⨅ (i : ι), ENNReal.toNNReal (f i)

theorem ENNReal.toNNReal_sInf (s : Set ENNReal) (hs : ∀ r ∈ s, r ≠ ⊤) :

ENNReal.toNNReal (sInf s) = sInf (ENNReal.toNNReal '' s)

theorem ENNReal.toNNReal_iSup {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

ENNReal.toNNReal (iSup f) = ⨆ (i : ι), ENNReal.toNNReal (f i)

theorem ENNReal.toNNReal_sSup (s : Set ENNReal) (hs : ∀ r ∈ s, r ≠ ⊤) :

ENNReal.toNNReal (sSup s) = sSup (ENNReal.toNNReal '' s)

theorem ENNReal.toReal_iInf {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

ENNReal.toReal (iInf f) = ⨅ (i : ι), ENNReal.toReal (f i)

theorem ENNReal.toReal_sInf (s : Set ENNReal) (hf : ∀ r ∈ s, r ≠ ⊤) :

ENNReal.toReal (sInf s) = sInf (ENNReal.toReal '' s)

theorem ENNReal.toReal_iSup {ι : Sort u_1} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

ENNReal.toReal (iSup f) = ⨆ (i : ι), ENNReal.toReal (f i)

theorem ENNReal.toReal_sSup (s : Set ENNReal) (hf : ∀ r ∈ s, r ≠ ⊤) :

ENNReal.toReal (sSup s) = sSup (ENNReal.toReal '' s)

theorem ENNReal.iInf_add {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} :

iInf f + a = ⨅ (i : ι), f i + a

theorem ENNReal.iSup_sub {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} :

(⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a

theorem ENNReal.sub_iInf {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} :

a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i

theorem ENNReal.sInf_add {a : ENNReal} {s : Set ENNReal} :

sInf s + a = ⨅ b ∈ s, b + a

theorem ENNReal.add_iInf {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} :

a + iInf f = ⨅ (b : ι), a + f b

theorem ENNReal.iInf_add_iInf {ι : Sort u_1} {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 {ι : Sort u_1} {α : Type u_2} {f : ι → α → ENNReal} {s : Finset α} [Nonempty ι] (h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f 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_2} {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_2} [Nonempty ι] {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_2} [Nonempty ι] {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_2} {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_1} {f : ι → ENNReal} :

⨆ (i : ι), f i = 0 ↔ ∀ (i : ι), f i = 0

@[simp]

theorem ENNReal.iSup_zero_eq_zero {ι : Sort u_1} :

⨆ (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 = ⊤

def Mathlib.Meta.Positivity.evalENNRealOfReal :

Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: ENNReal.ofReal.

Equations

One or more equations did not get rendered due to their size.

Instances For