Documentation

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Power function on ℝ≥0 and ℝ≥0∞ #

We construct the power functions x ^ y where

We also prove basic properties of these functions.

noncomputable def NNReal.rpow (x : NNReal) (y : ) :

The nonnegative real power function x^y, defined for x : ℝ≥0 and y : ℝ as the restriction of the real power function. For x > 0, it is equal to exp (y log x). For x = 0, one sets 0 ^ 0 = 1 and 0 ^ y = 0 for y ≠ 0.

Equations
  • x.rpow y = x ^ y,
Instances For
    noncomputable instance NNReal.instPowReal :
    Equations
    @[simp]
    theorem NNReal.rpow_eq_pow (x : NNReal) (y : ) :
    x.rpow y = x ^ y
    @[simp]
    theorem NNReal.coe_rpow (x : NNReal) (y : ) :
    (x ^ y) = x ^ y
    @[simp]
    theorem NNReal.rpow_zero (x : NNReal) :
    x ^ 0 = 1
    @[simp]
    theorem NNReal.rpow_eq_zero_iff {x : NNReal} {y : } :
    x ^ y = 0 x = 0 y 0
    theorem NNReal.rpow_eq_zero {x : NNReal} {y : } (hy : y 0) :
    x ^ y = 0 x = 0
    @[simp]
    theorem NNReal.zero_rpow {x : } (h : x 0) :
    0 ^ x = 0
    @[simp]
    theorem NNReal.rpow_one (x : NNReal) :
    x ^ 1 = x
    theorem NNReal.rpow_neg (x : NNReal) (y : ) :
    x ^ (-y) = (x ^ y)⁻¹
    @[simp]
    theorem NNReal.rpow_natCast (x : NNReal) (n : ) :
    x ^ n = x ^ n
    @[simp]
    theorem NNReal.rpow_intCast (x : NNReal) (n : ) :
    x ^ n = x ^ n
    @[simp]
    theorem NNReal.one_rpow (x : ) :
    1 ^ x = 1
    theorem NNReal.rpow_add {x : NNReal} (hx : x 0) (y : ) (z : ) :
    x ^ (y + z) = x ^ y * x ^ z
    theorem NNReal.rpow_add' {y : } {z : } (h : y + z 0) (x : NNReal) :
    x ^ (y + z) = x ^ y * x ^ z
    theorem NNReal.rpow_add_intCast {x : NNReal} (hx : x 0) (y : ) (n : ) :
    x ^ (y + n) = x ^ y * x ^ n
    theorem NNReal.rpow_add_natCast {x : NNReal} (hx : x 0) (y : ) (n : ) :
    x ^ (y + n) = x ^ y * x ^ n
    theorem NNReal.rpow_sub_intCast {x : NNReal} (hx : x 0) (y : ) (n : ) :
    x ^ (y - n) = x ^ y / x ^ n
    theorem NNReal.rpow_sub_natCast {x : NNReal} (hx : x 0) (y : ) (n : ) :
    x ^ (y - n) = x ^ y / x ^ n
    theorem NNReal.rpow_add_intCast' {y : } {n : } (h : y + n 0) (x : NNReal) :
    x ^ (y + n) = x ^ y * x ^ n
    theorem NNReal.rpow_add_natCast' {y : } {n : } (h : y + n 0) (x : NNReal) :
    x ^ (y + n) = x ^ y * x ^ n
    theorem NNReal.rpow_sub_intCast' {y : } {n : } (h : y - n 0) (x : NNReal) :
    x ^ (y - n) = x ^ y / x ^ n
    theorem NNReal.rpow_sub_natCast' {y : } {n : } (h : y - n 0) (x : NNReal) :
    x ^ (y - n) = x ^ y / x ^ n
    theorem NNReal.rpow_add_one {x : NNReal} (hx : x 0) (y : ) :
    x ^ (y + 1) = x ^ y * x
    theorem NNReal.rpow_sub_one {x : NNReal} (hx : x 0) (y : ) :
    x ^ (y - 1) = x ^ y / x
    theorem NNReal.rpow_add_one' {y : } (h : y + 1 0) (x : NNReal) :
    x ^ (y + 1) = x ^ y * x
    theorem NNReal.rpow_one_add' {y : } (h : 1 + y 0) (x : NNReal) :
    x ^ (1 + y) = x * x ^ y
    theorem NNReal.rpow_add_of_nonneg (x : NNReal) {y : } {z : } (hy : 0 y) (hz : 0 z) :
    x ^ (y + z) = x ^ y * x ^ z
    theorem NNReal.rpow_of_add_eq {w : } {y : } {z : } (x : NNReal) (hw : w 0) (h : y + z = w) :
    x ^ w = x ^ y * x ^ z

    Variant of NNReal.rpow_add' that avoids having to prove y + z = w twice.

    theorem NNReal.rpow_mul (x : NNReal) (y : ) (z : ) :
    x ^ (y * z) = (x ^ y) ^ z
    theorem NNReal.rpow_natCast_mul (x : NNReal) (n : ) (z : ) :
    x ^ (n * z) = (x ^ n) ^ z
    theorem NNReal.rpow_mul_natCast (x : NNReal) (y : ) (n : ) :
    x ^ (y * n) = (x ^ y) ^ n
    theorem NNReal.rpow_intCast_mul (x : NNReal) (n : ) (z : ) :
    x ^ (n * z) = (x ^ n) ^ z
    theorem NNReal.rpow_mul_intCast (x : NNReal) (y : ) (n : ) :
    x ^ (y * n) = (x ^ y) ^ n
    theorem NNReal.rpow_neg_one (x : NNReal) :
    x ^ (-1) = x⁻¹
    theorem NNReal.rpow_sub {x : NNReal} (hx : x 0) (y : ) (z : ) :
    x ^ (y - z) = x ^ y / x ^ z
    theorem NNReal.rpow_sub' {y : } {z : } (h : y - z 0) (x : NNReal) :
    x ^ (y - z) = x ^ y / x ^ z
    theorem NNReal.rpow_sub_one' {y : } (h : y - 1 0) (x : NNReal) :
    x ^ (y - 1) = x ^ y / x
    theorem NNReal.rpow_one_sub' {y : } (h : 1 - y 0) (x : NNReal) :
    x ^ (1 - y) = x / x ^ y
    theorem NNReal.rpow_inv_rpow_self {y : } (hy : y 0) (x : NNReal) :
    (x ^ y) ^ (1 / y) = x
    theorem NNReal.rpow_self_rpow_inv {y : } (hy : y 0) (x : NNReal) :
    (x ^ (1 / y)) ^ y = x
    theorem NNReal.inv_rpow (x : NNReal) (y : ) :
    x⁻¹ ^ y = (x ^ y)⁻¹
    theorem NNReal.div_rpow (x : NNReal) (y : NNReal) (z : ) :
    (x / y) ^ z = x ^ z / y ^ z
    theorem NNReal.sqrt_eq_rpow (x : NNReal) :
    NNReal.sqrt x = x ^ (1 / 2)
    @[deprecated NNReal.rpow_natCast]
    theorem NNReal.rpow_nat_cast (x : NNReal) (n : ) :
    x ^ n = x ^ n

    Alias of NNReal.rpow_natCast.

    @[simp]
    theorem NNReal.rpow_ofNat (x : NNReal) (n : ) [n.AtLeastTwo] :
    theorem NNReal.rpow_two (x : NNReal) :
    x ^ 2 = x ^ 2
    theorem NNReal.mul_rpow {x : NNReal} {y : NNReal} {z : } :
    (x * y) ^ z = x ^ z * y ^ z
    @[simp]
    theorem NNReal.rpowMonoidHom_apply (r : ) :
    ∀ (x : NNReal), (NNReal.rpowMonoidHom r) x = x ^ r

    rpow as a MonoidHom

    Equations
    Instances For
      theorem NNReal.list_prod_map_rpow (l : List NNReal) (r : ) :
      (List.map (fun (x : NNReal) => x ^ r) l).prod = l.prod ^ r

      rpow variant of List.prod_map_pow for ℝ≥0

      theorem NNReal.list_prod_map_rpow' {ι : Type u_1} (l : List ι) (f : ιNNReal) (r : ) :
      (List.map (fun (x : ι) => f x ^ r) l).prod = (List.map f l).prod ^ r
      theorem NNReal.multiset_prod_map_rpow {ι : Type u_1} (s : Multiset ι) (f : ιNNReal) (r : ) :
      (Multiset.map (fun (x : ι) => f x ^ r) s).prod = (Multiset.map f s).prod ^ r

      rpow version of Multiset.prod_map_pow for ℝ≥0.

      theorem NNReal.finset_prod_rpow {ι : Type u_1} (s : Finset ι) (f : ιNNReal) (r : ) :
      is, f i ^ r = (∏ is, f i) ^ r

      rpow version of Finset.prod_pow for ℝ≥0.

      theorem Real.list_prod_map_rpow (l : List ) (hl : xl, 0 x) (r : ) :
      (List.map (fun (x : ) => x ^ r) l).prod = l.prod ^ r

      rpow version of List.prod_map_pow for Real.

      theorem Real.list_prod_map_rpow' {ι : Type u_1} (l : List ι) (f : ι) (hl : il, 0 f i) (r : ) :
      (List.map (fun (x : ι) => f x ^ r) l).prod = (List.map f l).prod ^ r
      theorem Real.multiset_prod_map_rpow {ι : Type u_1} (s : Multiset ι) (f : ι) (hs : is, 0 f i) (r : ) :
      (Multiset.map (fun (x : ι) => f x ^ r) s).prod = (Multiset.map f s).prod ^ r

      rpow version of Multiset.prod_map_pow.

      theorem Real.finset_prod_rpow {ι : Type u_1} (s : Finset ι) (f : ι) (hs : is, 0 f i) (r : ) :
      is, f i ^ r = (∏ is, f i) ^ r

      rpow version of Finset.prod_pow.

      theorem NNReal.rpow_le_rpow {x : NNReal} {y : NNReal} {z : } (h₁ : x y) (h₂ : 0 z) :
      x ^ z y ^ z
      theorem NNReal.rpow_lt_rpow {x : NNReal} {y : NNReal} {z : } (h₁ : x < y) (h₂ : 0 < z) :
      x ^ z < y ^ z
      theorem NNReal.rpow_lt_rpow_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
      x ^ z < y ^ z x < y
      theorem NNReal.rpow_le_rpow_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
      x ^ z y ^ z x y
      theorem NNReal.le_rpow_inv_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
      x y ^ z⁻¹ x ^ z y
      @[deprecated NNReal.le_rpow_inv_iff]
      theorem NNReal.le_rpow_one_div_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
      x y ^ (1 / z) x ^ z y
      theorem NNReal.rpow_inv_le_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
      x ^ z⁻¹ y x y ^ z
      @[deprecated NNReal.rpow_inv_le_iff]
      theorem NNReal.rpow_one_div_le_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
      x ^ (1 / z) y x y ^ z
      theorem NNReal.lt_rpow_inv_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
      x < y ^ z⁻¹ x ^ z < y
      theorem NNReal.rpow_inv_lt_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
      x ^ z⁻¹ < y x < y ^ z
      theorem NNReal.rpow_lt_rpow_of_neg {x : NNReal} {z : } {y : NNReal} (hx : 0 < x) (hxy : x < y) (hz : z < 0) :
      y ^ z < x ^ z
      theorem NNReal.rpow_le_rpow_of_nonpos {x : NNReal} {z : } {y : NNReal} (hx : 0 < x) (hxy : x y) (hz : z 0) :
      y ^ z x ^ z
      theorem NNReal.rpow_lt_rpow_iff_of_neg {x : NNReal} {z : } {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
      x ^ z < y ^ z y < x
      theorem NNReal.rpow_le_rpow_iff_of_neg {x : NNReal} {z : } {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
      x ^ z y ^ z y x
      theorem NNReal.le_rpow_inv_iff_of_pos {z : } {y : NNReal} (hy : 0 y) (hz : 0 < z) (x : NNReal) :
      x y ^ z⁻¹ x ^ z y
      theorem NNReal.rpow_inv_le_iff_of_pos {z : } {y : NNReal} (hy : 0 y) (hz : 0 < z) (x : NNReal) :
      x ^ z⁻¹ y x y ^ z
      theorem NNReal.lt_rpow_inv_iff_of_pos {z : } {y : NNReal} (hy : 0 y) (hz : 0 < z) (x : NNReal) :
      x < y ^ z⁻¹ x ^ z < y
      theorem NNReal.rpow_inv_lt_iff_of_pos {z : } {y : NNReal} (hy : 0 y) (hz : 0 < z) (x : NNReal) :
      x ^ z⁻¹ < y x < y ^ z
      theorem NNReal.le_rpow_inv_iff_of_neg {x : NNReal} {z : } {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
      x y ^ z⁻¹ y x ^ z
      theorem NNReal.lt_rpow_inv_iff_of_neg {x : NNReal} {z : } {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
      x < y ^ z⁻¹ y < x ^ z
      theorem NNReal.rpow_inv_lt_iff_of_neg {x : NNReal} {z : } {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
      x ^ z⁻¹ < y y ^ z < x
      theorem NNReal.rpow_inv_le_iff_of_neg {x : NNReal} {z : } {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
      x ^ z⁻¹ y y ^ z x
      theorem NNReal.rpow_lt_rpow_of_exponent_lt {x : NNReal} {y : } {z : } (hx : 1 < x) (hyz : y < z) :
      x ^ y < x ^ z
      theorem NNReal.rpow_le_rpow_of_exponent_le {x : NNReal} {y : } {z : } (hx : 1 x) (hyz : y z) :
      x ^ y x ^ z
      theorem NNReal.rpow_lt_rpow_of_exponent_gt {x : NNReal} {y : } {z : } (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
      x ^ y < x ^ z
      theorem NNReal.rpow_le_rpow_of_exponent_ge {x : NNReal} {y : } {z : } (hx0 : 0 < x) (hx1 : x 1) (hyz : z y) :
      x ^ y x ^ z
      theorem NNReal.rpow_pos {p : } {x : NNReal} (hx_pos : 0 < x) :
      0 < x ^ p
      theorem NNReal.rpow_lt_one {x : NNReal} {z : } (hx1 : x < 1) (hz : 0 < z) :
      x ^ z < 1
      theorem NNReal.rpow_le_one {x : NNReal} {z : } (hx2 : x 1) (hz : 0 z) :
      x ^ z 1
      theorem NNReal.rpow_lt_one_of_one_lt_of_neg {x : NNReal} {z : } (hx : 1 < x) (hz : z < 0) :
      x ^ z < 1
      theorem NNReal.rpow_le_one_of_one_le_of_nonpos {x : NNReal} {z : } (hx : 1 x) (hz : z 0) :
      x ^ z 1
      theorem NNReal.one_lt_rpow {x : NNReal} {z : } (hx : 1 < x) (hz : 0 < z) :
      1 < x ^ z
      theorem NNReal.one_le_rpow {x : NNReal} {z : } (h : 1 x) (h₁ : 0 z) :
      1 x ^ z
      theorem NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg {x : NNReal} {z : } (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
      1 < x ^ z
      theorem NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos {x : NNReal} {z : } (hx1 : 0 < x) (hx2 : x 1) (hz : z 0) :
      1 x ^ z
      theorem NNReal.rpow_le_self_of_le_one {x : NNReal} {z : } (hx : x 1) (h_one_le : 1 z) :
      x ^ z x
      theorem NNReal.rpow_left_injective {x : } (hx : x 0) :
      Function.Injective fun (y : NNReal) => y ^ x
      theorem NNReal.rpow_eq_rpow_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
      x ^ z = y ^ z x = y
      theorem NNReal.rpow_left_surjective {x : } (hx : x 0) :
      Function.Surjective fun (y : NNReal) => y ^ x
      theorem NNReal.rpow_left_bijective {x : } (hx : x 0) :
      Function.Bijective fun (y : NNReal) => y ^ x
      theorem NNReal.eq_rpow_inv_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
      x = y ^ z⁻¹ x ^ z = y
      @[deprecated NNReal.eq_rpow_inv_iff]
      theorem NNReal.eq_rpow_one_div_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
      x = y ^ (1 / z) x ^ z = y
      theorem NNReal.rpow_inv_eq_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
      x ^ z⁻¹ = y x = y ^ z
      @[deprecated NNReal.rpow_inv_eq_iff]
      theorem NNReal.rpow_one_div_eq_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
      x ^ (1 / z) = y x = y ^ z
      @[simp]
      theorem NNReal.rpow_rpow_inv {y : } (hy : y 0) (x : NNReal) :
      (x ^ y) ^ y⁻¹ = x
      @[simp]
      theorem NNReal.rpow_inv_rpow {y : } (hy : y 0) (x : NNReal) :
      (x ^ y⁻¹) ^ y = x
      theorem NNReal.pow_rpow_inv_natCast (x : NNReal) {n : } (hn : n 0) :
      (x ^ n) ^ (↑n)⁻¹ = x
      theorem NNReal.rpow_inv_natCast_pow (x : NNReal) {n : } (hn : n 0) :
      (x ^ (↑n)⁻¹) ^ n = x
      theorem Real.toNNReal_rpow_of_nonneg {x : } {y : } (hx : 0 x) :
      (x ^ y).toNNReal = x.toNNReal ^ y
      theorem NNReal.strictMono_rpow_of_pos {z : } (h : 0 < z) :
      StrictMono fun (x : NNReal) => x ^ z
      theorem NNReal.monotone_rpow_of_nonneg {z : } (h : 0 z) :
      Monotone fun (x : NNReal) => x ^ z
      @[simp]
      theorem NNReal.orderIsoRpow_apply (y : ) (hy : 0 < y) (x : NNReal) :
      (NNReal.orderIsoRpow y hy) x = x ^ y
      def NNReal.orderIsoRpow (y : ) (hy : 0 < y) :

      Bundles fun x : ℝ≥0 => x ^ y into an order isomorphism when y : ℝ is positive, where the inverse is fun x : ℝ≥0 => x ^ (1 / y).

      Equations
      Instances For
        theorem NNReal.orderIsoRpow_symm_eq (y : ) (hy : 0 < y) :
        theorem Real.nnnorm_rpow_of_nonneg {x : } {y : } (hx : 0 x) :
        noncomputable def ENNReal.rpow :

        The real power function x^y on extended nonnegative reals, defined for x : ℝ≥0∞ and y : ℝ as the restriction of the real power function if 0 < x < ⊤, and with the natural values for 0 and (i.e., 0 ^ x = 0 for x > 0, 1 for x = 0 and for x < 0, and ⊤ ^ x = 1 / 0 ^ x).

        Equations
        Instances For
          noncomputable instance ENNReal.instPowReal :
          Equations
          @[simp]
          theorem ENNReal.rpow_eq_pow (x : ENNReal) (y : ) :
          x.rpow y = x ^ y
          @[simp]
          theorem ENNReal.rpow_zero {x : ENNReal} :
          x ^ 0 = 1
          theorem ENNReal.top_rpow_def (y : ) :
          ^ y = if 0 < y then else if y = 0 then 1 else 0
          @[simp]
          theorem ENNReal.top_rpow_of_pos {y : } (h : 0 < y) :
          @[simp]
          theorem ENNReal.top_rpow_of_neg {y : } (h : y < 0) :
          ^ y = 0
          @[simp]
          theorem ENNReal.zero_rpow_of_pos {y : } (h : 0 < y) :
          0 ^ y = 0
          @[simp]
          theorem ENNReal.zero_rpow_of_neg {y : } (h : y < 0) :
          0 ^ y =
          theorem ENNReal.zero_rpow_def (y : ) :
          0 ^ y = if 0 < y then 0 else if y = 0 then 1 else
          @[simp]
          theorem ENNReal.zero_rpow_mul_self (y : ) :
          0 ^ y * 0 ^ y = 0 ^ y
          theorem ENNReal.coe_rpow_of_ne_zero {x : NNReal} (h : x 0) (y : ) :
          (x ^ y) = x ^ y
          theorem ENNReal.coe_rpow_of_nonneg (x : NNReal) {y : } (h : 0 y) :
          (x ^ y) = x ^ y
          theorem ENNReal.coe_rpow_def (x : NNReal) (y : ) :
          x ^ y = if x = 0 y < 0 then else (x ^ y)
          @[simp]
          theorem ENNReal.rpow_one (x : ENNReal) :
          x ^ 1 = x
          @[simp]
          theorem ENNReal.one_rpow (x : ) :
          1 ^ x = 1
          @[simp]
          theorem ENNReal.rpow_eq_zero_iff {x : ENNReal} {y : } :
          x ^ y = 0 x = 0 0 < y x = y < 0
          theorem ENNReal.rpow_eq_zero_iff_of_pos {x : ENNReal} {y : } (hy : 0 < y) :
          x ^ y = 0 x = 0
          @[simp]
          theorem ENNReal.rpow_eq_top_iff {x : ENNReal} {y : } :
          x ^ y = x = 0 y < 0 x = 0 < y
          theorem ENNReal.rpow_eq_top_iff_of_pos {x : ENNReal} {y : } (hy : 0 < y) :
          x ^ y = x =
          theorem ENNReal.rpow_lt_top_iff_of_pos {x : ENNReal} {y : } (hy : 0 < y) :
          x ^ y < x <
          theorem ENNReal.rpow_eq_top_of_nonneg (x : ENNReal) {y : } (hy0 : 0 y) :
          x ^ y = x =
          theorem ENNReal.rpow_ne_top_of_nonneg {x : ENNReal} {y : } (hy0 : 0 y) (h : x ) :
          x ^ y
          theorem ENNReal.rpow_lt_top_of_nonneg {x : ENNReal} {y : } (hy0 : 0 y) (h : x ) :
          x ^ y <
          theorem ENNReal.rpow_add {x : ENNReal} (y : ) (z : ) (hx : x 0) (h'x : x ) :
          x ^ (y + z) = x ^ y * x ^ z
          theorem ENNReal.rpow_add_of_nonneg {x : ENNReal} (y : ) (z : ) (hy : 0 y) (hz : 0 z) :
          x ^ (y + z) = x ^ y * x ^ z
          theorem ENNReal.rpow_neg (x : ENNReal) (y : ) :
          x ^ (-y) = (x ^ y)⁻¹
          theorem ENNReal.rpow_sub {x : ENNReal} (y : ) (z : ) (hx : x 0) (h'x : x ) :
          x ^ (y - z) = x ^ y / x ^ z
          theorem ENNReal.rpow_neg_one (x : ENNReal) :
          x ^ (-1) = x⁻¹
          theorem ENNReal.rpow_mul (x : ENNReal) (y : ) (z : ) :
          x ^ (y * z) = (x ^ y) ^ z
          @[simp]
          theorem ENNReal.rpow_natCast (x : ENNReal) (n : ) :
          x ^ n = x ^ n
          @[deprecated ENNReal.rpow_natCast]
          theorem ENNReal.rpow_nat_cast (x : ENNReal) (n : ) :
          x ^ n = x ^ n

          Alias of ENNReal.rpow_natCast.

          @[simp]
          theorem ENNReal.rpow_ofNat (x : ENNReal) (n : ) [n.AtLeastTwo] :
          @[simp]
          theorem ENNReal.rpow_intCast (x : ENNReal) (n : ) :
          x ^ n = x ^ n
          @[deprecated ENNReal.rpow_intCast]
          theorem ENNReal.rpow_int_cast (x : ENNReal) (n : ) :
          x ^ n = x ^ n

          Alias of ENNReal.rpow_intCast.

          theorem ENNReal.rpow_two (x : ENNReal) :
          x ^ 2 = x ^ 2
          theorem ENNReal.mul_rpow_eq_ite (x : ENNReal) (y : ENNReal) (z : ) :
          (x * y) ^ z = if (x = 0 y = x = y = 0) z < 0 then else x ^ z * y ^ z
          theorem ENNReal.mul_rpow_of_ne_top {x : ENNReal} {y : ENNReal} (hx : x ) (hy : y ) (z : ) :
          (x * y) ^ z = x ^ z * y ^ z
          theorem ENNReal.coe_mul_rpow (x : NNReal) (y : NNReal) (z : ) :
          (x * y) ^ z = x ^ z * y ^ z
          theorem ENNReal.prod_coe_rpow {ι : Type u_1} (s : Finset ι) (f : ιNNReal) (r : ) :
          is, (f i) ^ r = (∏ is, f i) ^ r
          theorem ENNReal.mul_rpow_of_ne_zero {x : ENNReal} {y : ENNReal} (hx : x 0) (hy : y 0) (z : ) :
          (x * y) ^ z = x ^ z * y ^ z
          theorem ENNReal.mul_rpow_of_nonneg (x : ENNReal) (y : ENNReal) {z : } (hz : 0 z) :
          (x * y) ^ z = x ^ z * y ^ z
          theorem ENNReal.prod_rpow_of_ne_top {ι : Type u_1} {s : Finset ι} {f : ιENNReal} (hf : is, f i ) (r : ) :
          is, f i ^ r = (∏ is, f i) ^ r
          theorem ENNReal.prod_rpow_of_nonneg {ι : Type u_1} {s : Finset ι} {f : ιENNReal} {r : } (hr : 0 r) :
          is, f i ^ r = (∏ is, f i) ^ r
          theorem ENNReal.inv_rpow (x : ENNReal) (y : ) :
          x⁻¹ ^ y = (x ^ y)⁻¹
          theorem ENNReal.div_rpow_of_nonneg (x : ENNReal) (y : ENNReal) {z : } (hz : 0 z) :
          (x / y) ^ z = x ^ z / y ^ z
          theorem ENNReal.strictMono_rpow_of_pos {z : } (h : 0 < z) :
          StrictMono fun (x : ENNReal) => x ^ z
          theorem ENNReal.monotone_rpow_of_nonneg {z : } (h : 0 z) :
          Monotone fun (x : ENNReal) => x ^ z
          @[simp]
          theorem ENNReal.orderIsoRpow_apply (y : ) (hy : 0 < y) (x : ENNReal) :
          (ENNReal.orderIsoRpow y hy) x = x ^ y

          Bundles fun x : ℝ≥0∞ => x ^ y into an order isomorphism when y : ℝ is positive, where the inverse is fun x : ℝ≥0∞ => x ^ (1 / y).

          Equations
          Instances For
            theorem ENNReal.rpow_le_rpow {x : ENNReal} {y : ENNReal} {z : } (h₁ : x y) (h₂ : 0 z) :
            x ^ z y ^ z
            theorem ENNReal.rpow_lt_rpow {x : ENNReal} {y : ENNReal} {z : } (h₁ : x < y) (h₂ : 0 < z) :
            x ^ z < y ^ z
            theorem ENNReal.rpow_le_rpow_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
            x ^ z y ^ z x y
            theorem ENNReal.rpow_lt_rpow_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
            x ^ z < y ^ z x < y
            theorem ENNReal.le_rpow_inv_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
            x y ^ z⁻¹ x ^ z y
            @[deprecated ENNReal.le_rpow_inv_iff]
            theorem ENNReal.le_rpow_one_div_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
            x y ^ (1 / z) x ^ z y
            theorem ENNReal.rpow_inv_lt_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
            x ^ z⁻¹ < y x < y ^ z
            theorem ENNReal.lt_rpow_inv_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
            x < y ^ z⁻¹ x ^ z < y
            @[deprecated ENNReal.lt_rpow_inv_iff]
            theorem ENNReal.lt_rpow_one_div_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
            x < y ^ (1 / z) x ^ z < y
            theorem ENNReal.rpow_inv_le_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
            x ^ z⁻¹ y x y ^ z
            @[deprecated ENNReal.rpow_inv_le_iff]
            theorem ENNReal.rpow_one_div_le_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
            x ^ (1 / z) y x y ^ z
            theorem ENNReal.rpow_lt_rpow_of_exponent_lt {x : ENNReal} {y : } {z : } (hx : 1 < x) (hx' : x ) (hyz : y < z) :
            x ^ y < x ^ z
            theorem ENNReal.rpow_le_rpow_of_exponent_le {x : ENNReal} {y : } {z : } (hx : 1 x) (hyz : y z) :
            x ^ y x ^ z
            theorem ENNReal.rpow_lt_rpow_of_exponent_gt {x : ENNReal} {y : } {z : } (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
            x ^ y < x ^ z
            theorem ENNReal.rpow_le_rpow_of_exponent_ge {x : ENNReal} {y : } {z : } (hx1 : x 1) (hyz : z y) :
            x ^ y x ^ z
            theorem ENNReal.rpow_le_self_of_le_one {x : ENNReal} {z : } (hx : x 1) (h_one_le : 1 z) :
            x ^ z x
            theorem ENNReal.le_rpow_self_of_one_le {x : ENNReal} {z : } (hx : 1 x) (h_one_le : 1 z) :
            x x ^ z
            theorem ENNReal.rpow_pos_of_nonneg {p : } {x : ENNReal} (hx_pos : 0 < x) (hp_nonneg : 0 p) :
            0 < x ^ p
            theorem ENNReal.rpow_pos {p : } {x : ENNReal} (hx_pos : 0 < x) (hx_ne_top : x ) :
            0 < x ^ p
            theorem ENNReal.rpow_lt_one {x : ENNReal} {z : } (hx : x < 1) (hz : 0 < z) :
            x ^ z < 1
            theorem ENNReal.rpow_le_one {x : ENNReal} {z : } (hx : x 1) (hz : 0 z) :
            x ^ z 1
            theorem ENNReal.rpow_lt_one_of_one_lt_of_neg {x : ENNReal} {z : } (hx : 1 < x) (hz : z < 0) :
            x ^ z < 1
            theorem ENNReal.rpow_le_one_of_one_le_of_neg {x : ENNReal} {z : } (hx : 1 x) (hz : z < 0) :
            x ^ z 1
            theorem ENNReal.one_lt_rpow {x : ENNReal} {z : } (hx : 1 < x) (hz : 0 < z) :
            1 < x ^ z
            theorem ENNReal.one_le_rpow {x : ENNReal} {z : } (hx : 1 x) (hz : 0 < z) :
            1 x ^ z
            theorem ENNReal.one_lt_rpow_of_pos_of_lt_one_of_neg {x : ENNReal} {z : } (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
            1 < x ^ z
            theorem ENNReal.one_le_rpow_of_pos_of_le_one_of_neg {x : ENNReal} {z : } (hx1 : 0 < x) (hx2 : x 1) (hz : z < 0) :
            1 x ^ z
            @[simp]
            theorem ENNReal.toNNReal_rpow (x : ENNReal) (z : ) :
            (x ^ z).toNNReal = x.toNNReal ^ z
            theorem ENNReal.toReal_rpow (x : ENNReal) (z : ) :
            x.toReal ^ z = (x ^ z).toReal
            theorem ENNReal.ofReal_rpow_of_pos {x : } {p : } (hx_pos : 0 < x) :
            theorem ENNReal.ofReal_rpow_of_nonneg {x : } {p : } (hx_nonneg : 0 x) (hp_nonneg : 0 p) :
            @[simp]
            theorem ENNReal.rpow_rpow_inv {y : } (hy : y 0) (x : ENNReal) :
            (x ^ y) ^ y⁻¹ = x
            @[simp]
            theorem ENNReal.rpow_inv_rpow {y : } (hy : y 0) (x : ENNReal) :
            (x ^ y⁻¹) ^ y = x
            theorem ENNReal.pow_rpow_inv_natCast {n : } (hn : n 0) (x : ENNReal) :
            (x ^ n) ^ (↑n)⁻¹ = x
            theorem ENNReal.rpow_inv_natCast_pow {n : } (hn : n 0) (x : ENNReal) :
            (x ^ (↑n)⁻¹) ^ n = x
            theorem ENNReal.rpow_natCast_mul (x : ENNReal) (n : ) (z : ) :
            x ^ (n * z) = (x ^ n) ^ z
            theorem ENNReal.rpow_mul_natCast (x : ENNReal) (y : ) (n : ) :
            x ^ (y * n) = (x ^ y) ^ n
            theorem ENNReal.rpow_intCast_mul (x : ENNReal) (n : ) (z : ) :
            x ^ (n * z) = (x ^ n) ^ z
            theorem ENNReal.rpow_mul_intCast (x : ENNReal) (y : ) (n : ) :
            x ^ (y * n) = (x ^ y) ^ n
            theorem ENNReal.rpow_left_injective {x : } (hx : x 0) :
            Function.Injective fun (y : ENNReal) => y ^ x
            theorem ENNReal.rpow_left_surjective {x : } (hx : x 0) :
            Function.Surjective fun (y : ENNReal) => y ^ x
            theorem ENNReal.rpow_left_bijective {x : } (hx : x 0) :
            Function.Bijective fun (y : ENNReal) => y ^ x