logRatio_pos — Mathlib

English

If (1/2) < c and c < 1, then logRatio(c) > 0.

Русский

Если (1/2) < c < 1, то logRatio(c) > 0.

LaTeX

$$\\text{If } \\tfrac12 < c < 1, \\quad \\logRatio(c) > 0$$

Lean4

theorem logRatio_pos {c : ℝ≥0∞} (hc_gt : (2 : ℝ≥0∞)⁻¹ < c) (hc_lt : c < 1) : 0 < logRatio c :=
  by
  refine div_pos (Real.log_pos ?_) (by positivity)
  rw [one_lt_div_iff]
  refine Or.inl ⟨?_, ?_⟩
  · simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, true_and]
    finiteness
  · refine (ENNReal.toReal_lt_toReal (by finiteness) (by finiteness)).mpr ?_
    refine ENNReal.sub_lt_of_lt_add hc_lt.le ?_
    rw [← two_mul]
    rwa [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt

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