English
If sequences u and v of elements of a seminormed commutative group E agree eventually from index N onward, and the partial products of v form a Cauchy sequence, then the partial products of u also form a Cauchy sequence.
Русский
Если последовательности u_n и v_n в E совпадают после некоторого N, и частичные произведения v_n образуют последовательность Cauchy, то и частичные произведения u_n образуют Cauchy.
LaTeX
$$$\\forall u,v:E^{\\mathbb{N}}, \\; (\\forall n\\ge N, u_n=v_n) \\land CauchySeq(\\lambda n. \\prod_{k=0}^n v_k) \\Rightarrow CauchySeq(\\lambda n. \\prod_{k=0}^n u_k)$$$
Lean4
@[to_additive]
theorem cauchySeq_prod_of_eventually_eq {u v : ℕ → E} {N : ℕ} (huv : ∀ n ≥ N, u n = v n)
(hv : CauchySeq fun n => ∏ k ∈ range (n + 1), v k) : CauchySeq fun n => ∏ k ∈ range (n + 1), u k :=
by
let d : ℕ → E := fun n => ∏ k ∈ range (n + 1), u k / v k
rw [show (fun n => ∏ k ∈ range (n + 1), u k) = d * fun n => ∏ k ∈ range (n + 1), v k by ext n; simp [d]]
suffices ∀ n ≥ N, d n = d N from (tendsto_atTop_of_eventually_const this).cauchySeq.mul hv
intro n hn
dsimp [d]
rw [eventually_constant_prod _ (add_le_add_right hn 1)]
intro m hm
simp [huv m (le_of_lt hm)]
