logRatio_mono — Mathlib

English

logRatio(c) = log(c/(1−c)) / (8(1+√2)^2).

Русский

logRatio(c) = log(c/(1−c)) / (8(1+√2)^2).

LaTeX

$$\\operatorname{logRatio}(c) = \\dfrac{\\log\\left( \\dfrac{c}{1-c} \\right)}{8\\,(1+\\sqrt{2})^2}$$

Lean4

theorem logRatio_mono {c d : ℝ≥0∞} (hc : (2 : ℝ≥0∞)⁻¹ < c) (hd : d < 1) (h : c ≤ d) : logRatio c ≤ logRatio d :=
  by
  unfold logRatio
  gcongr
  · refine div_pos ?_ ?_
    · rw [ENNReal.toReal_pos_iff]
      exact ⟨lt_trans (by norm_num) hc, h.trans_lt (by finiteness)⟩
    · simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt]
      exact ⟨h.trans_lt hd, by finiteness⟩
  · simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hd, true_and]
    finiteness
  · finiteness
  · finiteness

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