English
In a complete space, if ∑‖f_i‖ converges, then ∏′ (1+f_i) converges to a finite limit.
Русский
В полной пространстве, если ∑‖f_i‖ сходится, то бесконечное произведение ∏′ (1+f_i) сходится к конечному пределу.
LaTeX
$$$\prod'_{i} (1 + f_i) \text{ converges}$$$
Lean4
/-- In a complete normed ring, `∏' i, (1 + f i)` is convergent if the sum of real numbers
`∑' i, ‖f i‖` is convergent. -/
theorem multipliable_one_add_of_summable [CompleteSpace R] (hf : Summable fun i ↦ ‖f i‖) :
Multipliable fun i ↦ (1 + f i) := by
classical
refine CompleteSpace.complete <| Metric.cauchy_iff.mpr ⟨by infer_instance, fun ε hε ↦ ?_⟩
obtain ⟨r₁, hr₁, s₁, hs₁⟩ := (multipliable_norm_one_add_of_summable_norm hf).eventually_bounded_finset_prod
obtain ⟨s₂, hs₂⟩ := prod_vanishing_of_summable_norm hf (show 0 < ε / (2 * r₁) by positivity)
simp only [unconditional, Filter.mem_map, mem_atTop_sets, ge_iff_le, le_eq_subset, Set.mem_preimage]
let s := s₁ ∪ s₂
refine ⟨Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ⟨s, fun b hb ↦ ?_⟩, ?_⟩
· rw [← union_sdiff_of_subset hb, prod_union sdiff_disjoint.symm, Metric.mem_ball, dist_eq_norm_sub, ← mul_sub_one,
show ε / 2 = r₁ * (ε / (2 * r₁)) by field_simp]
apply (norm_mul_le _ _).trans_lt
refine lt_of_le_of_lt (b := r₁ * ‖∏ x ∈ b \ s, (1 + f x) - 1‖) ?_ ?_
· refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
exact (Finset.norm_prod_le _ _).trans (hs₁ _ subset_union_left)
· refine mul_lt_mul_of_pos_left (hs₂ _ ?_) hr₁
simp [s, sdiff_union_distrib, disjoint_iff_inter_eq_empty]
· intro x hx y hy
exact (dist_triangle_right _ _ (∏ i ∈ s, (1 + f i))).trans_lt (add_halves ε ▸ add_lt_add hx hy)
