multipliable_norm_one_add_of_summable_norm

English

If ∑‖f_i‖ converges, then ∑‖1+f_i‖ is Multipliable, hence ∥1+f_i∥ is multipliable.

Русский

Если ∑‖f_i‖ сходится, то ∥1+f_i∥ является множителем (существует произведение).

LaTeX

$$$\text{Multipliable}( \|1+f_i\| )$$$

Lean4

theorem multipliable_norm_one_add_of_summable_norm (hf : Summable fun i ↦ ‖f i‖) : Multipliable fun i ↦ ‖1 + f i‖ :=
  by
  conv => enter [1, i]; rw [← sub_add_cancel ‖1 + f i‖ 1, add_comm]
  refine Real.multipliable_one_add_of_summable <| hf.of_norm_bounded (fun i ↦ ?_)
  simpa using abs_norm_sub_norm_le (1 + f i) 1

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