Results about division in extended non-negative reals

This file establishes basic properties related to the inversion and division operations on ℝ≥0∞. For instance, as a consequence of being a DivInvOneMonoid, ℝ≥0∞ inherits a power operation with integer exponent.

Main results

A few order isomorphisms are worthy of mention:

• OrderIso.invENNReal : ℝ≥0∞ ≃o ℝ≥0∞ᵒᵈ: The map x ↦ x⁻¹ as an order isomorphism to the dual.

• orderIsoIicOneBirational : ℝ≥0∞ ≃o Iic (1 : ℝ≥0∞): The birational order isomorphism between ℝ≥0∞ and the unit interval Set.Iic (1 : ℝ≥0∞) given by x ↦ (x⁻¹ + 1)⁻¹ with inverse x ↦ (x⁻¹ - 1)⁻¹

• orderIsoIicCoe (a : ℝ≥0) : Iic (a : ℝ≥0∞) ≃o Iic a: Order isomorphism between an initial interval in ℝ≥0∞ and an initial interval in ℝ≥0 given by the identity map.

• orderIsoUnitIntervalBirational : ℝ≥0∞ ≃o Icc (0 : ℝ) 1: An order isomorphism between the extended nonnegative real numbers and the unit interval. This is orderIsoIicOneBirational composed with the identity order isomorphism between Iic (1 : ℝ≥0∞) and Icc (0 : ℝ) 1.

theorem ENNReal.div_eq_inv_mul {a b : ENNReal} : a / b = b⁻¹ * a

@[simp]

theorem ENNReal.inv_zero : 0⁻¹ = ⊤

@[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)⁻¹

theorem ENNReal.coe_inv_two : ↑2⁻¹ = 2⁻¹

@[simp]

theorem ENNReal.coe_div {r p : NNReal} (hr : r ≠ 0) : ↑(p / r) = ↑p / ↑r

theorem ENNReal.coe_div_le {r p : NNReal} : ↑(p / r) ≤ ↑p / ↑r

theorem ENNReal.div_zero {a : ENNReal} (h : a ≠ 0) : a / 0 = ⊤

instance ENNReal.instDivInvOneMonoid : DivInvOneMonoid ENNReal

Equations

• ENNReal.instDivInvOneMonoid = DivInvOneMonoid.mk ENNReal.instDivInvOneMonoid.proof_1

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.inv_mul_cancel_left' {a b : ENNReal} (ha₀ : a = 0 → b = 0) (ha : a = ⊤ → b = 0) : a⁻¹ * (a * b) = b

See ENNReal.inv_mul_cancel_left for a simpler version assuming a ≠ 0, a ≠ ∞.

theorem ENNReal.inv_mul_cancel_left {a b : ENNReal} (ha₀ : a ≠ 0) (ha : a ≠ ⊤) : a⁻¹ * (a * b) = b

See ENNReal.inv_mul_cancel_left' for a stronger version.

theorem ENNReal.mul_inv_cancel_left' {a b : ENNReal} (ha₀ : a = 0 → b = 0) (ha : a = ⊤ → b = 0) : a * (a⁻¹ * b) = b

See ENNReal.mul_inv_cancel_left for a simpler version assuming a ≠ 0, a ≠ ∞.

theorem ENNReal.mul_inv_cancel_left {a b : ENNReal} (ha₀ : a ≠ 0) (ha : a ≠ ⊤) : a * (a⁻¹ * b) = b

See ENNReal.mul_inv_cancel_left' for a stronger version.

theorem ENNReal.mul_inv_cancel_right' {a b : ENNReal} (hb₀ : b = 0 → a = 0) (hb : b = ⊤ → a = 0) : a * b * b⁻¹ = a

See ENNReal.mul_inv_cancel_right for a simpler version assuming b ≠ 0, b ≠ ∞.

theorem ENNReal.mul_inv_cancel_right {a b : ENNReal} (hb₀ : b ≠ 0) (hb : b ≠ ⊤) : a * b * b⁻¹ = a

See ENNReal.mul_inv_cancel_right' for a stronger version.

theorem ENNReal.inv_mul_cancel_right' {a b : ENNReal} (hb₀ : b = 0 → a = 0) (hb : b = ⊤ → a = 0) : a * b⁻¹ * b = a

See ENNReal.inv_mul_cancel_right for a simpler version assuming b ≠ 0, b ≠ ∞.

theorem ENNReal.inv_mul_cancel_right {a b : ENNReal} (hb₀ : b ≠ 0) (hb : b ≠ ⊤) : a * b⁻¹ * b = a

See ENNReal.inv_mul_cancel_right' for a stronger version.

