English
Alternate version: if log f_i converges and eventually f_i > 0, then ∏ f_i converges.
Русский
Альтернативная версия: если log f_i сходится и в конце f_i > 0, то ∏ f_i сходится.
LaTeX
$$$\prod_{i} f_i \text{ converges}$$$
Lean4
/-- Alternate version of `Real.multipliable_of_summable_log` assuming only that positivity holds
eventually. -/
theorem multipliable_of_summable_log' (hfn : ∀ᶠ i in cofinite, 0 < f i) (hf : Summable fun i ↦ log (f i)) :
Multipliable f :=
by
have : Summable fun i ↦ log (if 0 < f i then f i else 1) :=
by
apply hf.congr_cofinite
filter_upwards [hfn] with i hi using by simp [hi]
have : Multipliable fun i ↦ if 0 < f i then f i else 1 :=
by
refine multipliable_of_summable_log (fun i ↦ ?_) this
split_ifs with h <;> simp [h]
refine this.congr_cofinite₀ (fun i ↦ ?_) ?_
· split_ifs with h <;> simp [h, ne_of_gt]
· filter_upwards [hfn] with i hi using by simp [hi]
