Summing a single contributing shift in a supported family

theorem MagnitudeConjecture.sum_supported_single_shift {ι : Type u} [Fintype ι] {α : Type v} [DecidableEq α] (F : ι → Finset α) (s : α) (hs : ∀ (i : ι), s ∈ F i) (w : ι → ℕ) : (∑ a : (i : ι) × ↥(F i), if ↑a.snd = s then w a.fst else 0) = ∑ i : ι, w i

If a prescribed shift belongs to every fiber, summing a weight supported at that shift retains one copy of each label's weight.

theorem MagnitudeConjecture.sum_eq_of_supported_single_shift {ι : Type u} [Fintype ι] {α : Type v} [DecidableEq α] (F : ι → Finset α) (s : α) (hs : ∀ (i : ι), s ∈ F i) (w : ι → ℕ) (f : (i : ι) × ↥(F i) → ℕ) (hf : ∀ (a : (i : ι) × ↥(F i)), f a = if ↑a.snd = s then w a.fst else 0) : ∑ a : (i : ι) × ↥(F i), f a = ∑ i : ι, w i

Apply the single-shift sum to any pointwise identified weight.