theorem ENNReal.mul_div_cancel_right' {a b : ENNReal} (hb₀ : b = 0 → a = 0) (hb : b = ⊤ → a = 0) : a * b / b = a

See ENNReal.mul_div_cancel_right for a simpler version assuming b ≠ 0, b ≠ ∞.

theorem ENNReal.mul_div_cancel_right {a b : ENNReal} (hb₀ : b ≠ 0) (hb : b ≠ ⊤) : a * b / b = a

See ENNReal.mul_div_cancel_right' for a stronger version.

theorem ENNReal.div_mul_cancel' {a b : ENNReal} (ha₀ : a = 0 → b = 0) (ha : a = ⊤ → b = 0) : b / a * a = b

See ENNReal.div_mul_cancel for a simpler version assuming a ≠ 0, a ≠ ∞.

theorem ENNReal.div_mul_cancel {a b : ENNReal} (ha₀ : a ≠ 0) (ha : a ≠ ⊤) : b / a * a = b

See ENNReal.div_mul_cancel' for a stronger version.

theorem ENNReal.mul_div_cancel' {a b : ENNReal} (ha₀ : a = 0 → b = 0) (ha : a = ⊤ → b = 0) : a * (b / a) = b

See ENNReal.mul_div_cancel for a simpler version assuming a ≠ 0, a ≠ ∞.

theorem ENNReal.mul_div_cancel {a b : ENNReal} (ha₀ : a ≠ 0) (ha : a ≠ ⊤) : a * (b / a) = b

See ENNReal.mul_div_cancel' for a stronger version.

theorem ENNReal.mul_comm_div {a b c : ENNReal} : a / b * c = a * (c / b)

theorem ENNReal.mul_div_right_comm {a b c : ENNReal} : a * b / c = a / c * b

instance ENNReal.instInvolutiveInv : InvolutiveInv ENNReal

Equations

• ENNReal.instInvolutiveInv = InvolutiveInv.mk ENNReal.instInvolutiveInv.proof_1

@[simp]

theorem ENNReal.inv_eq_one {a : ENNReal} : a⁻¹ = 1 ↔ a = 1

@[simp]

theorem ENNReal.inv_eq_top {a : ENNReal} : a⁻¹ = ⊤ ↔ a = 0

theorem ENNReal.inv_ne_top {a : ENNReal} : a⁻¹ ≠ ⊤ ↔ a ≠ 0

theorem ENNReal.Finiteness.inv_ne_top {a : ENNReal} : a ≠ 0 → a⁻¹ ≠ ⊤

Alias of the reverse direction of ENNReal.inv_ne_top.

@[simp]

theorem ENNReal.inv_lt_top {x : ENNReal} : x⁻¹ < ⊤ ↔ 0 < x

theorem ENNReal.div_lt_top {x y : ENNReal} (h1 : x ≠ ⊤) (h2 : y ≠ 0) : x / y < ⊤

@[simp]

theorem ENNReal.inv_eq_zero {a : ENNReal} : a⁻¹ = 0 ↔ a = ⊤

theorem ENNReal.inv_ne_zero {a : ENNReal} : a⁻¹ ≠ 0 ↔ a ≠ ⊤

theorem ENNReal.div_pos {a b : ENNReal} (ha : a ≠ 0) (hb : b ≠ ⊤) : 0 < a / b

theorem ENNReal.inv_mul_le_iff {x y z : ENNReal} (h1 : x ≠ 0) (h2 : x ≠ ⊤) : x⁻¹ * y ≤ z ↔ y ≤ x * z

theorem ENNReal.mul_inv_le_iff {x y z : ENNReal} (h1 : y ≠ 0) (h2 : y ≠ ⊤) : x * y⁻¹ ≤ z ↔ x ≤ z * y

theorem ENNReal.div_le_iff {x y z : ENNReal} (h1 : y ≠ 0) (h2 : y ≠ ⊤) : x / y ≤ z ↔ x ≤ z * y

theorem ENNReal.div_le_iff' {x y z : ENNReal} (h1 : y ≠ 0) (h2 : y ≠ ⊤) : x / y ≤ z ↔ x ≤ y * z

theorem ENNReal.mul_inv {a b : ENNReal} (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : a ≠ ⊤ ∨ b ≠ 0) : (a * b)⁻¹ = a⁻¹ * b⁻¹

theorem ENNReal.inv_div {a b : ENNReal} (htop : b ≠ ⊤ ∨ a ≠ ⊤) (hzero : b ≠ 0 ∨ a ≠ 0) : (a / b)⁻¹ = b / a

