summable_log_one_add_of_summable — Mathlib

English

If f is summable as a real sequence, then log(1+f) is summable as well.

Русский

Если последовательность f суммируема, то log(1+f) тоже суммируема.

LaTeX

$$$\text{Summable}(\log(1+f_i))$ given $\text{Summable}(f_i)$$$

Lean4

theorem summable_log_one_add_of_summable (hf : Summable f) : Summable (fun i ↦ log (1 + f i)) :=
  by
  rw [← summable_ofReal]
  apply (Complex.summable_log_one_add_of_summable (summable_ofReal.mpr hf)).congr_cofinite
  filter_upwards [hf.tendsto_cofinite_zero.eventually_const_le neg_one_lt_zero] with i hi
  rw [ofReal_log, ofReal_add, ofReal_one]
  linarith

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