English
One factor can be extracted from a factorized rational function: the whole product equals (· − u0)^{d(u0)} times the product with d updated at u0 to zero.
Русский
Из процесса произведения можно вытащить один фактор: произведение равно (\cdot − u0)^{d(u0)} умноженное на произведение с обновлением d, где d(u0) заменено на 0.
LaTeX
$$$ \prod_{u} (\cdot - u)^{d(u)} = (\cdot - u_0)^{d(u_0)} \cdot \prod_{u} (\cdot - u)^{\operatorname{update}(d, u_0, 0)(u)}$$$
Lean4
/-- Helper Lemma for Computations: Extract one factor out of a factorized rational function.
-/
theorem extractFactor {d : 𝕜 → ℤ} (u₀ : 𝕜) (hd : d.support.Finite) :
(∏ᶠ u, (· - u) ^ d u) = ((· - u₀) ^ d u₀) * (∏ᶠ u, (· - u) ^ (update d u₀ 0 u)) :=
by
by_cases h₁d : d u₀ = 0
· simp [← eq_update_self_iff.2 h₁d, h₁d]
· have : (fun u ↦ (fun x ↦ x - u) ^ d u).mulSupport ⊆ hd.toFinset := by simp [mulSupport]
rw [finprod_eq_prod_of_mulSupport_subset _ this]
have : u₀ ∈ hd.toFinset := by simp_all
rw [← Finset.mul_prod_erase hd.toFinset _ this]
congr 1
have : (fun u ↦ (· - u) ^ (update d u₀ 0 u)).mulSupport ⊆ hd.toFinset.erase u₀ :=
by
rw [mulSupport]
intro x hx
by_cases h₁x : x = u₀ <;> simp_all
simp_all [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
