Commit 2020-08-15 12:43 18746ef6

View on Github →

feat(analysis/special_functions/pow): Added lemmas for rpow of neg exponent (#3715) I noticed that the library was missing some lemmas regarding the bounds of rpow of a negative exponent so I added them. I cleaned up the other similar preexisting lemmas for consistency. I then repeated the process for nnreal lemmas.

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem nnreal.one_le_rpow_of_pos_of_le_one_of_nonpos

added theorem nnreal.one_lt_rpow_of_pos_of_lt_one_of_neg

added theorem nnreal.rpow_le_one_of_one_le_of_nonpos

modified theorem nnreal.rpow_lt_one

added theorem nnreal.rpow_lt_one_of_one_lt_of_neg

modified theorem real.one_le_rpow

added theorem real.one_le_rpow_of_pos_of_le_one_of_nonpos

modified theorem real.one_lt_rpow

added theorem real.one_lt_rpow_of_pos_of_lt_one_of_neg

modified theorem real.rpow_le_one

added theorem real.rpow_le_one_of_one_le_of_nonpos

modified theorem real.rpow_lt_one

added theorem real.rpow_lt_one_of_one_lt_of_neg