Documentation

TestingLowerBounds.ForMathlib.EReal

instance EReal.instCharZero_testingLowerBounds :

Equations

EReal.instCharZero_testingLowerBounds = ⋯

instance EReal.instNoZeroDivisors_testingLowerBounds :

NoZeroDivisors EReal

Equations

EReal.instNoZeroDivisors_testingLowerBounds = ⋯

theorem EReal.coe_ennreal_toReal {x : ENNReal} (hx : x ≠ ⊤) :

↑x.toReal = ↑x

theorem EReal.lt_neg_iff_lt_neg {x : EReal} {y : EReal} :

x < -y ↔ y < -x

theorem EReal.le_neg_iff_le_neg {x : EReal} {y : EReal} :

x ≤ -y ↔ y ≤ -x

theorem EReal.neg_le_iff_neg_le {x : EReal} {y : EReal} :

-x ≤ y ↔ -y ≤ x

theorem EReal.top_mul_ennreal_coe {x : ENNReal} (hx : x ≠ 0) :

⊤ * ↑x = ⊤

theorem EReal.ennreal_coe_mul_top {x : ENNReal} (hx : x ≠ 0) :

↑x * ⊤ = ⊤

theorem EReal.mul_eq_top (a : EReal) (b : EReal) :

a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤

theorem EReal.mul_ne_top (a : EReal) (b : EReal) :

a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

theorem EReal.mul_eq_bot (a : EReal) (b : EReal) :

a * b = ⊥ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

theorem EReal.mul_ne_bot (a : EReal) (b : EReal) :

a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

theorem EReal.mul_pos_iff {a : EReal} {b : EReal} :

0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

theorem EReal.mul_neg_iff {a : EReal} {b : EReal} :

a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

theorem EReal.mul_nonneg_iff {a : EReal} {b : EReal} :

0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem EReal.mul_nonpos_iff {a : EReal} {b : EReal} :

a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

