Documentation

Mathlib.Data.ENNReal.Inv

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 : ENNReal} {b : ENNReal} :

a / b = b⁻¹ * a

@[simp]

theorem ENNReal.inv_zero :

@[simp]

theorem ENNReal.inv_top :

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 : NNReal} {p : NNReal} (hr : r ≠ 0) :

↑(p / r) = ↑p / ↑r

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

a / 0 = ⊤

instance ENNReal.instDivInvOneMonoidENNReal :

DivInvOneMonoid ENNReal

Equations

ENNReal.instDivInvOneMonoidENNReal = let src := inferInstanceAs (DivInvMonoid ENNReal); DivInvOneMonoid.mk ENNReal.instDivInvOneMonoidENNReal.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.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

instance ENNReal.instInvolutiveInvENNReal :

InvolutiveInv ENNReal

Equations

ENNReal.instInvolutiveInvENNReal = InvolutiveInv.mk ENNReal.instInvolutiveInvENNReal.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

@[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.inv_ne_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 < 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 : ENNReal} {b : ENNReal} :

a⁻¹ < b⁻¹ ↔ b < a

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

a⁻¹ < b ↔ b⁻¹ < a

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

a < b⁻¹ ↔ b < a⁻¹

@[simp]

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

a⁻¹ ≤ b⁻¹ ↔ b ≤ a

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

a⁻¹ ≤ b ↔ b⁻¹ ≤ a

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

a ≤ b⁻¹ ↔ b ≤ a⁻¹

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

b⁻¹ ≤ a⁻¹

theorem ENNReal.inv_lt_inv' {a : ENNReal} {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

@[simp]

theorem OrderIso.invENNReal_apply :

∀ (a : ENNReal), OrderIso.invENNReal a = (OrderDual.toDual a)⁻¹

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.inv ENNReal).trans OrderDual.toDual, map_rel_iff' := (_ : ∀ {a b : ENNReal}, b⁻¹ ≤ a⁻¹ ↔ a ≤ b) }

Instances For

@[simp]

theorem OrderIso.invENNReal_symm_apply (a : ENNReal ᵒᵈ) :

(OrderIso.symm OrderIso.invENNReal) 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 ≠ ⊤) :

@[simp]

theorem ENNReal.top_div_coe {p : NNReal} :

⊤ / ↑p = ⊤

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

@[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.div_self_le_one {a : ENNReal} :

a / a ≤ 1

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

theorem ENNReal.mul_le_iff_le_inv {a : ENNReal} {b : ENNReal} {r : ENNReal} (hr₀ : r ≠ 0) (hr₁ : r ≠ ⊤) :

r * a ≤ b ↔ a ≤ r⁻¹ * b

instance ENNReal.instPosSMulStrictMonoNNRealENNRealToSMulInstNNRealCommSemiringToSemiringToOrderedSemiringToOrderedCommSemiringInstCanonicallyOrderedCommSemiringENNRealInstAlgebraNNRealInstNNRealCommSemiringIdToCommSemiringToPreorderToPartialOrderInstNNRealStrictOrderedSemiringToPartialOrderToCompleteSemilatticeInfToCompleteLatticeToCompletelyDistribLatticeInstCompleteLinearOrderENNRealInstNNRealZero :

PosSMulStrictMono NNReal ENNReal

Equations

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

instance ENNReal.instSMulPosMonoNNRealENNRealToSMulInstNNRealCommSemiringToSemiringToOrderedSemiringToOrderedCommSemiringInstCanonicallyOrderedCommSemiringENNRealInstAlgebraNNRealInstNNRealCommSemiringIdToCommSemiringToPreorderToPartialOrderInstNNRealStrictOrderedSemiringToPartialOrderToCompleteSemilatticeInfToCompleteLatticeToCompletelyDistribLatticeInstCompleteLinearOrderENNRealInstENNRealZero :

SMulPosMono NNReal ENNReal

Equations

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

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

x ≤ y

theorem ENNReal.le_of_forall_pos_nnreal_lt {x : ENNReal} {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) :

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

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 : 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.one_half_lt_one :

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⁻¹

@[simp]

theorem ENNReal.orderIsoIicOneBirational_apply_coe (x : ENNReal) :

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

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.

Instances For

@[simp]

theorem ENNReal.orderIsoIicOneBirational_symm_apply (x : ↑(Set.Iic 1)) :

(OrderIso.symm ENNReal.orderIsoIicOneBirational) x = ((↑x)⁻¹ - 1)⁻¹

@[simp]

theorem ENNReal.orderIsoIicCoe_apply_coe (a : NNReal) :

∀ (a_1 : ↑(Set.Iic ↑a)), ↑((ENNReal.orderIsoIicCoe a) a_1) = ENNReal.toNNReal ↑a_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.

Instances For

@[simp]

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

↑((OrderIso.symm (ENNReal.orderIsoIicCoe a)) 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 = OrderIso.trans ENNReal.orderIsoIicOneBirational (OrderIso.trans (ENNReal.orderIsoIicCoe 1) (OrderIso.symm (NNReal.orderIsoIccZeroCoe 1)))

Instances For

@[simp]

theorem ENNReal.orderIsoUnitIntervalBirational_apply_coe (x : ENNReal) :

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

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 > 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 > 0, (↑n)⁻¹ * a < b

theorem ENNReal.exists_nnreal_pos_mul_lt {a : ENNReal} {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 : 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 ≠ ⊤) :

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