lt_log_of_pow_lt

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.lt_log_of_pow_lt

English

If x > 0 and x^z ≤ y, then z log x ≤ log y.

Русский

Если x > 0 и x^z ≤ y, то z log x ≤ log y.

LaTeX

$$$0 < x \land x^z \le y \Rightarrow z \log x \le \log y$$$

Lean4

theorem lt_log_of_pow_lt (hx : 0 < x) (h : x ^ n < y) : n * log x < log y :=
  lt_log_of_rpow_lt hx (rpow_natCast _ _ ▸ h)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru