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.

Instances For
    @[simp]
    theorem NNReal.rpow_eq_pow (x : NNReal) (y : ) :
    NNReal.rpow x 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
    @[simp]
    theorem NNReal.zero_rpow {x : } (h : x 0) :
    0 ^ x = 0
    @[simp]
    theorem NNReal.rpow_one (x : NNReal) :
    x ^ 1 = x
    @[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' (x : NNReal) {y : } {z : } (h : y + z 0) :
    x ^ (y + z) = x ^ y * x ^ z
    theorem NNReal.rpow_mul (x : NNReal) (y : ) (z : ) :
    x ^ (y * z) = (x ^ y) ^ z
    theorem NNReal.rpow_neg (x : NNReal) (y : ) :
    x ^ (-y) = (x ^ y)⁻¹
    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' (x : NNReal) {y : } {z : } (h : y - z 0) :
    x ^ (y - z) = x ^ y / x ^ z
    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)
    @[simp]
    theorem NNReal.rpow_nat_cast (x : NNReal) (n : ) :
    x ^ n = x ^ n
    @[simp]
    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
    theorem NNReal.list_prod_map_rpow (l : List NNReal) (r : ) :
    List.prod (List.map (fun x => x ^ r) l) = List.prod l ^ 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.prod (List.map (fun x => f x ^ r) l) = List.prod (List.map f l) ^ r
    theorem NNReal.multiset_prod_map_rpow {ι : Type u_1} (s : Multiset ι) (f : ιNNReal) (r : ) :

    rpow version of Multiset.prod_map_pow for ℝ≥0.

    theorem NNReal.finset_prod_rpow {ι : Type u_1} (s : Finset ι) (f : ιNNReal) (r : ) :
    (Finset.prod s fun i => f i ^ r) = (Finset.prod s fun i => f i) ^ r

    rpow version of Finset.prod_pow for ℝ≥0.

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

    rpow version of List.prod_map_pow for Real.

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

    rpow version of Multiset.prod_map_pow.

    theorem Real.finset_prod_rpow {ι : Type u_1} (s : Finset ι) (f : ι) (hs : ∀ (i : ι), i s0 f i) (r : ) :
    (Finset.prod s fun i => f i ^ r) = (Finset.prod s fun i => 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_one_div_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
    x y ^ (1 / z) x ^ z y
    theorem NNReal.rpow_one_div_le_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
    x ^ (1 / z) y x y ^ z
    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 => 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 => y ^ x
    theorem NNReal.rpow_left_bijective {x : } (hx : x 0) :
    Function.Bijective fun y => y ^ x
    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_one_div_eq_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
    x ^ (1 / z) = y x = y ^ z
    theorem NNReal.pow_nat_rpow_nat_inv (x : NNReal) {n : } (hn : n 0) :
    (x ^ n) ^ (n)⁻¹ = x
    theorem NNReal.rpow_nat_inv_pow_nat (x : NNReal) {n : } (hn : n 0) :
    (x ^ (n)⁻¹) ^ n = x
    theorem Real.toNNReal_rpow_of_nonneg {x : } {y : } (hx : 0 x) :
    theorem NNReal.strictMono_rpow_of_pos {z : } (h : 0 < z) :
    StrictMono fun x => x ^ z
    theorem NNReal.monotone_rpow_of_nonneg {z : } (h : 0 z) :
    Monotone fun x => 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).

    Instances For
      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).

      Instances For
        @[simp]
        theorem ENNReal.rpow_eq_pow (x : ENNReal) (y : ) :
        ENNReal.rpow x 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
        @[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_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_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_mul (x : ENNReal) (y : ) (z : ) :
        x ^ (y * z) = (x ^ y) ^ z
        @[simp]
        theorem ENNReal.rpow_nat_cast (x : ENNReal) (n : ) :
        x ^ n = x ^ n
        @[simp]
        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.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.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 => x ^ z
        theorem ENNReal.monotone_rpow_of_nonneg {z : } (h : 0 z) :
        Monotone fun x => 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).

        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_one_div_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
          x y ^ (1 / z) x ^ z y
          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_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
          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) :
          theorem ENNReal.rpow_left_injective {x : } (hx : x 0) :
          Function.Injective fun y => y ^ x
          theorem ENNReal.rpow_left_surjective {x : } (hx : x 0) :
          Function.Surjective fun y => y ^ x
          theorem ENNReal.rpow_left_bijective {x : } (hx : x 0) :
          Function.Bijective fun y => y ^ x