English
For a group-valued sequence f: ℕ → G, shifting the index by k alters the HasProd by multiplication with the finite product ∏_{i<k} f(i); equivalently, HasProd (f(n+k)) g is equivalent to HasProd f (g ∙ ∏_{i<k} f(i)).
Русский
Для последовательности f: ℕ → G сдвиг индекса на k умножает целевой HasProd на произведение первых k значений; эквивалентно HasProd (f(n+k)) g ↔ HasProd f (g · ∏_{i<k} f(i)).
LaTeX
$$$\text{HasProd}(f(n+k))\, g \;\iff\; \text{HasProd}(f)\left(g \cdot \prod_{i=0}^{k-1} f(i)\right)$$$
Lean4
@[to_additive]
theorem cauchySeq_finset_iff_nat_tprod_vanishing {f : ℕ → G} :
(CauchySeq fun s : Finset ℕ ↦ ∏ n ∈ s, f n) ↔ ∀ e ∈ 𝓝 (1 : G), ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e :=
by
refine cauchySeq_finset_iff_tprod_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
· obtain ⟨s, hs⟩ := vanish e he
refine ⟨if h : s.Nonempty then s.max' h + 1 else 0, fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩
split_ifs at ht with h
· exact fun m hmt hms ↦ (s.le_max' _ hms).not_gt (Nat.succ_le_iff.mp <| ht hmt)
· exact fun _ _ hs ↦ h ⟨_, hs⟩
· obtain ⟨N, hN⟩ := vanish e he
exact ⟨range N, fun t ht ↦ hN _ fun n hnt ↦ le_of_not_gt fun h ↦ Set.disjoint_left.mp ht hnt (mem_range.mpr h)⟩
