logRatio_nonneg — Mathlib

English

For hc > 1/2, hd < 1 and c ≤ d, we have logRatio(c) ≤ logRatio(d).

Русский

Для hc > 1/2, hd < 1 и c ≤ d верно logRatio(c) ≤ logRatio(d).

LaTeX

$$\\text{If } (2)^{-1} < c \\le d \\le 1, \\quad \\logRatio(c) \\le \\logRatio(d)$$

Lean4

theorem logRatio_nonneg {c : ℝ≥0∞} (hc_ge : (2 : ℝ≥0∞)⁻¹ ≤ c) (hc_le : c ≤ 1) : 0 ≤ logRatio c :=
  by
  by_cases hc1 : c = 2⁻¹
  · simp [logRatio, hc1]
  by_cases hc2 : c = 1
  · simp [logRatio, hc2]
  exact (logRatio_pos (lt_of_le_of_ne' hc_ge hc1) (lt_of_le_of_ne hc_le hc2)).le

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