tprod_one_add_ne_zero_of_summable

English

If each 1+f_i ≠ 0 and ∑‖f_i‖ converges, then ∏′ (1+f_i) ≠ 0.

Русский

Если каждый 1+f_i ≠ 0 and ∑‖f_i‖ сходится, то ∏′ (1+f_i) ≠ 0.

LaTeX

$$$\prod'_{i} (1 + f_i) \neq 0$$$

Lean4

theorem tprod_one_add_ne_zero_of_summable [CompleteSpace R] [NormMulClass R] (hf : ∀ i, 1 + f i ≠ 0)
    (hu : Summable (‖f ·‖)) : ∏' i : ι, (1 + f i) ≠ 0 :=
  by
  rw [← norm_ne_zero_iff, Multipliable.norm_tprod]
  · rw [← Real.rexp_tsum_eq_tprod (fun i ↦ norm_pos_iff.mpr <| hf i) hu.summable_log_norm_one_add]
    apply Real.exp_ne_zero
  · exact multipliable_one_add_of_summable hu

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