theorem EReal.add_ne_top {x : EReal} {y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :

theorem EReal.add_ne_top_iff_of_ne_bot {x : EReal} {y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) :

x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

theorem EReal.add_ne_top_iff_of_ne_bot_of_ne_top {x : EReal} {y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) :

x + y ≠ ⊤ ↔ x ≠ ⊤

theorem EReal.add_ne_bot_iff {x : EReal} {y : EReal} :

x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

theorem EReal.add_ne_bot {x : EReal} {y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) :

theorem EReal.coe_mul_add_of_nonneg {x : ℝ} (hx_nonneg : 0 ≤ x) (y : EReal) (z : EReal) :

↑x * (y + z) = ↑x * y + ↑x * z

theorem EReal.add_mul_coe_of_nonneg {x : ℝ} (hx_nonneg : 0 ≤ x) (y : EReal) (z : EReal) :

(y + z) * ↑x = y * ↑x + z * ↑x

theorem EReal.add_sub_cancel (x : EReal) (y : ℝ) :

x + ↑y - ↑y = x

theorem EReal.add_sub_cancel' (x : EReal) (y : ℝ) :

↑y + x - ↑y = x

@[simp]

theorem EReal.sub_self {x : EReal} (h_top : x ≠ ⊤) (h_bot : x ≠ ⊥) :

x - x = 0

theorem EReal.sub_self_le_zero {x : EReal} :

x - x ≤ 0

theorem EReal.top_sub_of_ne_top {x : EReal} (hx : x ≠ ⊤) :

theorem EReal.top_mul_add_of_nonneg {x : EReal} {y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) :

⊤ * (x + y) = ⊤ * x + ⊤ * y

theorem EReal.mul_add_coe_of_nonneg (x : EReal) {y : ℝ} {z : ℝ} (hy : 0 ≤ y) (hz : 0 ≤ z) :

x * (↑y + ↑z) = x * ↑y + x * ↑z

theorem EReal.coe_add_mul_of_nonneg (x : EReal) {y : ℝ} {z : ℝ} (hy : 0 ≤ y) (hz : 0 ≤ z) :

(↑y + ↑z) * x = ↑y * x + ↑z * x

theorem EReal.toReal_nonneg {x : EReal} (hx : 0 ≤ x) :

0 ≤ x.toReal

theorem EReal.toReal_nonpos {x : EReal} (hx : x ≤ 0) :

x.toReal ≤ 0

theorem EReal.toReal_ne_zero_iff {x : EReal} :

x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥

theorem EReal.toReal_eq_zero_iff {x : EReal} :

x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥

theorem EReal.sub_nonneg {x : EReal} {y : EReal} (hy : y ≠ ⊤) (hy' : y ≠ ⊥) :

0 ≤ x - y ↔ y ≤ x

theorem EReal.sub_nonpos {x : EReal} {y : EReal} (hy : y ≠ ⊤) (hy' : y ≠ ⊥) :

x - y ≤ 0 ↔ x ≤ y

@[simp]

theorem EReal.nsmul_eq_mul {n : ℕ} {x : EReal} :

n • x = ↑n * x

theorem EReal.lowerSemicontinuous_add :

LowerSemicontinuous fun (p : EReal × EReal) => p.1 + p.2

instance EReal.instMeasurableAdd₂_testingLowerBounds :

MeasurableAdd₂ EReal

Equations

EReal.instMeasurableAdd₂_testingLowerBounds = ⋯

theorem EReal.measurable_from_prod_countable'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [Countable β] [MeasurableSingletonClass β] {f : β × α → γ} (hf : ∀ (y : β), Measurable fun (x : α) => f (y, x)) :

theorem EReal.measurable_of_measurable_real_prod {β : Type u_2} {γ : Type u_3} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : EReal × β → γ} (h_real : Measurable fun (p : ℝ × β) => f (↑p.1, p.2)) (h_bot : Measurable fun (x : β) => f (⊥, x)) (h_top : Measurable fun (x : β) => f (⊤, x)) :

theorem EReal.measurable_of_measurable_real_real {β : Type u_2} {mβ : MeasurableSpace β} {f : EReal × EReal → β} (h_real : Measurable fun (p : ℝ × ℝ) => f (↑p.1, ↑p.2)) (h_bot_left : Measurable fun (r : ℝ) => f (⊥, ↑r)) (h_top_left : Measurable fun (r : ℝ) => f (⊤, ↑r)) (h_bot_right : Measurable fun (r : ℝ) => f (↑r, ⊥)) (h_top_right : Measurable fun (r : ℝ) => f (↑r, ⊤)) :

instance EReal.instMeasurableMul₂_testingLowerBounds :

MeasurableMul₂ EReal

Equations

EReal.instMeasurableMul₂_testingLowerBounds = ⋯

noncomputable def EReal.toENNReal (x : EReal) :

Reinterpret an EReal number x as an ENNReal number. Returns 0 if x < 0.

Equations

x.toENNReal = if x = ⊤ then ⊤ else ENNReal.ofReal x.toReal

Instances For

@[simp]

theorem EReal.toENNReal_top :

⊤.toENNReal = ⊤

@[simp]

theorem EReal.toENNReal_of_ne_top {x : EReal} (hx : x ≠ ⊤) :

x.toENNReal = ENNReal.ofReal x.toReal

@[simp]

theorem EReal.toENNReal_eq_top_iff {x : EReal} :

x.toENNReal = ⊤ ↔ x = ⊤

theorem EReal.toENNReal_ne_top_iff {x : EReal} :

x.toENNReal ≠ ⊤ ↔ x ≠ ⊤

@[simp]

theorem EReal.toENNReal_of_nonpos {x : EReal} (hx : x ≤ 0) :

x.toENNReal = 0

theorem EReal.toENNReal_eq_zero_iff {x : EReal} :

x.toENNReal = 0 ↔ x ≤ 0

theorem EReal.toENNReal_ne_zero_iff {x : EReal} :

x.toENNReal ≠ 0 ↔ 0 < x

@[simp]

theorem EReal.coe_toENNReal {x : EReal} (hx : 0 ≤ x) :

↑x.toENNReal = x

@[simp]

theorem EReal.toENNReal_coe {x : ENNReal} :

(↑x).toENNReal = x

theorem EReal.toENNReal_le_toENNReal {x : EReal} {y : EReal} (h : x ≤ y) :

x.toENNReal ≤ y.toENNReal

@[simp]

theorem EReal.real_coe_toENNReal (x : ℝ) :

(↑x).toENNReal = ENNReal.ofReal x

@[simp]

theorem EReal.toReal_toENNReal {x : EReal} (hx : 0 ≤ x) :

x.toENNReal.toReal = x.toReal

theorem measurable_ereal_toENNReal :

Measurable EReal.toENNReal

theorem Measurable.ereal_toENNReal {α : Type u_1} :

∀ {x : MeasurableSpace α} {f : α → EReal}, Measurable f → Measurable fun (x : α) => (f x).toENNReal

theorem EReal.toENNReal_add {x : EReal} {y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) :

(x + y).toENNReal = x.toENNReal + y.toENNReal

theorem EReal.toENNReal_sub {x : EReal} {y : EReal} (hy : 0 ≤ y) :

(x - y).toENNReal = x.toENNReal - y.toENNReal

theorem EReal.toENNReal_mul {x : EReal} {y : EReal} (hx : 0 ≤ x) :

(x * y).toENNReal = x.toENNReal * y.toENNReal

theorem EReal.toENNReal_mul' {x : EReal} {y : EReal} (hy : 0 ≤ y) :

(x * y).toENNReal = x.toENNReal * y.toENNReal

theorem ENNReal.toEReal_sub {x : ENNReal} {y : ENNReal} (hy_top : y ≠ ⊤) (h_le : y ≤ x) :

↑(x - y) = ↑x - ↑y

theorem ENNReal.min_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} :

min a b * c = min (a * c) (b * c)

theorem ENNReal.mul_min {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a * min b c = min (a * b) (a * c)

@[simp]

theorem ENNReal.toReal_toEReal_of_ne_top {x : ENNReal} (hx : x ≠ ⊤) :

↑x.toReal = ↑x