English
For a family of finite sets t(i) indexed by i in ι, and f(i,·) a function on each t(i), the product over i of the sum over elements b in t(i) of f(i,b) equals the sum over all p in the product set of the t(i) of the product over i of f(i, p(i)).
Русский
Для семейства конечных множеств t(i) и функций f(i,b) имеем тождество произведения по i от сумм по b∈t(i) равное сумме по всем функциям p который выбирают элемент из каждого t(i) от произведения по i f(i, p(i)).
LaTeX
$$$\\prod_{i} \\left( \\sum_{b\\in t(i)} f(i,b) \\right) = \\sum_{p\\in \\prod_i t(i)} \\prod_{i} f(i, p(i))$$$
Lean4
/-- The product over a sum can be written as a sum over the product of sets, `Finset.Pi`.
`Finset.prod_univ_sum` is an alternative statement when the product is over `univ`. -/
theorem prod_sum {κ : ι → Type*} (s : Finset ι) (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → R) :
∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f x.1 (p x.1 x.2) := by
classical
induction s using Finset.induction with
| empty => simp
| insert a s ha
ih =>
have h₁ :
∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) :=
by
intro x _ y _ h
simp only [disjoint_iff_ne, mem_image]
rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
have : Pi.cons s a x p₂ a (mem_insert_self _ _) = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
rw [Pi.cons_same, Pi.cons_same] at this
exact h this
rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
refine sum_congr rfl fun b _ => ?_
have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ := fun p₁ _ p₂ _ eq =>
Pi.cons_injective ha eq
rw [sum_image h₂, mul_sum]
refine sum_congr rfl fun g _ => ?_
rw [attach_insert, prod_insert, prod_image]
· simp only [Pi.cons_same]
congr with ⟨v, hv⟩
congr
exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
· exact fun _ _ _ _ => Subtype.eq ∘ Subtype.mk.inj
·
simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and, Subtype.exists, exists_prop, exists_eq_right] using
ha
