English
For any finite set s and functions f,g: i ↦ R, the product over s of (f(i) + g(i)) equals the sum over all t ⊆ s of (t.prod f) times ((s \\ t).prod g).
Русский
Для любого конечного множества s и функций f,g: s → R,\nпроизведение по i∈s (f(i)+g(i)) равно сумме по всем подмножествам t⊆s от (t.prod f) (s\\t).prod g.
LaTeX
$$$\\prod_{i\\in s} (f(i) + g(i)) = \\sum_{t\\in s.powerset} \\left( \\prod_{i\\in t} f(i) \\right) \\left( \\prod_{i\\in s\\setminus t} g(i) \\right)$$$
Lean4
/-- The product of `f a + g a` over all of `s` is the sum over the powerset of `s` of the product of
`f` over a subset `t` times the product of `g` over the complement of `t` -/
theorem prod_add (f g : ι → R) (s : Finset ι) :
∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i := by
classical
calc
∏ i ∈ s, (f i + g i) = ∏ i ∈ s, ∑ p ∈ ({ True, False } : Finset Prop), if p then f i else g i := by simp
_ =
∑ p ∈ (s.pi fun _ => { True, False } : Finset (∀ a ∈ s, Prop)),
∏ a ∈ s.attach, if p a.1 a.2 then f a.1 else g a.1 :=
(prod_sum _ _ _)
_ = ∑ t ∈ s.powerset, (∏ a ∈ t, f a) * ∏ a ∈ s \ t, g a :=
sum_bij' (fun f _ ↦ {a ∈ s | ∃ h : a ∈ s, f a h}) (fun t _ a _ => a ∈ t) (by simp) (by simp [Classical.em])
(by simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
(by simp_rw [Finset.ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto)
(fun a _ ↦
by
simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk, Subtype.map_coe, id_eq,
prod_attach]
congr 2 with x
simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
tauto)
