From the block inequality to the bound for fractional packings

AaronsonAmbainis.packingBound_of_block : BlockInequality → PackingBound: the packing bound (Lemma 6.5 of the paper) follows from the block inequality (Lemma 6.4). This file contains the limit M → ∞ (Pack.le_of_scaled); the inequality for a fixed M is Pack.scaled_bound in Pack/Scaled.lean.

theorem AaronsonAmbainis.Pack.le_of_scaled (L C : ℝ) (d : ℕ) (key : ∀ (M : ℕ), 0 < M → ↑M ^ 2 * L ≤ ↑d ^ 2 * (Real.pi * ↑M + 2) ^ 2 + C) : L ≤ Real.pi ^ 2 * ↑d ^ 2

The limit step: if M² L ≤ d² (π M + 2)² + C for every natural M ≥ 1, then L ≤ π² d².

theorem AaronsonAmbainis.packingBound_of_block : BlockInequality → PackingBound

The bound for fractional packings follows from the block inequality.