Commit 2024-08-26 16:52 a16c2767

View on Github →

feat(Analysis/SpecialFunctions/Pow/Real): Specialise some lemmas to natural/integers powers (#15859) From LeanAPAP

Estimated changes

added theorem Real.le_log_of_pow_le
added theorem Real.le_log_of_rpow_le
added theorem Real.le_log_of_zpow_le
added theorem Real.le_pow_iff_log_le
added theorem Real.le_pow_of_log_le
modified theorem Real.le_rpow_iff_log_le
modified theorem Real.le_rpow_of_log_le
added theorem Real.le_zpow_of_log_le
added theorem Real.lt_log_of_pow_lt
added theorem Real.lt_log_of_rpow_lt
added theorem Real.lt_log_of_zpow_lt
added theorem Real.lt_pow_iff_log_lt
added theorem Real.lt_pow_of_log_lt
modified theorem Real.lt_rpow_iff_log_lt
modified theorem Real.lt_rpow_of_log_lt
added theorem Real.lt_zpow_of_log_lt
added theorem Real.pow_le_iff_le_log
added theorem Real.pow_le_of_le_log
added theorem Real.pow_lt_iff_lt_log
added theorem Real.pow_lt_of_lt_log
added theorem Real.rpow_le_of_le_log
added theorem Real.rpow_lt_of_lt_log
added theorem Real.zpow_le_of_le_log
added theorem Real.zpow_lt_of_lt_log