The packing bound before the limit

scaled_bound: from the block inequality, for a fractional packing κ and every natural number M ≥ 1, M² ∑_S κ_S |f x - f (x^S)| ≤ d² (π M + 2)² + ∑_S |f x - f (x^S)|. This is the inequality M² Λ ≤ d² (π M + 2)² + C₀ in the proof of the packing bound (Lemma 6.5 of the paper).

Proof: N = M², k S = ⌊N κ S⌋₊, block family Σ S, Fin (k S), m = ⌈π M / 2⌉₊.

theorem AaronsonAmbainis.Pack.card_blocks_le {ι : Type} [Fintype ι] [DecidableEq ι] (κ : Finset ι → ℝ) (hκ : ∀ (S : Finset ι), 0 ≤ κ S) (hpack : ∀ (i : ι), ∑ S : Finset ι with i ∈ S, κ S ≤ 1) (N : ℕ) (i : ι) : {b : (S : Finset ι) × Fin ⌊↑N * κ S⌋₊ | i ∈ b.fst}.card ≤ N

For k S = ⌊N κ S⌋₊ and a fractional packing κ, every coordinate lies in at most N blocks of the family Σ S, Fin (k S).

theorem AaronsonAmbainis.Pack.scaled_bound (hB : BlockInequality) (ι : Type) [Fintype ι] [DecidableEq ι] (d : ℕ) (f : Cube ι → ℝ) (hf : ∀ (x : Cube ι), |f x| ≤ 1) (hd : HasDegreeLE f d) (x : Cube ι) (κ : Finset ι → ℝ) (hκ : ∀ (S : Finset ι), 0 ≤ κ S) (hpack : ∀ (i : ι), ∑ S : Finset ι with i ∈ S, κ S ≤ 1) (M : ℕ) (hM : 0 < M) : ↑M ^ 2 * ∑ S : Finset ι, κ S * |f x - f (flipSet x S)| ≤ ↑d ^ 2 * (Real.pi * ↑M + 2) ^ 2 + ∑ S : Finset ι, |f x - f (flipSet x S)|

The packing bound before the limit, from the block inequality with N = M ^ 2 and m = ⌈π M / 2⌉₊.