Lemmas about EReal

theorem EReal.le_of_toReal_le {a b : EReal} (h1 : a ≠ ⊤) (h2 : b ≠ ⊤) (h3 : a ≠ ⊥) (h4 : b ≠ ⊥) (h5 : b.toReal ≤ a.toReal) : b ≤ a

theorem EReal.toReal_log {x : ENNReal} (hx₀ : x ≠ 0) (hxₜ : x ≠ ⊤) : x.log.toReal = Real.log x.toReal

theorem EReal.mul_add_ENNReal {a : ENNReal} {b c : EReal} (hb₀ : 0 ≤ b) (hc₀ : 0 ≤ c) : a * (b + c).toENNReal = a * b.toENNReal + a * c.toENNReal

theorem EReal.toReal_inv (r : EReal) : r⁻¹.toReal = r.toReal⁻¹

theorem EReal.inv_ne_top {r : EReal} : r⁻¹ ≠ ⊤

theorem EReal.toENNReal_inv {r : EReal} (hr : 0 < r) : r⁻¹.toENNReal = r.toENNReal⁻¹

theorem EReal.iSup_coe_mul_of_nonneg {α : Type u_1} [Nonempty α] {f : α → EReal} {a : ℝ} (ha : 0 ≤ a) : ↑a * ⨆ (x : α), f x = ⨆ (x : α), ↑a * f x

theorem EReal.iSup_ennreal_mul {α : Type u_1} [Nonempty α] {f : α → EReal} {a : ENNReal} (ha : a ≠ ⊤) : ↑a * ⨆ (x : α), f x = ⨆ (x : α), ↑a * f x

theorem EReal.inv_coe_ennreal {x : ENNReal} (hx : x ≠ 0) : (↑x)⁻¹ = ↑x⁻¹

theorem EReal.mul_sub_of_nonneg_of_ne_top {a b c : EReal} (ha : 0 ≤ a) (ha' : a ≠ ⊤) : a * (b - c) = a * b - a * c

theorem EReal.add_sub_add (a b : EReal) {c d : EReal} (hc : c ≠ ⊥) (hd : d ≠ ⊥) : a + b - (c + d) = a - c + (b - d)

theorem EReal.mul_sub_of_eq_zero {a b c : EReal} (h : b = 0 ∨ c = 0) : a * (b - c) = a * b - a * c

theorem EReal.ne_bot_of_nonneg {a : EReal} (ha : 0 ≤ a) : a ≠ ⊥

theorem EReal.neg_div (a b : EReal) : -a / b = -(a / b)

@[simp]

theorem EReal.toENNReal_one : toENNReal 1 = 1

theorem EReal.coe_ennreal_div {a b : ENNReal} (hb_zero : b ≠ 0) : ↑(a / b) = ↑a / ↑b

theorem EReal.coe_ennreal_inv {a : ENNReal} (ha : a ≠ 0) : ↑a⁻¹ = (↑a)⁻¹

instance instMeasurableInvEReal_eValues : MeasurableInv EReal

theorem EReal.sub_lt_sub_of_le_of_lt {x y z t : EReal} (h : x ≤ y) (h' : z < t) (hy_top : y ≠ ⊤) (hy_bot : y ≠ ⊥) : x - t < y - z

theorem EReal.top_sub_eq_top_or_bot {a : EReal} : ⊤ - a = ⊤ ∨ ⊤ - a = ⊥

theorem EReal.sub_eq_bot {a b : EReal} : a - b = ⊥ ↔ a = ⊥ ∨ b = ⊤

theorem EReal.add_sub_add_comm {a b c d : EReal} (h1 : c ≠ ⊥ ∨ d ≠ ⊤) (h2 : c ≠ ⊤ ∨ d ≠ ⊥) : a + b - (c + d) = a - c + (b - d)

theorem EReal.coe_ennreal_sub_toENNReal (a b : ENNReal) : (↑a - ↑b).toENNReal = a - b

theorem EReal.neg_coe_ennreal_sub_toENNReal {a b : ENNReal} (h : a ≠ ⊤ ∨ b ≠ ⊤) : (-(↑a - ↑b)).toENNReal = b - a

theorem EReal.ne_top_exists_finite_iff {a : EReal} : a ≠ ⊤ ↔ ∃ (b : EReal), b ≠ ⊤ ∧ a ≤ b

@[implicit_reducible]

noncomputable instance instENormEReal_eValues : ENorm EReal

Equations

• instENormEReal_eValues = { enorm := fun (x : EReal) => (max x 0).toENNReal + (-min x 0).toENNReal }

@[implicit_reducible]

noncomputable instance instSMulNNRealEReal_eValues : SMul NNReal EReal

Equations

• instSMulNNRealEReal_eValues = { smul := fun (c : NNReal) (x : EReal) => ↑↑c * x }

@[implicit_reducible]

noncomputable instance instSMulENNRealEReal_eValues : SMul ENNReal EReal

Equations

• instSMulENNRealEReal_eValues = { smul := fun (c : ENNReal) (x : EReal) => ↑c * x }

@[simp]

theorem EReal.smul_nnreal_eq_mul (c : NNReal) (x : EReal) : c • x = ↑↑c * x

@[simp]

theorem EReal.smul_ennreal_eq_mul (c : ENNReal) (x : EReal) : c • x = ↑c * x

theorem EReal.coe_ennreal_limsup {α : Type} (F : Filter α) [F.NeBot] (g : α → ENNReal) : ↑(Filter.limsup g F) = Filter.limsup (fun (x : α) => ↑(g x)) F

theorem EReal.limsup_coe_ennreal {α : Type} (F : Filter α) [F.NeBot] (g : α → EReal) : (Filter.limsup g F).toENNReal = Filter.limsup (fun (x : α) => (g x).toENNReal) F

theorem EReal.coe_ennreal_liminf {α : Type} (F : Filter α) [F.NeBot] (g : α → ENNReal) : ↑(Filter.liminf g F) = Filter.liminf (fun (x : α) => ↑(g x)) F

theorem EReal.liminf_coe_ennreal {α : Type} (F : Filter α) [F.NeBot] (g : α → EReal) : (Filter.liminf g F).toENNReal = Filter.liminf (fun (x : α) => (g x).toENNReal) F

theorem EReal.distrib_real {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (u : EReal) : (↑a + ↑b) * u = ↑a * u + ↑b * u

theorem EReal.distrib_ennreal (a b : ENNReal) (u : EReal) : (↑a + ↑b) * u = ↑a * u + ↑b * u

theorem EReal.coe_ennreal_mul_sub {c α β : ENNReal} (h : c = ⊤ → α = 0) : ↑c * (↑β - ↑α) = ↑(c * β) - ↑(c * α)

Distributing an ℝ≥0∞ factor over a difference of ℝ≥0∞ values. The hypothesis rules out the bad case ∞ * (β - α) = ∞ versus ∞ * β - ∞ * α = ⊥ with 0 < α < β.