English
If f: ℤ → M has suitable Multipliable halves on positive and negative indices, then the bilateral product over all integers equals the product of the positive part, the central term f(0), and the negative part.
Русский
Если f: ℤ → M такова, что суммы по положительным и по отрицательным индексам сходятся, то двустороннее произведение по всем целым числам равно произведению по положительным индексам, f(0) и произведению по отрицательным индексам.
LaTeX
$$$$\\prod' n : \\mathbb{Z}, f(n) = (\\prod' n : \\mathbb{N}, f(n+1)) \\cdot f(0) \\cdot (\\prod' n : \\mathbb{N}, f(-n-1)).$$$$
Lean4
theorem tendsto_atTop_of_pos [Field α] [LinearOrder α] [IsStrictOrderedRing α] [TopologicalSpace α] [OrderTopology α]
{f : ℕ → α} (hf : Summable f⁻¹) (hf' : ∀ n, 0 < f n) : Tendsto f atTop atTop :=
inv_inv f ▸ Filter.Tendsto.inv_tendsto_nhdsGT_zero <|
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hf.tendsto_atTop_zero <|
Eventually.of_forall fun _ ↦ inv_pos.2 (hf' _)
