English
Let d: 𝕜 → ℤ have finite support. Then the function obtained by taking the finite product over u of (· − u)^{d(u)} is the same as the function x ↦ ∏ᶠ u, (x − u)^{d(u)}; i.e., the evaluation at x commutes with the finite product over the finite support of d.
Русский
Пусть d: 𝕜 → ℤ имеет конечную опору. Тогда функция, заданная конечным произведением по всем u из опоры d: (· − u)^{d(u)}, совпадает с функцией x ↦ ∏ᶠ u, (x − u)^{d(u)}; т.е. разложение по x фиксируется при конечном произведении по ограниченной поддержке d.
LaTeX
$$$ \left( \prod_{u \in \operatorname{supp}(d)} (\cdot - u)^{d(u)} \right) = \left( x \mapsto \prod_{u \in \operatorname{supp}(d)} (x - u)^{d(u)} \right)$$$
Lean4
/-- Helper Lemma: If the support of `d` is finite, then evaluation of functions commutes with finprod,
and the function `∏ᶠ u, (· - u) ^ d u` equals `fun x ↦ ∏ᶠ u, (x - u) ^ d u`.
-/
theorem finprod_eq_fun {d : 𝕜 → ℤ} (h : d.support.Finite) : (∏ᶠ u, (· - u) ^ d u) = fun x ↦ ∏ᶠ u, (x - u) ^ d u :=
by
ext x
rw [finprod_eq_prod_of_mulSupport_subset (s := h.toFinset), finprod_eq_prod_of_mulSupport_subset (s := h.toFinset)]
· simp
· intro u
contrapose
simp_all
· simp [mulSupport d]
