The block family of an integer packing

Given multiplicities k S : ℕ (S : Finset ι), the block family is indexed by Σ S : Finset ι, Fin (k S) with block map b ↦ b.1: the set S occurs k S times. It is the list of blocks used in the proof of the packing bound (Lemma 6.5 of the paper).

• card_blocks : the number of blocks containing i is ∑_{S ∋ i} k S;
• sum_blocks : a sum over the family of a function of the block is ∑_S k S * g S.

theorem AaronsonAmbainis.Pack.card_blocks {ι : Type} [Fintype ι] [DecidableEq ι] (k : Finset ι → ℕ) (i : ι) : {b : (S : Finset ι) × Fin (k S) | i ∈ b.fst}.card = ∑ S : Finset ι with i ∈ S, k S

The number of blocks of the family Σ S, Fin (k S) which contain i.

theorem AaronsonAmbainis.Pack.sum_blocks {ι : Type} [Fintype ι] (k : Finset ι → ℕ) (g : Finset ι → ℝ) : ∑ b : (S : Finset ι) × Fin (k S), g b.fst = ∑ S : Finset ι, ↑(k S) * g S

A sum over the family Σ S, Fin (k S) of a function of the block.