Commit 2023-05-20 09:37 848e5dfc

View on Github →

feat: port Analysis.SpecialFunctions.Pow.Real (#4085)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

added theorem Complex.abs_cpow_eq_rpow_re_of_nonneg

added theorem Complex.abs_cpow_eq_rpow_re_of_pos

added theorem Complex.abs_cpow_inv_nat

added theorem Complex.abs_cpow_le

added theorem Complex.abs_cpow_of_imp

added theorem Complex.abs_cpow_of_ne_zero

added theorem Complex.abs_cpow_real

added theorem Complex.of_real_cpow

added theorem Complex.of_real_cpow_of_nonpos

added theorem Real.abs_log_mul_self_rpow_lt

added theorem Real.abs_rpow_le_abs_rpow

added theorem Real.abs_rpow_le_exp_log_mul

added theorem Real.abs_rpow_of_nonneg

added theorem Real.div_rpow

added theorem Real.eq_zero_rpow_iff

added theorem Real.exists_rat_pow_btwn

added theorem Real.exists_rat_pow_btwn_rat

added theorem Real.exists_rat_pow_btwn_rat_aux

added theorem Real.exp_mul

added theorem Real.exp_one_rpow

added theorem Real.inv_rpow

added theorem Real.le_rpow_add

added theorem Real.le_rpow_iff_log_le

added theorem Real.le_rpow_inv_iff_of_neg

added theorem Real.le_rpow_of_log_le

added theorem Real.log_rpow

added theorem Real.lt_rpow_iff_log_lt

added theorem Real.lt_rpow_inv_iff_of_neg

added theorem Real.lt_rpow_of_log_lt

added theorem Real.mul_rpow

added theorem Real.norm_rpow_of_nonneg

added theorem Real.one_le_rpow

added theorem Real.one_le_rpow_of_pos_of_le_one_of_nonpos

added theorem Real.one_lt_rpow

added theorem Real.one_lt_rpow_iff

added theorem Real.one_lt_rpow_iff_of_pos

added theorem Real.one_lt_rpow_of_pos_of_lt_one_of_neg

added theorem Real.one_rpow

added theorem Real.pow_nat_rpow_nat_inv

added theorem Real.rpow_add'

added theorem Real.rpow_add

added theorem Real.rpow_add_int

added theorem Real.rpow_add_nat

added theorem Real.rpow_add_of_nonneg

added theorem Real.rpow_add_one

added theorem Real.rpow_def

added theorem Real.rpow_def_of_neg

added theorem Real.rpow_def_of_nonneg

added theorem Real.rpow_def_of_nonpos

added theorem Real.rpow_def_of_pos

added theorem Real.rpow_div_two_eq_sqrt

added theorem Real.rpow_eq_pow

added theorem Real.rpow_eq_zero_iff_of_nonneg

added theorem Real.rpow_int_cast

added theorem Real.rpow_inv_le_iff_of_neg

added theorem Real.rpow_inv_lt_iff_of_neg

added theorem Real.rpow_le_one

added theorem Real.rpow_le_one_iff_of_pos

added theorem Real.rpow_le_one_of_one_le_of_nonpos

added theorem Real.rpow_le_rpow

added theorem Real.rpow_le_rpow_iff

added theorem Real.rpow_le_rpow_left_iff

added theorem Real.rpow_le_rpow_left_iff_of_base_lt_one

added theorem Real.rpow_le_rpow_of_exponent_ge'

added theorem Real.rpow_le_rpow_of_exponent_ge

added theorem Real.rpow_le_rpow_of_exponent_le

added theorem Real.rpow_left_injOn

added theorem Real.rpow_lt_one

added theorem Real.rpow_lt_one_iff

added theorem Real.rpow_lt_one_iff_of_pos

added theorem Real.rpow_lt_one_of_one_lt_of_neg

added theorem Real.rpow_lt_rpow

added theorem Real.rpow_lt_rpow_iff

added theorem Real.rpow_lt_rpow_left_iff

added theorem Real.rpow_lt_rpow_left_iff_of_base_lt_one

added theorem Real.rpow_lt_rpow_of_exponent_gt

added theorem Real.rpow_lt_rpow_of_exponent_lt

added theorem Real.rpow_mul

added theorem Real.rpow_nat_cast

added theorem Real.rpow_nat_inv_pow_nat

added theorem Real.rpow_neg

added theorem Real.rpow_neg_one

added theorem Real.rpow_nonneg_of_nonneg

added theorem Real.rpow_one

added theorem Real.rpow_pos_of_pos

added theorem Real.rpow_sub'

added theorem Real.rpow_sub

added theorem Real.rpow_sub_int

added theorem Real.rpow_sub_nat

added theorem Real.rpow_sub_one

added theorem Real.rpow_sum_of_nonneg

added theorem Real.rpow_sum_of_pos

added theorem Real.rpow_two

added theorem Real.rpow_zero

added theorem Real.sqrt_eq_rpow

added theorem Real.zero_rpow

added theorem Real.zero_rpow_eq_iff

added theorem Real.zero_rpow_le_one

added theorem Real.zero_rpow_nonneg