English
If f: ℝ → ℝ satisfies f(y+1) = f(y) + log y for all y>0 and n ≠ 0, then f(n) = f(1) + log((n−1)!).
Русский
Если f: ℝ → ℝ удовлетворяет f(y+1) = f(y) + log y для всех y>0 и n ≠ 0, тогда f(n) = f(1) + log((n−1)!).
LaTeX
$$$$ f(n) = f(1) + \log((n-1)!). $$$$
Lean4
theorem f_nat_eq (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) (hn : n ≠ 0) : f n = f 1 + log (n - 1)! :=
by
refine Nat.le_induction (by simp) (fun m hm IH => ?_) n (Nat.one_le_iff_ne_zero.2 hn)
have A : 0 < (m : ℝ) := Nat.cast_pos.2 hm
simp only [hf_feq A, Nat.cast_add, Nat.cast_one, Nat.add_succ_sub_one, add_zero]
rw [IH, add_assoc, ← log_mul (Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)) A.ne', ← Nat.cast_mul]
conv_rhs => rw [← Nat.succ_pred_eq_of_pos hm, Nat.factorial_succ, mul_comm]
congr
exact (Nat.succ_pred_eq_of_pos hm).symm
