f_add_nat_eq — Mathlib

English

If f satisfies f(y+1) = f(y) + log y for y>0, then for any n ∈ ℕ, f(x+n) = f(x) + ∑_{m=0}^{n-1} log(x+m).

Русский

Если f удовлетворяет f(y+1) = f(y) + log y для y>0, то для любого x и n ∈ ℕ выполняется f(x+n) = f(x) + ∑_{m=0}^{n-1} log(x+m).

LaTeX

$$$$ f(x+n) = f(x) + \sum_{m=0}^{n-1} \log(x+m). $$$$

Lean4

theorem f_add_nat_eq (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) (hx : 0 < x) (n : ℕ) :
    f (x + n) = f x + ∑ m ∈ Finset.range n, log (x + m) := by
  induction n with
  | zero => simp
  | succ n hn =>
    have : x + n.succ = x + n + 1 := by push_cast; ring
    rw [this, hf_feq, hn]
    · rw [Finset.range_add_one, Finset.sum_insert Finset.notMem_range_self]
      abel
    · linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))]

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