English
Under a subset condition h𝒜, the sum of collapses over u.powerset equals the sum over 𝒜; i.e., the compressed sums match the original sums.
Русский
При условии подмножества h𝒜 сумма collapses по u.powerset равна сумме по 𝒜.
LaTeX
$$∑_{s∈u.powerset} collapse 𝒜 a f s = ∑_{s∈𝒜} f s$$
Lean4
theorem sum_collapse (h𝒜 : 𝒜 ⊆ (insert a u).powerset) (hu : a ∉ u) :
∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ 𝒜, f s :=
by
calc
_ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ u.powerset.image (insert a) ∩ 𝒜, f s := ?_
_ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ ((insert a u).powerset \ u.powerset) ∩ 𝒜, f s := ?_
_ = ∑ s ∈ 𝒜, f s := ?_
· rw [← Finset.sum_ite_mem, ← Finset.sum_ite_mem, sum_image, ← sum_add_distrib]
· exact sum_congr rfl fun s hs ↦ collapse_eq (notMem_mono (mem_powerset.1 hs) hu) _ _
· exact (insert_erase_invOn.2.injOn).mono fun s hs ↦ notMem_mono (mem_powerset.1 hs) hu
· congr with s
simp only [mem_image, mem_powerset, mem_sdiff, subset_insert_iff]
refine ⟨?_, fun h ↦ ⟨_, h.1, ?_⟩⟩
· rintro ⟨s, hs, rfl⟩
exact ⟨subset_insert_iff.1 <| insert_subset_insert _ hs, fun h ↦ hu <| h <| mem_insert_self _ _⟩
· rw [insert_erase (erase_ne_self.1 fun hs ↦ ?_)]
rw [hs] at h
exact h.2 h.1
·
rw [← sum_union (disjoint_sdiff_self_right.mono inf_le_left inf_le_left), ← union_inter_distrib_right,
union_sdiff_of_subset (powerset_mono.2 <| subset_insert _ _), inter_eq_right.2 h𝒜]
