Commit 2020-06-05 11:58 a433eb07

View on Github →

feat(analysis/special_functions/pow): real powers on ennreal (#2951) Real powers of extended nonnegative real numbers. We develop an API based on that of real powers of reals and nnreals, proving the corresponding lemmas.

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem ennreal.coe_mul_rpow

added theorem ennreal.coe_rpow_of_ne_zero

added theorem ennreal.coe_rpow_of_nonneg

added theorem ennreal.mul_rpow_of_ne_top

added theorem ennreal.mul_rpow_of_ne_zero

added theorem ennreal.one_le_rpow

added theorem ennreal.one_lt_rpow

added theorem ennreal.one_rpow

added theorem ennreal.rpow_add

added theorem ennreal.rpow_eq_pow

added theorem ennreal.rpow_eq_top_iff

added theorem ennreal.rpow_eq_zero_iff

added theorem ennreal.rpow_le_one

added theorem ennreal.rpow_le_rpow

added theorem ennreal.rpow_le_rpow_of_exponent_ge

added theorem ennreal.rpow_le_rpow_of_exponent_le

added theorem ennreal.rpow_lt_one

added theorem ennreal.rpow_lt_rpow

added theorem ennreal.rpow_lt_rpow_of_exponent_gt

added theorem ennreal.rpow_lt_rpow_of_exponent_lt

added theorem ennreal.rpow_mul

added theorem ennreal.rpow_nat_cast

added theorem ennreal.rpow_neg

added theorem ennreal.rpow_neg_one

added theorem ennreal.rpow_one

added theorem ennreal.rpow_zero

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_of_neg

added theorem ennreal.zero_rpow_of_pos

modified theorem nnreal.rpow_add

modified theorem nnreal.rpow_le_one

modified theorem real.rpow_le_one