English
Given HasProd for the nonnegative index, and HasProd for the shifted negative indices, one obtains HasProd for the full ℤ-indexed sequence via HasProd.of_nat_of_neg_add_one.
Русский
Для HasProd по неотрицательным и по сдвинутым отрицательным частям получаем HasProd полной ℤ‑индексированной последовательности.
LaTeX
$$$\text{HasProd}(f) = \text{HasProd}(f_{\ge0}) \cdot \text{HasProd}(f_{<0})$$$
Lean4
@[to_additive]
theorem nat_mul_neg {f : ℤ → M} (hf : HasProd f m) : HasProd (fun n : ℕ ↦ f n * f (-n)) (m * f 0) := by
-- Note this is much easier to prove if you assume more about the target space, but we have to
-- work hard to prove it under the very minimal assumptions here.
apply (hf.mul (hasProd_ite_eq (0 : ℤ) (f 0))).hasProd_of_prod_eq fun u ↦ ?_
refine ⟨u.image Int.natAbs, fun v' hv' ↦ ?_⟩
let u1 := v'.image fun x : ℕ ↦ (x : ℤ)
let u2 := v'.image fun x : ℕ ↦ -(x : ℤ)
have A : u ⊆ u1 ∪ u2 := by
intro x hx
simp only [u1, u2, mem_union, mem_image]
rcases le_total 0 x with (h'x | h'x)
· refine Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
simp only [Int.natCast_natAbs, abs_eq_self, h'x]
· refine Or.inr ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
simp only [abs_of_nonpos h'x, Int.natCast_natAbs, neg_neg]
exact
⟨_, A,
calc
(∏ x ∈ u1 ∪ u2, (f x * if x = 0 then f 0 else 1)) = (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x :=
by
rw [prod_mul_distrib]
congr 1
refine (prod_subset_one_on_sdiff inter_subset_union ?_ ?_).symm
· intro x hx
suffices x ≠ 0 by simp only [this, if_false]
rintro rfl
simp only [mem_sdiff, mem_union, mem_image, Nat.cast_eq_zero, exists_eq_right, neg_eq_zero, or_self,
mem_inter, and_self, and_not_self, u1, u2] at hx
· intro x hx
simp only [u1, u2, mem_inter, mem_image] at hx
suffices x = 0 by simp only [this, if_true]
cutsat
_ = (∏ x ∈ u1, f x) * ∏ x ∈ u2, f x := prod_union_inter
_ = (∏ b ∈ v', f b) * ∏ b ∈ v', f (-b) := by simp [u1, u2]
_ = ∏ b ∈ v', (f b * f (-b)) := prod_mul_distrib.symm⟩
