English
If ∑‖f_i‖ is summable, then there exists a finite s₂ such that for all t with Disjoint t and s₂, ‖∏_{i∈t} (1+f_i)−1‖ < ε for any ε>0.
Русский
Если ∑‖f_i‖ суммируема, существует конечный набор s₂, чтобы для любых t раздельных, выполнялось ‖∏_{i∈t} (1+f_i)−1‖ < ε.
LaTeX
$$$\exists s_2, \forall t, \text{Disjoint}(t,s_2) \Rightarrow \left\|\prod_{i\in t} (1+f_i) - 1\right\| < \varepsilon$$$
Lean4
theorem prod_vanishing_of_summable_norm (hf : Summable fun i ↦ ‖f i‖) {ε : ℝ} (hε : 0 < ε) :
∃ s₂, ∀ t, Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε :=
by
suffices ∃ s, ∀ t, Disjoint t s → Real.exp (∑ i ∈ t, ‖f i‖) - 1 < ε from
this.imp fun s hs t ht ↦ (t.norm_prod_one_add_sub_one_le _).trans_lt (hs t ht)
suffices {x | Real.exp x - 1 < ε} ∈ 𝓝 0 from hf.vanishing this
let f (x) := Real.exp x - 1
have : Set.Iio ε ∈ nhds (f 0) := by simpa [f] using Iio_mem_nhds hε
exact ContinuousAt.preimage_mem_nhds (by fun_prop) this
