The Chebyshev gate parameters

For N = M ^ 2 (the bound for the number of blocks through a coordinate) and m = ⌈π M / 2⌉₊, this file proves the three numerical facts used in the proof of the packing bound (Lemma 6.5 of the paper):

• gate_pos : 0 < m (for M ≥ 1);
• gate_cos : N (1 - cos (π / m)) ≤ 2 (for M ≥ 1);
• gate_sq : 4 m² ≤ (π M + 2)².

theorem AaronsonAmbainis.Pack.gate_pos (M : ℕ) (hM : 0 < M) : 0 < ⌈Real.pi * ↑M / 2⌉₊

m = ⌈π M / 2⌉₊ is positive when M is.

theorem AaronsonAmbainis.Pack.gate_cos (M : ℕ) (hM : 0 < M) : ↑(M ^ 2) * (1 - Real.cos (Real.pi / ↑⌈Real.pi * ↑M / 2⌉₊)) ≤ 2

The hypothesis N (1 - cos (π / m)) ≤ 2 of the block inequality for N = M ^ 2 and m = ⌈π M / 2⌉₊.

theorem AaronsonAmbainis.Pack.gate_sq (M : ℕ) : 4 * ↑⌈Real.pi * ↑M / 2⌉₊ ^ 2 ≤ (Real.pi * ↑M + 2) ^ 2

4 m² ≤ (π M + 2)² for m = ⌈π M / 2⌉₊.