English
For a fixed b and under suitable convergence hypotheses (LeAtTop, LeBot, etc.), the tprod of f over β equals f(b) times the tprod over β of the function that equals f(x) when x ≠ b and 1 when x = b. This is a version for a commutative monoid.
Русский
При подходящих условиях сходимости (LeAtTop и т.д.) т-продукт f по β равен f(b) умножить на т-продукт по β от функции, равной f(x) при x ≠ b и 1 при x = b. Это версия для коммутативного моноида.
LaTeX
$$$[DecidableEq\\ β]\\ [L.LeAtTop] [L.NeBot] \\ \\{f:\\beta\\to\\alpha\\} (b:\\beta)\\ (hf: Multipliable (update\\ f\\ b\\ 1)\\ L) : \\\\ \\prod'[L] x, f x = f b * \\prod'[L] x, \\; ite(x=b) 1 (f x)$$$
Lean4
/-- Version of `tprod_eq_mul_tprod_ite` for `CommMonoid` rather than `CommGroup`.
Requires a different convergence assumption involving `Function.update`. -/
@[to_additive /-- Version of `tsum_eq_add_tsum_ite` for `AddCommMonoid` rather than `AddCommGroup`.
Requires a different convergence assumption involving `Function.update`. -/
]
protected theorem tprod_eq_mul_tprod_ite' [DecidableEq β] [L.LeAtTop] [L.NeBot] {f : β → α} (b : β)
(hf : Multipliable (update f b 1) L) : ∏'[L] x, f x = f b * ∏'[L] x, ite (x = b) 1 (f x) :=
calc
∏'[L] x, f x = ∏'[L] x, (ite (x = b) (f x) 1 * update f b 1 x) :=
tprod_congr fun n ↦ by split_ifs with h <;> simp [update_apply, h]
_ = (∏'[L] x, ite (x = b) (f x) 1) * ∏'[L] x, update f b 1 x :=
(Multipliable.tprod_mul ⟨ite (b = b) (f b) 1, hasProd_single b (fun _ hb ↦ if_neg hb) L⟩ hf)
_ = ite (b = b) (f b) 1 * ∏'[L] x, update f b 1 x := by
congr
exact tprod_eq_mulSingle b fun b' hb' ↦ if_neg hb'
_ = f b * ∏'[L] x, ite (x = b) 1 (f x) := by simp only [update, if_true, eq_rec_constant, dite_eq_ite]