theorem ENNReal.prod_inv_distrib {ι : Type u_1} {f : ι → ENNReal} {s : Finset ι} (hf : (↑s).Pairwise fun (i j : ι) => f i ≠ 0 ∨ f j ≠ ⊤) : (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹

theorem ENNReal.mul_div_mul_left {c : ENNReal} (a b : ENNReal) (hc : c ≠ 0) (hc' : c ≠ ⊤) : c * a / (c * b) = a / b

theorem ENNReal.mul_div_mul_right {c : ENNReal} (a b : ENNReal) (hc : c ≠ 0) (hc' : c ≠ ⊤) : a * c / (b * c) = a / b

theorem ENNReal.sub_div {a b c : ENNReal} (h : 0 < b → b < a → c ≠ 0) : (a - b) / c = a / c - b / c

@[simp]

theorem ENNReal.inv_pos {a : ENNReal} : 0 < a⁻¹ ↔ a ≠ ⊤

theorem ENNReal.inv_strictAnti : StrictAnti Inv.inv

@[simp]

theorem ENNReal.inv_lt_inv {a b : ENNReal} : a⁻¹ < b⁻¹ ↔ b < a

theorem ENNReal.inv_lt_iff_inv_lt {a b : ENNReal} : a⁻¹ < b ↔ b⁻¹ < a

theorem ENNReal.lt_inv_iff_lt_inv {a b : ENNReal} : a < b⁻¹ ↔ b < a⁻¹

@[simp]

theorem ENNReal.inv_le_inv {a b : ENNReal} : a⁻¹ ≤ b⁻¹ ↔ b ≤ a

theorem ENNReal.inv_le_iff_inv_le {a b : ENNReal} : a⁻¹ ≤ b ↔ b⁻¹ ≤ a

theorem ENNReal.le_inv_iff_le_inv {a b : ENNReal} : a ≤ b⁻¹ ↔ b ≤ a⁻¹

theorem ENNReal.inv_le_inv' {a b : ENNReal} (h : a ≤ b) : b⁻¹ ≤ a⁻¹

theorem ENNReal.inv_lt_inv' {a b : ENNReal} (h : a < b) : b⁻¹ < a⁻¹

@[simp]

theorem ENNReal.inv_le_one {a : ENNReal} : a⁻¹ ≤ 1 ↔ 1 ≤ a

theorem ENNReal.one_le_inv {a : ENNReal} : 1 ≤ a⁻¹ ↔ a ≤ 1

@[simp]

theorem ENNReal.inv_lt_one {a : ENNReal} : a⁻¹ < 1 ↔ 1 < a

@[simp]

theorem ENNReal.one_lt_inv {a : ENNReal} : 1 < a⁻¹ ↔ a < 1

def OrderIso.invENNReal : ENNReal ≃o ENNRealᵒᵈ

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

Equations

• OrderIso.invENNReal = { toEquiv := Equiv.trans (Equiv.inv ENNReal) OrderDual.toDual, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.invENNReal_apply (a✝ : ENNReal) : OrderIso.invENNReal a✝ = (OrderDual.toDual a✝)⁻¹

@[simp]

theorem OrderIso.invENNReal_symm_apply (a : ENNRealᵒᵈ) : OrderIso.invENNReal.symm 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 ⊤

theorem ENNReal.top_div_of_ne_top {a : ENNReal} (h : a ≠ ⊤) : ⊤ / a = ⊤

@[simp]

theorem ENNReal.top_div_coe {p : NNReal} : ⊤ / ↑p = ⊤

theorem ENNReal.top_div_of_lt_top {a : ENNReal} (h : a < ⊤) : ⊤ / a = ⊤

@[simp]

theorem ENNReal.zero_div {a : ENNReal} : 0 / a = 0

theorem ENNReal.div_eq_top {a b : ENNReal} : a / b = ⊤ ↔ a ≠ 0 ∧ b = 0 ∨ a = ⊤ ∧ b ≠ ⊤

theorem ENNReal.le_div_iff_mul_le {a b c : ENNReal} (h0 : b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ⊤ ∨ c ≠ ⊤) : a ≤ c / b ↔ a * b ≤ c

theorem ENNReal.div_le_iff_le_mul {a b c : ENNReal} (hb0 : b ≠ 0 ∨ c ≠ ⊤) (hbt : b ≠ ⊤ ∨ c ≠ 0) : a / b ≤ c ↔ a ≤ c * b

theorem ENNReal.lt_div_iff_mul_lt {a b c : ENNReal} (hb0 : b ≠ 0 ∨ c ≠ ⊤) (hbt : b ≠ ⊤ ∨ c ≠ 0) : c < a / b ↔ c * b < a

theorem ENNReal.div_le_of_le_mul {a b c : ENNReal} (h : a ≤ b * c) : a / c ≤ b

theorem ENNReal.div_le_of_le_mul' {a b c : ENNReal} (h : a ≤ b * c) : a / b ≤ c

@[simp]

theorem ENNReal.div_self_le_one {a : ENNReal} : a / a ≤ 1

@[simp]

theorem ENNReal.mul_inv_le_one (a : ENNReal) : a * a⁻¹ ≤ 1

@[simp]

theorem ENNReal.inv_mul_le_one (a : ENNReal) : a⁻¹ * a ≤ 1

@[simp]

theorem ENNReal.mul_inv_ne_top (a : ENNReal) : a * a⁻¹ ≠ ⊤

@[simp]

theorem ENNReal.inv_mul_ne_top (a : ENNReal) : a⁻¹ * a ≠ ⊤

theorem ENNReal.mul_le_of_le_div {a b c : ENNReal} (h : a ≤ b / c) : a * c ≤ b

theorem ENNReal.mul_le_of_le_div' {a b c : ENNReal} (h : a ≤ b / c) : c * a ≤ b

theorem ENNReal.div_lt_iff {a b c : ENNReal} (h0 : b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ⊤ ∨ c ≠ ⊤) : c / b < a ↔ c < a * b

theorem ENNReal.mul_lt_of_lt_div {a b c : ENNReal} (h : a < b / c) : a * c < b

theorem ENNReal.mul_lt_of_lt_div' {a b c : ENNReal} (h : a < b / c) : c * a < b

theorem ENNReal.div_lt_of_lt_mul {a b c : ENNReal} (h : a < b * c) : a / c < b

theorem ENNReal.div_lt_of_lt_mul' {a b c : ENNReal} (h : a < b * c) : a / b < c

theorem ENNReal.inv_le_iff_le_mul {a b : ENNReal} (h₁ : b = ⊤ → a ≠ 0) (h₂ : a = ⊤ → b ≠ 0) : a⁻¹ ≤ b ↔ 1 ≤ a * b

@[simp]

theorem ENNReal.le_inv_iff_mul_le {a b : ENNReal} : a ≤ b⁻¹ ↔ a * b ≤ 1

theorem ENNReal.div_le_div {a b c d : ENNReal} (hab : a ≤ b) (hdc : d ≤ c) : a / c ≤ b / d

theorem ENNReal.div_le_div_left {a b : ENNReal} (h : a ≤ b) (c : ENNReal) : c / b ≤ c / a

theorem ENNReal.div_le_div_right {a b : ENNReal} (h : a ≤ b) (c : ENNReal) : a / c ≤ b / c

theorem ENNReal.eq_inv_of_mul_eq_one_left {a b : ENNReal} (h : a * b = 1) : a = b⁻¹

theorem ENNReal.mul_le_iff_le_inv {a b r : ENNReal} (hr₀ : r ≠ 0) (hr₁ : r ≠ ⊤) : r * a ≤ b ↔ a ≤ r⁻¹ * b

instance ENNReal.instPosSMulStrictMonoNNReal : PosSMulStrictMono NNReal ENNReal

instance ENNReal.instSMulPosMonoNNReal : SMulPosMono NNReal ENNReal

theorem ENNReal.le_of_forall_nnreal_lt {x y : ENNReal} (h : ∀ (r : NNReal), ↑r < x → ↑r ≤ y) : x ≤ y

theorem ENNReal.le_of_forall_pos_nnreal_lt {x y : ENNReal} (h : ∀ (r : NNReal), 0 < r → ↑r < x → ↑r ≤ y) : x ≤ y

theorem ENNReal.eq_top_of_forall_nnreal_le {x : ENNReal} (h : ∀ (r : NNReal), ↑r ≤ x) : x = ⊤

theorem ENNReal.add_div {a b c : ENNReal} : (a + b) / c = a / c + b / c

theorem ENNReal.div_add_div_same {a b 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 b : ENNReal} : a * (b / a) ≤ b

theorem ENNReal.eq_div_iff {a b c : ENNReal} (ha : a ≠ 0) (ha' : a ≠ ⊤) : b = c / a ↔ a * b = c

theorem ENNReal.div_eq_div_iff {a b c 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 b : ENNReal} (hb₀ : b ≠ 0) (hb₁ : b ≠ ⊤) : a / b = 1 ↔ a = b

theorem ENNReal.inv_two_add_inv_two : 2⁻¹ + 2⁻¹ = 1

theorem ENNReal.inv_three_add_inv_three : 3⁻¹ + 3⁻¹ + 3⁻¹ = 1

@[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 b : ENNReal} : a / b = 0 ↔ a = 0 ∨ b = ⊤

@[simp]

theorem ENNReal.div_pos_iff {a b : ENNReal} : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤

theorem ENNReal.div_ne_zero {a b : ENNReal} : a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ⊤

theorem ENNReal.half_pos {a : ENNReal} (h : a ≠ 0) : 0 < a / 2

theorem ENNReal.one_half_lt_one : 2⁻¹ < 1

theorem ENNReal.half_lt_self {a : ENNReal} (hz : a ≠ 0) (ht : a ≠ ⊤) : a / 2 < a

theorem ENNReal.half_le_self {a : ENNReal} : a / 2 ≤ a

theorem ENNReal.sub_half {a : ENNReal} (h : a ≠ ⊤) : a - a / 2 = a / 2

@[simp]

theorem ENNReal.one_sub_inv_two : 1 - 2⁻¹ = 2⁻¹

theorem ENNReal.mul_le_of_forall_lt {a b c : ENNReal} (h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c) : a * b ≤ c

theorem ENNReal.le_mul_of_forall_lt {a b c : ENNReal} (h₁ : a ≠ 0 ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ b ≠ 0) (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b

def ENNReal.orderIsoIicOneBirational : ENNReal ≃o ↑(Set.Iic 1)

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

Equations

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

@[simp]

theorem ENNReal.orderIsoIicOneBirational_apply_coe (x : ENNReal) : ↑(ENNReal.orderIsoIicOneBirational x) = (x⁻¹ + 1)⁻¹

@[simp]

theorem ENNReal.orderIsoIicOneBirational_symm_apply (x : ↑(Set.Iic 1)) : ENNReal.orderIsoIicOneBirational.symm x = ((↑x)⁻¹ - 1)⁻¹

def ENNReal.orderIsoIicCoe (a : NNReal) : ↑(Set.Iic ↑a) ≃o ↑(Set.Iic a)

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

Equations

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

@[simp]

theorem ENNReal.orderIsoIicCoe_apply_coe (a : NNReal) (a✝ : ↑(Set.Iic ↑a)) : ↑((ENNReal.orderIsoIicCoe a) a✝) = (↑a✝).toNNReal

@[simp]

theorem ENNReal.orderIsoIicCoe_symm_apply_coe (a : NNReal) (b : ↑(Set.Iic a)) : ↑((ENNReal.orderIsoIicCoe a).symm b) = ↑↑b

def ENNReal.orderIsoUnitIntervalBirational : ENNReal ≃o ↑(Set.Icc 0 1)

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

Equations

• ENNReal.orderIsoUnitIntervalBirational = ENNReal.orderIsoIicOneBirational.trans ((ENNReal.orderIsoIicCoe 1).trans (NNReal.orderIsoIccZeroCoe 1).symm)

@[simp]

theorem ENNReal.orderIsoUnitIntervalBirational_apply_coe (x : ENNReal) : ↑(ENNReal.orderIsoUnitIntervalBirational x) = (x⁻¹ + 1)⁻¹.toReal

theorem ENNReal.exists_inv_nat_lt {a : ENNReal} (h : a ≠ 0) : ∃ (n : ℕ), (↑n)⁻¹ < a

theorem ENNReal.exists_nat_pos_mul_gt {a b : ENNReal} (ha : a ≠ 0) (hb : b ≠ ⊤) : ∃ n > 0, b < ↑n * a

theorem ENNReal.exists_nat_mul_gt {a b : ENNReal} (ha : a ≠ 0) (hb : b ≠ ⊤) : ∃ (n : ℕ), b < ↑n * a

theorem ENNReal.exists_nat_pos_inv_mul_lt {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ 0) : ∃ n > 0, (↑n)⁻¹ * a < b

theorem ENNReal.exists_nnreal_pos_mul_lt {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ 0) : ∃ 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 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 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 ≠ ⊤) : Set.Ioo 0 ⊤ = ⋃ (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_1 : ℤ) => x ^ x_1

theorem ENNReal.zpow_add {x : ENNReal} (hx : x ≠ 0) (h'x : x ≠ ⊤) (m n : ℤ) : x ^ (m + n) = x ^ m * x ^ n

theorem ENNReal.zpow_neg {x : ENNReal} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m : ℤ) : x ^ (-m) = (x ^ m)⁻¹

theorem ENNReal.zpow_sub {x : ENNReal} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m n : ℤ) : x ^ (m - n) = x ^ m * (x ^ n)⁻¹

@[simp]

theorem ENNReal.iSup_eq_zero {ι : Sort u_1} {f : ι → ENNReal} : ⨆ (i : ι), f i = 0 ↔ ∀ (i : ι), f i = 0

@[simp]

theorem ENNReal.iSup_zero {ι : Sort u_1} : ⨆ (x : ι), 0 = 0

@[deprecated ENNReal.iSup_zero]

theorem ENNReal.iSup_zero_eq_zero {ι : Sort u_1} : ⨆ (x : ι), 0 = 0

Alias of ENNReal.iSup_zero.

theorem ENNReal.iSup_natCast : ⨆ (n : ℕ), ↑n = ⊤

@[simp]

theorem ENNReal.iSup_lt_eq_self (a : ENNReal) : ⨆ (b : ENNReal), ⨆ (_ : b < a), b = a

theorem ENNReal.isUnit_iff {a : ENNReal} : IsUnit a ↔ a ≠ 0 ∧ a ≠ ⊤

def ENNReal.mulLeftOrderIso (a : ENNReal) (ha : IsUnit a) : ENNReal ≃o ENNReal

Left multiplication by a nonzero finite a as an order isomorphism.

Equations

• a.mulLeftOrderIso ha = { toEquiv := ha.unit.mulLeft, map_rel_iff' := ⋯ }

@[simp]

theorem ENNReal.mulLeftOrderIso_symm_apply (a : ENNReal) (ha : IsUnit a) (x : ENNReal) : (RelIso.symm (a.mulLeftOrderIso ha)) x = ↑ha.unit⁻¹ * x

@[simp]

theorem ENNReal.mulLeftOrderIso_toEquiv (a : ENNReal) (ha : IsUnit a) : (a.mulLeftOrderIso ha).toEquiv = ha.unit.mulLeft

@[simp]

theorem ENNReal.mulLeftOrderIso_apply (a : ENNReal) (ha : IsUnit a) (x : ENNReal) : (a.mulLeftOrderIso ha) x = a * x

def ENNReal.mulRightOrderIso (a : ENNReal) (ha : IsUnit a) : ENNReal ≃o ENNReal

Right multiplication by a nonzero finite a as an order isomorphism.

Equations

• a.mulRightOrderIso ha = { toEquiv := ha.unit.mulRight, map_rel_iff' := ⋯ }

@[simp]

theorem ENNReal.mulRightOrderIso_toEquiv (a : ENNReal) (ha : IsUnit a) : (a.mulRightOrderIso ha).toEquiv = ha.unit.mulRight

@[simp]

theorem ENNReal.mulRightOrderIso_apply (a : ENNReal) (ha : IsUnit a) (x : ENNReal) : (a.mulRightOrderIso ha) x = x * a

@[simp]

theorem ENNReal.mulRightOrderIso_symm_apply (a : ENNReal) (ha : IsUnit a) (x : ENNReal) : (RelIso.symm (a.mulRightOrderIso ha)) x = x * ↑ha.unit⁻¹

theorem ENNReal.mul_iSup {ι : Sort u_1} (a : ENNReal) (f : ι → ENNReal) : a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

theorem ENNReal.iSup_mul {ι : Sort u_1} (f : ι → ENNReal) (a : ENNReal) : (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a

theorem ENNReal.mul_sSup {s : Set ENNReal} {a : ENNReal} : a * sSup s = ⨆ b ∈ s, a * b

theorem ENNReal.sSup_mul {s : Set ENNReal} {a : ENNReal} : sSup s * a = ⨆ b ∈ s, b * a

theorem ENNReal.iSup_div {ι : Sort u_1} (f : ι → ENNReal) (a : ENNReal) : iSup f / a = ⨆ (i : ι), f i / a

theorem ENNReal.sSup_div (s : Set ENNReal) (a : ENNReal) : sSup s / a = ⨆ b ∈ s, b / a

theorem ENNReal.mul_iInf' {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} (hinfty : a = ⊤ → ⨅ (i : ι), f i = 0 → ∃ (i : ι), f i = 0) (h₀ : a = 0 → Nonempty ι) : a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

Very general version for distributivity of multiplication over an infimum.

See ENNReal.mul_iInf_of_ne for the special case assuming a ≠ 0 and a ≠ ∞, and ENNReal.mul_iInf for the special case assuming Nonempty ι.

theorem ENNReal.iInf_mul' {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} (hinfty : a = ⊤ → ⨅ (i : ι), f i = 0 → ∃ (i : ι), f i = 0) (h₀ : a = 0 → Nonempty ι) : (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

Very general version for distributivity of multiplication over an infimum.

See ENNReal.iInf_mul_of_ne for the special case assuming a ≠ 0 and a ≠ ∞, and ENNReal.iInf_mul for the special case assuming Nonempty ι.

theorem ENNReal.mul_iInf_of_ne {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} (ha₀ : a ≠ 0) (ha : a ≠ ⊤) : a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

If a ≠ 0 and a ≠ ∞, then right multiplication by a maps infimum to infimum.

See ENNReal.mul_iInf' for the general case, and ENNReal.iInf_mul for another special case that assumes Nonempty ι but does not require a ≠ 0, and ENNReal.

theorem ENNReal.iInf_mul_of_ne {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} (ha₀ : a ≠ 0) (ha : a ≠ ⊤) : (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

If a ≠ 0 and a ≠ ∞, then right multiplication by a maps infimum to infimum.

See ENNReal.iInf_mul' for the general case, and ENNReal.iInf_mul for another special case that assumes Nonempty ι but does not require a ≠ 0.

theorem ENNReal.mul_iInf {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι] (hinfty : a = ⊤ → ⨅ (i : ι), f i = 0 → ∃ (i : ι), f i = 0) : a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

See ENNReal.mul_iInf' for the general case, and ENNReal.mul_iInf_of_ne for another special case that assumes a ≠ 0 but does not require Nonempty ι.

theorem ENNReal.iInf_mul {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι] (hinfty : a = ⊤ → ⨅ (i : ι), f i = 0 → ∃ (i : ι), f i = 0) : (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

See ENNReal.iInf_mul' for the general case, and ENNReal.iInf_mul_of_ne for another special case that assumes a ≠ 0 but does not require Nonempty ι.

theorem ENNReal.iInf_div' {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} (hinfty : a = 0 → ⨅ (i : ι), f i = 0 → ∃ (i : ι), f i = 0) (h₀ : a = ⊤ → Nonempty ι) : (⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a

Very general version for distributivity of division over an infimum.

See ENNReal.iInf_div_of_ne for the special case assuming a ≠ 0 and a ≠ ∞, and ENNReal.iInf_div for the special case assuming Nonempty ι.

theorem ENNReal.iInf_div_of_ne {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} (ha₀ : a ≠ 0) (ha : a ≠ ⊤) : (⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a

If a ≠ 0 and a ≠ ∞, then division by a maps infimum to infimum.

See ENNReal.iInf_div' for the general case, and ENNReal.iInf_div for another special case that assumes Nonempty ι but does not require a ≠ ∞.

theorem ENNReal.iInf_div {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι] (hinfty : a = 0 → ⨅ (i : ι), f i = 0 → ∃ (i : ι), f i = 0) : (⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a

See ENNReal.iInf_div' for the general case, and ENNReal.iInf_div_of_ne for another special case that assumes a ≠ ∞ but does not require Nonempty ι.

theorem ENNReal.inv_iInf {ι : Sort u_1} (f : ι → ENNReal) : (⨅ (i : ι), f i)⁻¹ = ⨆ (i : ι), (f i)⁻¹

theorem ENNReal.inv_iSup {ι : Sort u_1} (f : ι → ENNReal) : (⨆ (i : ι), f i)⁻¹ = ⨅ (i : ι), (f i)⁻¹

theorem ENNReal.inv_sInf (s : Set ENNReal) : (sInf s)⁻¹ = ⨆ a ∈ s, a⁻¹

theorem ENNReal.inv_sSup (s : Set ENNReal) : (sSup s)⁻¹ = ⨅ a ∈ s, a⁻¹

theorem ENNReal.le_iInf_mul {ι : Type u_3} (u v : ι → ENNReal) : (⨅ (i : ι), u i) * ⨅ (i : ι), v i ≤ ⨅ (i : ι), u i * v i

theorem ENNReal.iSup_mul_le {ι : Type u_3} {u v : ι → ENNReal} : ⨆ (i : ι), u i * v i ≤ (⨆ (i : ι), u i) * ⨆ (i : ι), v i

theorem ENNReal.add_iSup {ι : Sort u_1} {a : ENNReal} [Nonempty ι] (f : ι → ENNReal) : a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i

theorem ENNReal.iSup_add {ι : Sort u_1} {a : ENNReal} [Nonempty ι] (f : ι → ENNReal) : (⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a

theorem ENNReal.add_biSup' {ι : Sort u_1} {a : ENNReal} {p : ι → Prop} (h : ∃ (i : ι), p i) (f : ι → ENNReal) : a + ⨆ (i : ι), ⨆ (_ : p i), f i = ⨆ (i : ι), ⨆ (_ : p i), a + f i

theorem ENNReal.biSup_add' {ι : Sort u_1} {a : ENNReal} {p : ι → Prop} (h : ∃ (i : ι), p i) (f : ι → ENNReal) : (⨆ (i : ι), ⨆ (_ : p i), f i) + a = ⨆ (i : ι), ⨆ (_ : p i), f i + a

theorem ENNReal.add_biSup {a : ENNReal} {ι : Type u_3} {s : Set ι} (hs : s.Nonempty) (f : ι → ENNReal) : a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i

theorem ENNReal.biSup_add {a : ENNReal} {ι : Type u_3} {s : Set ι} (hs : s.Nonempty) (f : ι → ENNReal) : (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a

theorem ENNReal.add_sSup {s : Set ENNReal} {a : ENNReal} (hs : s.Nonempty) : a + sSup s = ⨆ b ∈ s, a + b

theorem ENNReal.sSup_add {s : Set ENNReal} {a : ENNReal} (hs : s.Nonempty) : sSup s + a = ⨆ b ∈ s, b + a

theorem ENNReal.iSup_add_iSup_le {ι : Sort u_1} {κ : Sort u_2} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι] [Nonempty κ] {g : κ → ENNReal} (h : ∀ (i : ι) (j : κ), f i + g j ≤ a) : iSup f + iSup g ≤ a

theorem ENNReal.biSup_add_biSup_le' {ι : Sort u_1} {κ : Sort u_2} {f : ι → ENNReal} {a : ENNReal} {p : ι → Prop} {q : κ → Prop} (hp : ∃ (i : ι), p i) (hq : ∃ (j : κ), q j) {g : κ → ENNReal} (h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a) : (⨆ (i : ι), ⨆ (_ : p i), f i) + ⨆ (j : κ), ⨆ (_ : q j), g j ≤ a

theorem ENNReal.biSup_add_biSup_le {ι : Type u_3} {κ : Type u_4} {s : Set ι} {t : Set κ} (hs : s.Nonempty) (ht : t.Nonempty) {f : ι → ENNReal} {g : κ → ENNReal} {a : ENNReal} (h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a) : (⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a

theorem ENNReal.iSup_add_iSup {ι : Sort u_1} {f g : ι → ENNReal} (h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k) : iSup f + iSup g = ⨆ (i : ι), f i + g i

theorem ENNReal.iSup_add_iSup_of_monotone {ι : Type u_3} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {f g : ι → ENNReal} (hf : Monotone f) (hg : Monotone g) : iSup f + iSup g = ⨆ (a : ι), f a + g a

theorem ENNReal.finsetSum_iSup {α : Type u_3} {ι : Type u_4} {s : Finset α} {f : α → ι → ENNReal} (hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k) : ∑ a ∈ s, ⨆ (i : ι), f a i = ⨆ (i : ι), ∑ a ∈ s, f a i

theorem ENNReal.finsetSum_iSup_of_monotone {α : Type u_3} {ι : Type u_4} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {s : Finset α} {f : α → ι → ENNReal} (hf : ∀ (a : α), Monotone (f a)) : ∑ a ∈ s, iSup (f a) = ⨆ (n : ι), ∑ a ∈ s, f a n

@[deprecated ENNReal.finsetSum_iSup_of_monotone]

theorem ENNReal.finset_sum_iSup_nat {α : Type u_3} {ι : Type u_4} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {s : Finset α} {f : α → ι → ENNReal} (hf : ∀ (a : α), Monotone (f a)) : ∑ a ∈ s, iSup (f a) = ⨆ (n : ι), ∑ a ∈ s, f a n

Alias of ENNReal.finsetSum_iSup_of_monotone.

theorem ENNReal.le_iInf_mul_iInf {ι : Sort u_1} {κ : Sort u_2} {f : ι → ENNReal} {a : ENNReal} {g : κ → ENNReal} (hf : ∃ (i : ι), f i ≠ ⊤) (hg : ∃ (j : κ), g j ≠ ⊤) (ha : ∀ (i : ι) (j : κ), a ≤ f i * g j) : a ≤ (⨅ (i : ι), f i) * ⨅ (j : κ), g j

theorem ENNReal.iInf_mul_iInf {ι : Sort u_1} {f g : ι → ENNReal} (hf : ∃ (i : ι), f i ≠ ⊤) (hg : ∃ (j : ι), g j ≠ ⊤) (h : ∀ (i j : ι), ∃ (k : ι), f k * g k ≤ f i * g j) : (⨅ (i : ι), f i) * ⨅ (i : ι), g i = ⨅ (i : ι), f i * g i

theorem ENNReal.smul_iSup {ι : Sort u_1} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (f : ι → ENNReal) (c : R) : c • ⨆ (i : ι), f i = ⨆ (i : ι), c • f i

theorem ENNReal.smul_sSup {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (s : Set ENNReal) (c : R) : c • sSup s = ⨆ a ∈ s, c • a

theorem ENNReal.sub_iSup {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι] (ha : a ≠ ⊤) : a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

theorem ENNReal.exists_lt_add_of_lt_add {x y z : ENNReal} (h : x < y + z) (hy : y ≠ 0) (hz : z ≠ 0) : ∃ y' < y, ∃ z' < z, x < y' + z'