Commit 2023-08-13 08:12 f697cccc

View on Github →

feat: lemmas about monotonicity and asymptotics of rpow (#6140)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

added theorem tendsto_rpow_atBot_of_base_gt_one

added theorem tendsto_rpow_atBot_of_base_lt_one

added theorem tendsto_rpow_atTop_of_base_gt_one

added theorem tendsto_rpow_atTop_of_base_lt_one

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

added theorem Real.antitone_rpow_of_base_le_one

added theorem Real.monotone_rpow_of_base_ge_one

added theorem Real.rpow_le_rpow_of_exponent_nonpos

added theorem Real.rpow_lt_rpow_of_exponent_neg

added theorem Real.strictAnti_rpow_of_base_lt_one

added theorem Real.strictMono_rpow_of_base_gt_one