English
For any f: ℕ → G, the tail products ∏' k, f(k+i) converge to the identity as i → ∞, i.e., Tendsto (fun i ↦ ∏' k, f(k+i)) atTop (𝓝 1) (with multipliability omitted if appropriate).
Русский
Для любой f: ℕ → G хвостовые произведения сходятся к единице при i → ∞, т.е. Tendsto (fun i ↦ ∏' k, f(k+i)) к 1.
LaTeX
$$$\operatorname{Tendsto}_{i \to \mathrm{atTop}}\left(\prod_{k\ge0} f(k+i)\right) = 1$$$
Lean4
/-- For `f : ℕ → G`, the product `∏' k, f (k + i)` tends to one. This does not require a
multipliability assumption on `f`, as otherwise all such products are one. -/
@[to_additive /-- For `f : ℕ → G`, the sum `∑' k, f (k + i)` tends to zero. This does not require a
summability assumption on `f`, as otherwise all such sums are zero. -/
]
theorem tendsto_prod_nat_add [T2Space G] (f : ℕ → G) : Tendsto (fun i ↦ ∏' k, f (k + i)) atTop (𝓝 1) :=
by
by_cases hf : Multipliable f
· have h₀ : (fun i ↦ (∏' i, f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' k : ℕ, f (k + i) :=
by
ext1 i
rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]
have h₁ : Tendsto (fun _ : ℕ ↦ ∏' i, f i) atTop (𝓝 (∏' i, f i)) := tendsto_const_nhds
simpa only [h₀, div_self'] using Tendsto.div' h₁ hf.hasProd.tendsto_prod_nat
· refine tendsto_const_nhds.congr fun n ↦ (tprod_eq_one_of_not_multipliable ?_).symm
rwa [multipliable_nat_add_iff n]
