Documentation

Mathlib.Analysis.SpecialFunctions.Pow.Real

Power function on #

We construct the power functions x ^ y, where x and y are real numbers.

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

The real power function x ^ y, defined as the real part of the complex 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. For x < 0, the definition is somewhat arbitrary as it depends on the choice of a complex determination of the logarithm. With our conventions, it is equal to exp (y log x) cos (π y).

Equations
  • x.rpow y = (x ^ y).re
Instances For
    noncomputable instance Real.instPow :
    Equations
    @[simp]
    theorem Real.rpow_eq_pow (x : ) (y : ) :
    x.rpow y = x ^ y
    theorem Real.rpow_def (x : ) (y : ) :
    x ^ y = (x ^ y).re
    theorem Real.rpow_def_of_nonneg {x : } (hx : 0 x) (y : ) :
    x ^ y = if x = 0 then if y = 0 then 1 else 0 else Real.exp (Real.log x * y)
    theorem Real.rpow_def_of_pos {x : } (hx : 0 < x) (y : ) :
    x ^ y = Real.exp (Real.log x * y)
    theorem Real.exp_mul (x : ) (y : ) :
    Real.exp (x * y) = Real.exp x ^ y
    @[simp]
    theorem Real.rpow_intCast (x : ) (n : ) :
    x ^ n = x ^ n
    @[deprecated Real.rpow_intCast]
    theorem Real.rpow_int_cast (x : ) (n : ) :
    x ^ n = x ^ n

    Alias of Real.rpow_intCast.

    @[simp]
    theorem Real.rpow_natCast (x : ) (n : ) :
    x ^ n = x ^ n
    @[deprecated Real.rpow_natCast]
    theorem Real.rpow_nat_cast (x : ) (n : ) :
    x ^ n = x ^ n

    Alias of Real.rpow_natCast.

    @[simp]
    theorem Real.exp_one_rpow (x : ) :
    @[simp]
    theorem Real.exp_one_pow (n : ) :
    Real.exp 1 ^ n = Real.exp n
    theorem Real.rpow_eq_zero_iff_of_nonneg {x : } {y : } (hx : 0 x) :
    x ^ y = 0 x = 0 y 0
    @[simp]
    theorem Real.rpow_eq_zero {x : } {y : } (hx : 0 x) (hy : y 0) :
    x ^ y = 0 x = 0
    @[simp]
    theorem Real.rpow_ne_zero {x : } {y : } (hx : 0 x) (hy : y 0) :
    x ^ y 0 x 0
    theorem Real.rpow_def_of_neg {x : } (hx : x < 0) (y : ) :
    theorem Real.rpow_def_of_nonpos {x : } (hx : x 0) (y : ) :
    x ^ y = if x = 0 then if y = 0 then 1 else 0 else Real.exp (Real.log x * y) * Real.cos (y * Real.pi)
    theorem Real.rpow_pos_of_pos {x : } (hx : 0 < x) (y : ) :
    0 < x ^ y
    @[simp]
    theorem Real.rpow_zero (x : ) :
    x ^ 0 = 1
    theorem Real.rpow_zero_pos (x : ) :
    0 < x ^ 0
    @[simp]
    theorem Real.zero_rpow {x : } (h : x 0) :
    0 ^ x = 0
    theorem Real.zero_rpow_eq_iff {x : } {a : } :
    0 ^ x = a x 0 a = 0 x = 0 a = 1
    theorem Real.eq_zero_rpow_iff {x : } {a : } :
    a = 0 ^ x x 0 a = 0 x = 0 a = 1
    @[simp]
    theorem Real.rpow_one (x : ) :
    x ^ 1 = x
    @[simp]
    theorem Real.one_rpow (x : ) :
    1 ^ x = 1
    theorem Real.zero_rpow_le_one (x : ) :
    0 ^ x 1
    theorem Real.zero_rpow_nonneg (x : ) :
    0 0 ^ x
    theorem Real.rpow_nonneg {x : } (hx : 0 x) (y : ) :
    0 x ^ y
    theorem Real.abs_rpow_of_nonneg {x : } {y : } (hx_nonneg : 0 x) :
    |x ^ y| = |x| ^ y
    theorem Real.abs_rpow_le_abs_rpow (x : ) (y : ) :
    |x ^ y| |x| ^ y
    theorem Real.rpow_inv_log {x : } (hx₀ : 0 < x) (hx₁ : x 1) :

    See Real.rpow_inv_log for the equality when x ≠ 1 is strictly positive.

    theorem Real.norm_rpow_of_nonneg {x : } {y : } (hx_nonneg : 0 x) :
    x ^ y = x ^ y
    theorem Real.rpow_add {x : } (hx : 0 < x) (y : ) (z : ) :
    x ^ (y + z) = x ^ y * x ^ z
    theorem Real.rpow_add' {x : } {y : } {z : } (hx : 0 x) (h : y + z 0) :
    x ^ (y + z) = x ^ y * x ^ z
    theorem Real.rpow_of_add_eq {w : } {x : } {y : } {z : } (hx : 0 x) (hw : w 0) (h : y + z = w) :
    x ^ w = x ^ y * x ^ z

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

    theorem Real.rpow_add_of_nonneg {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 z) :
    x ^ (y + z) = x ^ y * x ^ z
    theorem Real.le_rpow_add {x : } (hx : 0 x) (y : ) (z : ) :
    x ^ y * x ^ z x ^ (y + z)

    For 0 ≤ x, the only problematic case in the equality x ^ y * x ^ z = x ^ (y + z) is for x = 0 and y + z = 0, where the right hand side is 1 while the left hand side can vanish. The inequality is always true, though, and given in this lemma.

    theorem Real.rpow_sum_of_pos {ι : Type u_1} {a : } (ha : 0 < a) (f : ι) (s : Finset ι) :
    a ^ xs, f x = xs, a ^ f x
    theorem Real.rpow_sum_of_nonneg {ι : Type u_1} {a : } (ha : 0 a) {s : Finset ι} {f : ι} (h : xs, 0 f x) :
    a ^ xs, f x = xs, a ^ f x
    theorem Real.rpow_neg {x : } (hx : 0 x) (y : ) :
    x ^ (-y) = (x ^ y)⁻¹
    theorem Real.rpow_sub {x : } (hx : 0 < x) (y : ) (z : ) :
    x ^ (y - z) = x ^ y / x ^ z
    theorem Real.rpow_sub' {x : } (hx : 0 x) {y : } {z : } (h : y - z 0) :
    x ^ (y - z) = x ^ y / x ^ z
    theorem HasCompactSupport.rpow_const {α : Type u_1} [TopologicalSpace α] {f : α} (hf : HasCompactSupport f) {r : } (hr : r 0) :
    HasCompactSupport fun (x : α) => f x ^ r

    Comparing real and complex powers #

    theorem Complex.ofReal_cpow {x : } (hx : 0 x) (y : ) :
    (x ^ y) = x ^ y
    theorem Complex.ofReal_cpow_of_nonpos {x : } (hx : x 0) (y : ) :
    x ^ y = (-x) ^ y * Complex.exp (Real.pi * Complex.I * y)
    theorem Complex.cpow_ofReal (x : ) (y : ) :
    x ^ y = (Complex.abs x ^ y) * ((Real.cos (x.arg * y)) + (Real.sin (x.arg * y)) * Complex.I)
    theorem Complex.cpow_ofReal_re (x : ) (y : ) :
    (x ^ y).re = Complex.abs x ^ y * Real.cos (x.arg * y)
    theorem Complex.cpow_ofReal_im (x : ) (y : ) :
    (x ^ y).im = Complex.abs x ^ y * Real.sin (x.arg * y)
    theorem Complex.abs_cpow_of_ne_zero {z : } (hz : z 0) (w : ) :
    Complex.abs (z ^ w) = Complex.abs z ^ w.re / Real.exp (z.arg * w.im)
    theorem Complex.abs_cpow_of_imp {z : } {w : } (h : z = 0w.re = 0w = 0) :
    Complex.abs (z ^ w) = Complex.abs z ^ w.re / Real.exp (z.arg * w.im)
    theorem Complex.abs_cpow_le (z : ) (w : ) :
    Complex.abs (z ^ w) Complex.abs z ^ w.re / Real.exp (z.arg * w.im)
    @[simp]
    theorem Complex.abs_cpow_real (x : ) (y : ) :
    Complex.abs (x ^ y) = Complex.abs x ^ y
    @[simp]
    theorem Complex.abs_cpow_inv_nat (x : ) (n : ) :
    Complex.abs (x ^ (↑n)⁻¹) = Complex.abs x ^ (↑n)⁻¹
    theorem Complex.abs_cpow_eq_rpow_re_of_pos {x : } (hx : 0 < x) (y : ) :
    Complex.abs (x ^ y) = x ^ y.re
    theorem Complex.abs_cpow_eq_rpow_re_of_nonneg {x : } (hx : 0 x) {y : } (hy : y.re 0) :
    Complex.abs (x ^ y) = x ^ y.re
    theorem Complex.norm_natCast_cpow_of_re_ne_zero (n : ) {s : } (hs : s.re 0) :
    n ^ s = n ^ s.re
    theorem Complex.norm_natCast_cpow_of_pos {n : } (hn : 0 < n) (s : ) :
    n ^ s = n ^ s.re
    theorem Complex.norm_natCast_cpow_pos_of_pos {n : } (hn : 0 < n) (s : ) :
    0 < n ^ s
    theorem Complex.cpow_mul_ofReal_nonneg {x : } (hx : 0 x) (y : ) (z : ) :
    x ^ (y * z) = (x ^ y) ^ z

    Positivity extension #

    Extension for the positivity tactic: exponentiation by a real number is positive (namely 1) when the exponent is zero. The other cases are done in evalRpow.

    Instances For

      Extension for the positivity tactic: exponentiation by a real number is nonnegative when the base is nonnegative and positive when the base is positive.

      Instances For

        Further algebraic properties of rpow #

        theorem Real.rpow_mul {x : } (hx : 0 x) (y : ) (z : ) :
        x ^ (y * z) = (x ^ y) ^ z
        theorem Real.rpow_add_intCast {x : } (hx : x 0) (y : ) (n : ) :
        x ^ (y + n) = x ^ y * x ^ n
        theorem Real.rpow_add_natCast {x : } (hx : x 0) (y : ) (n : ) :
        x ^ (y + n) = x ^ y * x ^ n
        theorem Real.rpow_sub_intCast {x : } (hx : x 0) (y : ) (n : ) :
        x ^ (y - n) = x ^ y / x ^ n
        theorem Real.rpow_sub_natCast {x : } (hx : x 0) (y : ) (n : ) :
        x ^ (y - n) = x ^ y / x ^ n
        theorem Real.rpow_add_intCast' {x : } {y : } (hx : 0 x) {n : } (h : y + n 0) :
        x ^ (y + n) = x ^ y * x ^ n
        theorem Real.rpow_add_natCast' {x : } {y : } {n : } (hx : 0 x) (h : y + n 0) :
        x ^ (y + n) = x ^ y * x ^ n
        theorem Real.rpow_sub_intCast' {x : } {y : } (hx : 0 x) {n : } (h : y - n 0) :
        x ^ (y - n) = x ^ y / x ^ n
        theorem Real.rpow_sub_natCast' {x : } {y : } {n : } (hx : 0 x) (h : y - n 0) :
        x ^ (y - n) = x ^ y / x ^ n
        @[deprecated Real.rpow_add_intCast]
        theorem Real.rpow_add_int {x : } (hx : x 0) (y : ) (n : ) :
        x ^ (y + n) = x ^ y * x ^ n

        Alias of Real.rpow_add_intCast.

        @[deprecated Real.rpow_add_natCast]
        theorem Real.rpow_add_nat {x : } (hx : x 0) (y : ) (n : ) :
        x ^ (y + n) = x ^ y * x ^ n

        Alias of Real.rpow_add_natCast.

        @[deprecated Real.rpow_sub_intCast]
        theorem Real.rpow_sub_int {x : } (hx : x 0) (y : ) (n : ) :
        x ^ (y - n) = x ^ y / x ^ n

        Alias of Real.rpow_sub_intCast.

        @[deprecated Real.rpow_sub_natCast]
        theorem Real.rpow_sub_nat {x : } (hx : x 0) (y : ) (n : ) :
        x ^ (y - n) = x ^ y / x ^ n

        Alias of Real.rpow_sub_natCast.

        @[deprecated Real.rpow_add_intCast']
        theorem Real.rpow_add_int' {x : } {y : } (hx : 0 x) {n : } (h : y + n 0) :
        x ^ (y + n) = x ^ y * x ^ n

        Alias of Real.rpow_add_intCast'.

        @[deprecated Real.rpow_add_natCast']
        theorem Real.rpow_add_nat' {x : } {y : } {n : } (hx : 0 x) (h : y + n 0) :
        x ^ (y + n) = x ^ y * x ^ n

        Alias of Real.rpow_add_natCast'.

        @[deprecated Real.rpow_sub_intCast']
        theorem Real.rpow_sub_int' {x : } {y : } (hx : 0 x) {n : } (h : y - n 0) :
        x ^ (y - n) = x ^ y / x ^ n

        Alias of Real.rpow_sub_intCast'.

        @[deprecated Real.rpow_sub_natCast']
        theorem Real.rpow_sub_nat' {x : } {y : } {n : } (hx : 0 x) (h : y - n 0) :
        x ^ (y - n) = x ^ y / x ^ n

        Alias of Real.rpow_sub_natCast'.

        theorem Real.rpow_add_one {x : } (hx : x 0) (y : ) :
        x ^ (y + 1) = x ^ y * x
        theorem Real.rpow_sub_one {x : } (hx : x 0) (y : ) :
        x ^ (y - 1) = x ^ y / x
        theorem Real.rpow_add_one' {x : } {y : } (hx : 0 x) (h : y + 1 0) :
        x ^ (y + 1) = x ^ y * x
        theorem Real.rpow_one_add' {x : } {y : } (hx : 0 x) (h : 1 + y 0) :
        x ^ (1 + y) = x * x ^ y
        theorem Real.rpow_sub_one' {x : } {y : } (hx : 0 x) (h : y - 1 0) :
        x ^ (y - 1) = x ^ y / x
        theorem Real.rpow_one_sub' {x : } {y : } (hx : 0 x) (h : 1 - y 0) :
        x ^ (1 - y) = x / x ^ y
        @[simp]
        theorem Real.rpow_two (x : ) :
        x ^ 2 = x ^ 2
        theorem Real.rpow_neg_one (x : ) :
        x ^ (-1) = x⁻¹
        theorem Real.mul_rpow {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) :
        (x * y) ^ z = x ^ z * y ^ z
        theorem Real.inv_rpow {x : } (hx : 0 x) (y : ) :
        x⁻¹ ^ y = (x ^ y)⁻¹
        theorem Real.div_rpow {x : } {y : } (hx : 0 x) (hy : 0 y) (z : ) :
        (x / y) ^ z = x ^ z / y ^ z
        theorem Real.log_rpow {x : } (hx : 0 < x) (y : ) :
        Real.log (x ^ y) = y * Real.log x
        theorem Real.mul_log_eq_log_iff {x : } {y : } {z : } (hx : 0 < x) (hz : 0 < z) :
        y * Real.log x = Real.log z x ^ y = z
        @[simp]
        theorem Real.rpow_rpow_inv {x : } {y : } (hx : 0 x) (hy : y 0) :
        (x ^ y) ^ y⁻¹ = x
        @[simp]
        theorem Real.rpow_inv_rpow {x : } {y : } (hx : 0 x) (hy : y 0) :
        (x ^ y⁻¹) ^ y = x
        theorem Real.pow_rpow_inv_natCast {x : } {n : } (hx : 0 x) (hn : n 0) :
        (x ^ n) ^ (↑n)⁻¹ = x
        theorem Real.rpow_inv_natCast_pow {x : } {n : } (hx : 0 x) (hn : n 0) :
        (x ^ (↑n)⁻¹) ^ n = x
        theorem Real.rpow_natCast_mul {x : } (hx : 0 x) (n : ) (z : ) :
        x ^ (n * z) = (x ^ n) ^ z
        theorem Real.rpow_mul_natCast {x : } (hx : 0 x) (y : ) (n : ) :
        x ^ (y * n) = (x ^ y) ^ n
        theorem Real.rpow_intCast_mul {x : } (hx : 0 x) (n : ) (z : ) :
        x ^ (n * z) = (x ^ n) ^ z
        theorem Real.rpow_mul_intCast {x : } (hx : 0 x) (y : ) (n : ) :
        x ^ (y * n) = (x ^ y) ^ n

        Note: lemmas about (∏ i ∈ s, f i ^ r) such as Real.finset_prod_rpow are proved in Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean instead.

        Order and monotonicity #

        theorem Real.rpow_lt_rpow {x : } {y : } {z : } (hx : 0 x) (hxy : x < y) (hz : 0 < z) :
        x ^ z < y ^ z
        theorem Real.strictMonoOn_rpow_Ici_of_exponent_pos {r : } (hr : 0 < r) :
        StrictMonoOn (fun (x : ) => x ^ r) (Set.Ici 0)
        theorem Real.rpow_le_rpow {x : } {y : } {z : } (h : 0 x) (h₁ : x y) (h₂ : 0 z) :
        x ^ z y ^ z
        theorem Real.monotoneOn_rpow_Ici_of_exponent_nonneg {r : } (hr : 0 r) :
        MonotoneOn (fun (x : ) => x ^ r) (Set.Ici 0)
        theorem Real.rpow_lt_rpow_of_neg {x : } {y : } {z : } (hx : 0 < x) (hxy : x < y) (hz : z < 0) :
        y ^ z < x ^ z
        theorem Real.rpow_le_rpow_of_nonpos {x : } {y : } {z : } (hx : 0 < x) (hxy : x y) (hz : z 0) :
        y ^ z x ^ z
        theorem Real.rpow_lt_rpow_iff {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
        x ^ z < y ^ z x < y
        theorem Real.rpow_le_rpow_iff {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
        x ^ z y ^ z x y
        theorem Real.rpow_lt_rpow_iff_of_neg {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
        x ^ z < y ^ z y < x
        theorem Real.rpow_le_rpow_iff_of_neg {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
        x ^ z y ^ z y x
        theorem Real.le_rpow_inv_iff_of_pos {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
        x y ^ z⁻¹ x ^ z y
        theorem Real.rpow_inv_le_iff_of_pos {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
        x ^ z⁻¹ y x y ^ z
        theorem Real.lt_rpow_inv_iff_of_pos {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
        x < y ^ z⁻¹ x ^ z < y
        theorem Real.rpow_inv_lt_iff_of_pos {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
        x ^ z⁻¹ < y x < y ^ z
        theorem Real.le_rpow_inv_iff_of_neg {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
        x y ^ z⁻¹ y x ^ z
        theorem Real.lt_rpow_inv_iff_of_neg {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
        x < y ^ z⁻¹ y < x ^ z
        theorem Real.rpow_inv_lt_iff_of_neg {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
        x ^ z⁻¹ < y y ^ z < x
        theorem Real.rpow_inv_le_iff_of_neg {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
        x ^ z⁻¹ y y ^ z x
        theorem Real.rpow_lt_rpow_of_exponent_lt {x : } {y : } {z : } (hx : 1 < x) (hyz : y < z) :
        x ^ y < x ^ z
        theorem Real.rpow_le_rpow_of_exponent_le {x : } {y : } {z : } (hx : 1 x) (hyz : y z) :
        x ^ y x ^ z
        theorem Real.rpow_lt_rpow_of_exponent_neg {x : } {y : } {z : } (hy : 0 < y) (hxy : y < x) (hz : z < 0) :
        x ^ z < y ^ z
        theorem Real.strictAntiOn_rpow_Ioi_of_exponent_neg {r : } (hr : r < 0) :
        StrictAntiOn (fun (x : ) => x ^ r) (Set.Ioi 0)
        theorem Real.rpow_le_rpow_of_exponent_nonpos {z : } {x : } {y : } (hy : 0 < y) (hxy : y x) (hz : z 0) :
        x ^ z y ^ z
        theorem Real.antitoneOn_rpow_Ioi_of_exponent_nonpos {r : } (hr : r 0) :
        AntitoneOn (fun (x : ) => x ^ r) (Set.Ioi 0)
        @[simp]
        theorem Real.rpow_le_rpow_left_iff {x : } {y : } {z : } (hx : 1 < x) :
        x ^ y x ^ z y z
        @[simp]
        theorem Real.rpow_lt_rpow_left_iff {x : } {y : } {z : } (hx : 1 < x) :
        x ^ y < x ^ z y < z
        theorem Real.rpow_lt_rpow_of_exponent_gt {x : } {y : } {z : } (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
        x ^ y < x ^ z
        theorem Real.rpow_le_rpow_of_exponent_ge {x : } {y : } {z : } (hx0 : 0 < x) (hx1 : x 1) (hyz : z y) :
        x ^ y x ^ z
        @[simp]
        theorem Real.rpow_le_rpow_left_iff_of_base_lt_one {x : } {y : } {z : } (hx0 : 0 < x) (hx1 : x < 1) :
        x ^ y x ^ z z y
        @[simp]
        theorem Real.rpow_lt_rpow_left_iff_of_base_lt_one {x : } {y : } {z : } (hx0 : 0 < x) (hx1 : x < 1) :
        x ^ y < x ^ z z < y
        theorem Real.rpow_lt_one {x : } {z : } (hx1 : 0 x) (hx2 : x < 1) (hz : 0 < z) :
        x ^ z < 1
        theorem Real.rpow_le_one {x : } {z : } (hx1 : 0 x) (hx2 : x 1) (hz : 0 z) :
        x ^ z 1
        theorem Real.rpow_lt_one_of_one_lt_of_neg {x : } {z : } (hx : 1 < x) (hz : z < 0) :
        x ^ z < 1
        theorem Real.rpow_le_one_of_one_le_of_nonpos {x : } {z : } (hx : 1 x) (hz : z 0) :
        x ^ z 1
        theorem Real.one_lt_rpow {x : } {z : } (hx : 1 < x) (hz : 0 < z) :
        1 < x ^ z
        theorem Real.one_le_rpow {x : } {z : } (hx : 1 x) (hz : 0 z) :
        1 x ^ z
        theorem Real.one_lt_rpow_of_pos_of_lt_one_of_neg {x : } {z : } (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
        1 < x ^ z
        theorem Real.one_le_rpow_of_pos_of_le_one_of_nonpos {x : } {z : } (hx1 : 0 < x) (hx2 : x 1) (hz : z 0) :
        1 x ^ z
        theorem Real.rpow_lt_one_iff_of_pos {x : } {y : } (hx : 0 < x) :
        x ^ y < 1 1 < x y < 0 x < 1 0 < y
        theorem Real.rpow_lt_one_iff {x : } {y : } (hx : 0 x) :
        x ^ y < 1 x = 0 y 0 1 < x y < 0 x < 1 0 < y
        theorem Real.rpow_lt_one_iff' {x : } {y : } (hx : 0 x) (hy : 0 < y) :
        x ^ y < 1 x < 1
        theorem Real.one_lt_rpow_iff_of_pos {x : } {y : } (hx : 0 < x) :
        1 < x ^ y 1 < x 0 < y x < 1 y < 0
        theorem Real.one_lt_rpow_iff {x : } {y : } (hx : 0 x) :
        1 < x ^ y 1 < x 0 < y 0 < x x < 1 y < 0
        theorem Real.rpow_le_rpow_of_exponent_ge' {x : } {y : } {z : } (hx0 : 0 x) (hx1 : x 1) (hz : 0 z) (hyz : z y) :
        x ^ y x ^ z
        theorem Real.rpow_left_injOn {x : } (hx : x 0) :
        Set.InjOn (fun (y : ) => y ^ x) {y : | 0 y}
        theorem Real.rpow_left_inj {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : z 0) :
        x ^ z = y ^ z x = y
        theorem Real.rpow_inv_eq {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : z 0) :
        x ^ z⁻¹ = y x = y ^ z
        theorem Real.eq_rpow_inv {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : z 0) :
        x = y ^ z⁻¹ x ^ z = y
        theorem Real.le_rpow_iff_log_le {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) :
        x y ^ z Real.log x z * Real.log y
        theorem Real.le_pow_iff_log_le {x : } {y : } {n : } (hx : 0 < x) (hy : 0 < y) :
        x y ^ n Real.log x n * Real.log y
        theorem Real.le_zpow_iff_log_le {x : } {y : } {n : } (hx : 0 < x) (hy : 0 < y) :
        x y ^ n Real.log x n * Real.log y
        theorem Real.le_rpow_of_log_le {x : } {y : } {z : } (hy : 0 < y) (h : Real.log x z * Real.log y) :
        x y ^ z
        theorem Real.le_pow_of_log_le {x : } {y : } {n : } (hy : 0 < y) (h : Real.log x n * Real.log y) :
        x y ^ n
        theorem Real.le_zpow_of_log_le {x : } {y : } {n : } (hy : 0 < y) (h : Real.log x n * Real.log y) :
        x y ^ n
        theorem Real.lt_rpow_iff_log_lt {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) :
        x < y ^ z Real.log x < z * Real.log y
        theorem Real.lt_pow_iff_log_lt {x : } {y : } {n : } (hx : 0 < x) (hy : 0 < y) :
        x < y ^ n Real.log x < n * Real.log y
        theorem Real.lt_zpow_iff_log_lt {x : } {y : } {n : } (hx : 0 < x) (hy : 0 < y) :
        x < y ^ n Real.log x < n * Real.log y
        theorem Real.lt_rpow_of_log_lt {x : } {y : } {z : } (hy : 0 < y) (h : Real.log x < z * Real.log y) :
        x < y ^ z
        theorem Real.lt_pow_of_log_lt {x : } {y : } {n : } (hy : 0 < y) (h : Real.log x < n * Real.log y) :
        x < y ^ n
        theorem Real.lt_zpow_of_log_lt {x : } {y : } {n : } (hy : 0 < y) (h : Real.log x < n * Real.log y) :
        x < y ^ n
        theorem Real.rpow_le_iff_le_log {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) :
        x ^ z y z * Real.log x Real.log y
        theorem Real.pow_le_iff_le_log {x : } {y : } {n : } (hx : 0 < x) (hy : 0 < y) :
        x ^ n y n * Real.log x Real.log y
        theorem Real.zpow_le_iff_le_log {x : } {y : } {n : } (hx : 0 < x) (hy : 0 < y) :
        x ^ n y n * Real.log x Real.log y
        theorem Real.le_log_of_rpow_le {x : } {y : } {z : } (hx : 0 < x) (h : x ^ z y) :
        theorem Real.le_log_of_pow_le {x : } {y : } {n : } (hx : 0 < x) (h : x ^ n y) :
        theorem Real.le_log_of_zpow_le {x : } {y : } {n : } (hx : 0 < x) (h : x ^ n y) :
        theorem Real.rpow_le_of_le_log {x : } {y : } {z : } (hy : 0 < y) (h : Real.log x z * Real.log y) :
        x y ^ z
        theorem Real.pow_le_of_le_log {x : } {y : } {n : } (hy : 0 < y) (h : Real.log x n * Real.log y) :
        x y ^ n
        theorem Real.zpow_le_of_le_log {x : } {y : } {n : } (hy : 0 < y) (h : Real.log x n * Real.log y) :
        x y ^ n
        theorem Real.rpow_lt_iff_lt_log {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) :
        x ^ z < y z * Real.log x < Real.log y
        theorem Real.pow_lt_iff_lt_log {x : } {y : } {n : } (hx : 0 < x) (hy : 0 < y) :
        x ^ n < y n * Real.log x < Real.log y
        theorem Real.zpow_lt_iff_lt_log {x : } {y : } {n : } (hx : 0 < x) (hy : 0 < y) :
        x ^ n < y n * Real.log x < Real.log y
        theorem Real.lt_log_of_rpow_lt {x : } {y : } {z : } (hx : 0 < x) (h : x ^ z < y) :
        theorem Real.lt_log_of_pow_lt {x : } {y : } {n : } (hx : 0 < x) (h : x ^ n < y) :
        n * Real.log x < Real.log y
        theorem Real.lt_log_of_zpow_lt {x : } {y : } {n : } (hx : 0 < x) (h : x ^ n < y) :
        n * Real.log x < Real.log y
        theorem Real.rpow_lt_of_lt_log {x : } {y : } {z : } (hy : 0 < y) (h : Real.log x < z * Real.log y) :
        x < y ^ z
        theorem Real.pow_lt_of_lt_log {x : } {y : } {n : } (hy : 0 < y) (h : Real.log x < n * Real.log y) :
        x < y ^ n
        theorem Real.zpow_lt_of_lt_log {x : } {y : } {n : } (hy : 0 < y) (h : Real.log x < n * Real.log y) :
        x < y ^ n
        theorem Real.rpow_le_one_iff_of_pos {x : } {y : } (hx : 0 < x) :
        x ^ y 1 1 x y 0 x 1 0 y
        theorem Real.abs_log_mul_self_rpow_lt (x : ) (t : ) (h1 : 0 < x) (h2 : x 1) (ht : 0 < t) :
        |Real.log x * x ^ t| < 1 / t

        Bound for |log x * x ^ t| in the interval (0, 1], for positive real t.

        theorem Real.log_le_rpow_div {x : } {ε : } (hx : 0 x) (hε : 0 < ε) :
        Real.log x x ^ ε / ε

        log x is bounded above by a multiple of every power of x with positive exponent.

        theorem Real.log_natCast_le_rpow_div (n : ) {ε : } (hε : 0 < ε) :
        Real.log n n ^ ε / ε

        The (real) logarithm of a natural number n is bounded by a multiple of every power of n with positive exponent.

        theorem Real.strictMono_rpow_of_base_gt_one {b : } (hb : 1 < b) :
        StrictMono fun (x : ) => b ^ x
        theorem Real.monotone_rpow_of_base_ge_one {b : } (hb : 1 b) :
        Monotone fun (x : ) => b ^ x
        theorem Real.strictAnti_rpow_of_base_lt_one {b : } (hb₀ : 0 < b) (hb₁ : b < 1) :
        StrictAnti fun (x : ) => b ^ x
        theorem Real.antitone_rpow_of_base_le_one {b : } (hb₀ : 0 < b) (hb₁ : b 1) :
        Antitone fun (x : ) => b ^ x
        theorem Real.rpow_le_rpow_of_exponent_le_or_ge {x : } {y : } {z : } (h : 1 x y z 0 < x x 1 z y) :
        x ^ y x ^ z

        Guessing rule for the bound tactic: when trying to prove x ^ y ≤ x ^ z, we can either assume 1 ≤ x or 0 < x ≤ 1.

        theorem Complex.norm_prime_cpow_le_one_half (p : Nat.Primes) {s : } (hs : 1 < s.re) :
        p ^ (-s) 1 / 2
        theorem Complex.one_sub_prime_cpow_ne_zero {p : } (hp : Nat.Prime p) {s : } (hs : 1 < s.re) :
        1 - p ^ (-s) 0
        theorem Complex.norm_natCast_cpow_le_norm_natCast_cpow_of_pos {n : } (hn : 0 < n) {w : } {z : } (h : w.re z.re) :
        n ^ w n ^ z
        theorem Complex.norm_natCast_cpow_le_norm_natCast_cpow_iff {n : } (hn : 1 < n) {w : } {z : } :
        n ^ w n ^ z w.re z.re
        theorem Complex.norm_log_natCast_le_rpow_div (n : ) {ε : } (hε : 0 < ε) :
        Complex.log n n ^ ε / ε

        Square roots of reals #

        theorem Real.sqrt_eq_rpow (x : ) :
        x = x ^ (1 / 2)
        theorem Real.rpow_div_two_eq_sqrt {x : } (r : ) (hx : 0 x) :
        x ^ (r / 2) = x ^ r
        theorem Real.exists_rat_pow_btwn_rat_aux {n : } (hn : n 0) (x : ) (y : ) (h : x < y) (hy : 0 < y) :
        ∃ (q : ), 0 < q x < q ^ n q ^ n < y
        theorem Real.exists_rat_pow_btwn_rat {n : } (hn : n 0) {x : } {y : } (h : x < y) (hy : 0 < y) :
        ∃ (q : ), 0 < q x < q ^ n q ^ n < y
        theorem Real.exists_rat_pow_btwn {n : } {α : Type u_1} [LinearOrderedField α] [Archimedean α] (hn : n 0) {x : α} {y : α} (h : x < y) (hy : 0 < y) :
        ∃ (q : ), 0 < q x < q ^ n q ^ n < y

        There is a rational power between any two positive elements of an archimedean ordered field.

        theorem Complex.cpow_inv_two_re (x : ) :
        (x ^ 2⁻¹).re = ((Complex.abs x + x.re) / 2)
        theorem Complex.cpow_inv_two_im_eq_sqrt {x : } (hx : 0 x.im) :
        (x ^ 2⁻¹).im = ((Complex.abs x - x.re) / 2)
        theorem Complex.cpow_inv_two_im_eq_neg_sqrt {x : } (hx : x.im < 0) :
        (x ^ 2⁻¹).im = -((Complex.abs x - x.re) / 2)
        theorem Complex.abs_cpow_inv_two_im (x : ) :
        |(x ^ 2⁻¹).im| = ((Complex.abs x - x.re) / 2)

        Tactic extensions for real powers #

        theorem Mathlib.Meta.NormNum.isRat_rpow_pos {a : } {b : } {nb : } {num : } {den : } (pb : Mathlib.Meta.NormNum.IsNat b nb) (pe' : Mathlib.Meta.NormNum.IsRat (a ^ nb) num den) :
        theorem Mathlib.Meta.NormNum.isRat_rpow_neg {a : } {b : } {nb : } {num : } {den : } (pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)) (pe' : Mathlib.Meta.NormNum.IsRat (a ^ Int.negOfNat nb) num den) :

        Evaluates expressions of the form a ^ b when a and b are both reals.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[deprecated Real.rpow_nonneg]
          theorem rpow_nonneg_of_nonneg {x : } (hx : 0 x) (y : ) :
          0 x ^ y

          Alias of Real.rpow_nonneg.