Commit 2023-05-21 12:39 85b38a0e

View on Github →

feat: port Analysis.SpecialFunctions.Pow.NNReal (#4161)

Estimated changes

Modified Mathlib.lean

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

added theorem ENNReal.coe_mul_rpow

added theorem ENNReal.coe_rpow_def

added theorem ENNReal.coe_rpow_of_ne_zero

added theorem ENNReal.coe_rpow_of_nonneg

added theorem ENNReal.div_rpow_of_nonneg

added theorem ENNReal.inv_rpow

added theorem ENNReal.le_rpow_one_div_iff

added theorem ENNReal.le_rpow_self_of_one_le

added theorem ENNReal.lt_rpow_one_div_iff

added theorem ENNReal.monotone_rpow_of_nonneg

added theorem ENNReal.mul_rpow_eq_ite

added theorem ENNReal.mul_rpow_of_ne_top

added theorem ENNReal.mul_rpow_of_ne_zero

added theorem ENNReal.mul_rpow_of_nonneg

added theorem ENNReal.ofReal_rpow_of_nonneg

added theorem ENNReal.ofReal_rpow_of_pos

added theorem ENNReal.one_le_rpow

added theorem ENNReal.one_le_rpow_of_pos_of_le_one_of_neg

added theorem ENNReal.one_lt_rpow

added theorem ENNReal.one_lt_rpow_of_pos_of_lt_one_of_neg

added theorem ENNReal.one_rpow

added def ENNReal.orderIsoRpow

added theorem ENNReal.orderIsoRpow_symm_apply

added theorem ENNReal.rpow_add

added theorem ENNReal.rpow_eq_pow

added theorem ENNReal.rpow_eq_top_iff

added theorem ENNReal.rpow_eq_top_iff_of_pos

added theorem ENNReal.rpow_eq_top_of_nonneg

added theorem ENNReal.rpow_eq_zero_iff

added theorem ENNReal.rpow_le_one

added theorem ENNReal.rpow_le_one_of_one_le_of_neg

added theorem ENNReal.rpow_le_rpow

added theorem ENNReal.rpow_le_rpow_iff

added theorem ENNReal.rpow_le_rpow_of_exponent_ge

added theorem ENNReal.rpow_le_rpow_of_exponent_le

added theorem ENNReal.rpow_le_self_of_le_one

added theorem ENNReal.rpow_left_bijective

added theorem ENNReal.rpow_left_injective

added theorem ENNReal.rpow_left_surjective

added theorem ENNReal.rpow_lt_one

added theorem ENNReal.rpow_lt_one_of_one_lt_of_neg

added theorem ENNReal.rpow_lt_rpow

added theorem ENNReal.rpow_lt_rpow_iff

added theorem ENNReal.rpow_lt_rpow_of_exponent_gt

added theorem ENNReal.rpow_lt_rpow_of_exponent_lt

added theorem ENNReal.rpow_lt_top_of_nonneg

added theorem ENNReal.rpow_mul

added theorem ENNReal.rpow_nat_cast

added theorem ENNReal.rpow_ne_top_of_nonneg

added theorem ENNReal.rpow_neg

added theorem ENNReal.rpow_neg_one

added theorem ENNReal.rpow_one

added theorem ENNReal.rpow_one_div_le_iff

added theorem ENNReal.rpow_pos

added theorem ENNReal.rpow_pos_of_nonneg

added theorem ENNReal.rpow_sub

added theorem ENNReal.rpow_two

added theorem ENNReal.rpow_zero

added theorem ENNReal.strictMono_rpow_of_pos

added theorem ENNReal.toNNReal_rpow

added theorem ENNReal.toReal_rpow

added theorem ENNReal.top_rpow_def

added theorem ENNReal.top_rpow_of_neg

added theorem ENNReal.top_rpow_of_pos

added theorem ENNReal.zero_rpow_def

added theorem ENNReal.zero_rpow_mul_self

added theorem ENNReal.zero_rpow_of_neg

added theorem ENNReal.zero_rpow_of_pos

added theorem NNReal.coe_rpow

added theorem NNReal.div_rpow

added theorem NNReal.eq_rpow_one_div_iff

added theorem NNReal.inv_rpow

added theorem NNReal.le_rpow_one_div_iff

added theorem NNReal.mul_rpow

added theorem NNReal.one_le_rpow

added theorem NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos

added theorem NNReal.one_lt_rpow

added theorem NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg

added theorem NNReal.one_rpow

added theorem NNReal.pow_nat_rpow_nat_inv

added theorem NNReal.rpow_add'

added theorem NNReal.rpow_add

added theorem NNReal.rpow_eq_pow

added theorem NNReal.rpow_eq_rpow_iff

added theorem NNReal.rpow_eq_zero_iff

added theorem NNReal.rpow_inv_rpow_self

added theorem NNReal.rpow_le_one

added theorem NNReal.rpow_le_one_of_one_le_of_nonpos

added theorem NNReal.rpow_le_rpow

added theorem NNReal.rpow_le_rpow_iff

added theorem NNReal.rpow_le_rpow_of_exponent_ge

added theorem NNReal.rpow_le_rpow_of_exponent_le

added theorem NNReal.rpow_le_self_of_le_one

added theorem NNReal.rpow_left_bijective

added theorem NNReal.rpow_left_injective

added theorem NNReal.rpow_left_surjective

added theorem NNReal.rpow_lt_one

added theorem NNReal.rpow_lt_one_of_one_lt_of_neg

added theorem NNReal.rpow_lt_rpow

added theorem NNReal.rpow_lt_rpow_iff

added theorem NNReal.rpow_lt_rpow_of_exponent_gt

added theorem NNReal.rpow_lt_rpow_of_exponent_lt

added theorem NNReal.rpow_mul

added theorem NNReal.rpow_nat_cast

added theorem NNReal.rpow_nat_inv_pow_nat

added theorem NNReal.rpow_neg

added theorem NNReal.rpow_neg_one

added theorem NNReal.rpow_one

added theorem NNReal.rpow_one_div_eq_iff

added theorem NNReal.rpow_one_div_le_iff

added theorem NNReal.rpow_pos

added theorem NNReal.rpow_self_rpow_inv

added theorem NNReal.rpow_sub'

added theorem NNReal.rpow_sub

added theorem NNReal.rpow_two

added theorem NNReal.rpow_zero

added theorem NNReal.sqrt_eq_rpow

added theorem NNReal.zero_rpow

added theorem Real.toNNReal_rpow_of_nonneg