English
If f(n) = f(−n) for all n and f is Multipliable, then ∏' n f(n) = f(0) · (∏' n≥1 f(n))^2.
Русский
Если f(−n) = f(n) и f умножимо, то произведение по всем целым числам равно f(0) умножить на квадрат т-произведения по положительным n.
LaTeX
$$$\\displaystyle \\bigl(\\forall n, f(-n)=f(n)\\bigr) \\land \\text{Multipliable}(f) \\Rightarrow \\prod'_{n} f(n) = f(0) \\cdot \\bigl(\\prod'_{n\\ge1} f(n)\\bigr)^2$$$
Lean4
@[to_additive tsum_int_eq_zero_add_two_mul_tsum_pnat]
theorem tprod_int_eq_zero_mul_tprod_pnat_sq [UniformSpace G] [IsUniformGroup G] [CompleteSpace G] [T2Space G]
{f : ℤ → G} (hf : ∀ n : ℤ, f (-n) = f n) (hf2 : Multipliable f) : ∏' n, f n = f 0 * (∏' n : ℕ+, f n) ^ 2 :=
by
have hf3 : Multipliable fun n : ℕ ↦ f n := (multipliable_int_iff_multipliable_nat_and_neg.mp hf2).1
have hf4 : Multipliable fun n : ℕ+ ↦ f n := by
rwa [multipliable_pnat_iff_multipliable_succ (f := (f ·)), multipliable_nat_add_iff 1 (f := (f ·))]
have := tprod_nat_mul_neg hf2
rw [← tprod_zero_pnat_eq_tprod_nat (by simpa [hf] using hf3.mul hf3), mul_comm _ (f 0)] at this
simp only [hf, Nat.cast_zero, mul_assoc, mul_right_inj] at this
rw [← this, mul_right_inj, hf4.tprod_mul hf4, sq]
