summable_log_norm_one_add — Mathlib

English

If ∑‖f‖ is summable, then ∑ log⁺(‖1+f‖) is summable.

Русский

Если ∑‖f‖ суммируема, то ∑ log⁺(‖1+f‖) суммируема.

LaTeX

$$$\text{Summable}(\|1 + f\|)$ given $\text{Summable}(\|f\|)$ and appropriate bounds.$$

Lean4

theorem summable_log_norm_one_add (hu : Summable fun n ↦ ‖f n‖) : Summable fun i ↦ Real.log ‖1 + f i‖ :=
  by
  suffices Summable (‖1 + f ·‖ - 1) from (Real.summable_log_one_add_of_summable this).congr (by simp)
  refine .of_norm (hu.of_nonneg_of_le (fun i ↦ by positivity) fun i ↦ ?_)
  simp only [Real.norm_eq_abs, abs_le]
  constructor
  · simpa using norm_add_le (1 + f i) (-f i)
  · simpa [add_comm] using norm_add_le (f i) 1

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