ge_logGammaSeq — Mathlib

English

Under the same hypotheses as above, for every 0 < x ≤ 1 and every n ≠ 0, we have f(1) + logGammaSeq(x, n) ≤ f(x).

Русский

При тех же предположениях, что и выше, для каждого 0 < x ≤ 1 и любого n ≠ 0 выполняется неравенство f(1) + logGammaSeq(x, n) ≤ f(x).

LaTeX

$$$ f(1) + \logGammaSeq(x,n) \le f(x) $$$

Lean4

theorem ge_logGammaSeq (hf_conv : ConvexOn ℝ (Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y)
    (hx : 0 < x) (hn : n ≠ 0) : f 1 + logGammaSeq x n ≤ f x :=
  by
  dsimp [logGammaSeq]
  rw [← add_sub_assoc, sub_le_iff_le_add, ← f_add_nat_eq (@hf_feq) hx, add_comm x _]
  refine le_trans (le_of_eq ?_) (f_add_nat_ge hf_conv @hf_feq ?_ hx)
  · rw [f_nat_eq @hf_feq, Nat.add_sub_cancel, Nat.cast_add_one, add_sub_cancel_right]
    · ring
    · exact Nat.succ_ne_zero _
  · cutsat

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