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:

theorem ENNReal.div_eq_inv_mul {a : ENNReal} {b : ENNReal} :
a / b = b⁻¹ * a
@[simp]
@[simp]
theorem ENNReal.coe_inv_le {r : NNReal} :
r⁻¹ (r)⁻¹
@[simp]
theorem ENNReal.coe_inv {r : NNReal} (hr : r 0) :
r⁻¹ = (r)⁻¹
@[simp]
theorem ENNReal.coe_div {r : NNReal} {p : NNReal} (hr : r 0) :
(p / r) = p / r
theorem ENNReal.coe_div_le {r : NNReal} {p : NNReal} :
(p / r) p / r
theorem ENNReal.div_zero {a : ENNReal} (h : a 0) :
a / 0 =
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
@[simp]
theorem ENNReal.inv_eq_one {a : ENNReal} :
a⁻¹ = 1 a = 1
@[simp]
theorem ENNReal.inv_eq_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.div_pos {a : ENNReal} {b : ENNReal} (ha : a 0) (hb : b ) :
0 < a / b
theorem ENNReal.inv_mul_le_iff {x : ENNReal} {y : ENNReal} {z : ENNReal} (h1 : x 0) (h2 : x ) :
x⁻¹ * y z y x * z
theorem ENNReal.mul_inv_le_iff {x : ENNReal} {y : ENNReal} {z : ENNReal} (h1 : y 0) (h2 : y ) :
x * y⁻¹ z x z * y
theorem ENNReal.div_le_iff {x : ENNReal} {y : ENNReal} {z : ENNReal} (h1 : y 0) (h2 : y ) :
x / y z x z * y
theorem ENNReal.div_le_iff' {x : ENNReal} {y : ENNReal} {z : ENNReal} (h1 : y 0) (h2 : y ) :
x / y z x y * z
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 < bb < ac 0) :
(a - b) / c = a / c - b / c
@[simp]
theorem ENNReal.inv_pos {a : ENNReal} :
@[simp]
theorem ENNReal.inv_lt_inv {a : ENNReal} {b : ENNReal} :
a⁻¹ < b⁻¹ b < a
@[simp]
theorem ENNReal.inv_le_inv {a : ENNReal} {b : ENNReal} :
theorem ENNReal.inv_le_inv' {a : ENNReal} {b : ENNReal} (h : a b) :
theorem ENNReal.inv_lt_inv' {a : ENNReal} {b : ENNReal} (h : a < b) :
@[simp]
theorem ENNReal.inv_le_one {a : ENNReal} :
a⁻¹ 1 1 a
@[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)⁻¹

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

Equations
Instances For
    @[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
    @[simp]
    theorem ENNReal.top_div_coe {p : NNReal} :
    / p =
    @[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.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) :
    a = b⁻¹
    theorem ENNReal.mul_le_iff_le_inv {a : ENNReal} {b : ENNReal} {r : ENNReal} (hr₀ : r 0) (hr₁ : r ) :
    r * a b a r⁻¹ * b
    theorem ENNReal.le_of_forall_nnreal_lt {x : ENNReal} {y : ENNReal} (h : ∀ (r : NNReal), r < xr y) :
    x y
    theorem ENNReal.le_of_forall_pos_nnreal_lt {x : ENNReal} {y : ENNReal} (h : ∀ (r : NNReal), 0 < rr < xr y) :
    x y
    theorem ENNReal.eq_top_of_forall_nnreal_le {x : ENNReal} (h : ∀ (r : NNReal), r x) :
    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
    @[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.half_lt_self {a : ENNReal} (hz : a 0) (ht : a ) :
    a / 2 < a
    theorem ENNReal.sub_half {a : ENNReal} (h : a ) :
    a - a / 2 = a / 2
    @[simp]
    theorem ENNReal.orderIsoIicOneBirational_apply_coe (x : ENNReal) :
    (ENNReal.orderIsoIicOneBirational x) = (x⁻¹ + 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.orderIsoIicCoe_apply_coe (a : NNReal) :
      ∀ (a_1 : (Set.Iic a)), ((ENNReal.orderIsoIicCoe a) a_1) = (a_1).toNNReal
      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)) :
        ((ENNReal.orderIsoIicCoe a).symm b) = b

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

        Equations
        Instances For
          @[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 : 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