English
A sequence of partial products converges (Cauchy) iff for every neighborhood of 1 there exists a finite set beyond which all tail products lie in that neighborhood.
Русский
Послідовность неполных произведений сходится (критерий Коши) тогда и только тогда, когда для любого окрестности 1 существует конечное множество после которого все хвостовые произведения попадают в эту окрестность.
LaTeX
$$$(\text{CauchySeq} \; \{\prod_{b\in s} f(b)\}) \iff \forall e \in \mathcal{N}(1), \exists s, \forall t, \text{Disjoint}(t,s) \Rightarrow \prod_{b\in t} f(b) \in e.$$$
Lean4
@[to_additive]
theorem cauchySeq_finset_iff_prod_vanishing :
(CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b) ↔
∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∏ b ∈ t, f b) ∈ e :=
by
classical
simp only [CauchySeq, cauchy_map_iff, prod_atTop_atTop_eq, uniformity_eq_comap_nhds_one α, tendsto_comap_iff,
Function.comp_def, atTop_neBot, true_and]
rw [tendsto_atTop']
constructor
· intro h e he
obtain ⟨⟨s₁, s₂⟩, h⟩ := h e he
use s₁ ∪ s₂
intro t ht
specialize h (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t) ⟨le_sup_left, le_sup_of_le_left le_sup_right⟩
simpa only [Finset.prod_union ht.symm, mul_div_cancel_left] using h
· rintro h e he
rcases exists_nhds_split_inv he with ⟨d, hd, hde⟩
rcases h d hd with ⟨s, h⟩
use (s, s)
rintro ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩
have : ((∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b) = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b := by
rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]
simp only [this]
exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)
