Arithmetic for the expander counting bound

Four elementary estimates, all in ℕ, which together turn the permutation count of PermCount into a bound small enough to survive a union bound over all vertex sets.

• A single binomial term is at most the whole binomial sum: C(s,t) 2^{s-t} ≤ 3^s.
• Descending factorials compare like powers: descFactorial s k · n^k ≤ s^k · descFactorial n k when s ≤ n — this is (s/n)^k in disguise, and it is where the smallness of a set of at most half the vertices enters.
• descFactorial n k · (n-k)! = n!, so the count is a fraction of n!.
• C(n,s) s^s ≤ 3^s n^s, the usual (e n / s)^s bound with e replaced by the integer 3. Its one analytic ingredient is (1 + 1/m)^m ≤ e < 3.

Main results

• Complexity.choose_mul_two_pow_le
• Complexity.descFactorial_mul_pow_le
• Complexity.descFactorial_mul_factorial_sub
• Complexity.choose_mul_pow_self_le

theorem Complexity.choose_mul_two_pow_le (s t : ℕ) (ht : t ≤ s) : s.choose t * 2 ^ (s - t) ≤ 3 ^ s

One term of a binomial sum.

theorem Complexity.descFactorial_mul_pow_le {s n : ℕ} (hsn : s ≤ n) (k : ℕ) : s.descFactorial k * n ^ k ≤ s ^ k * n.descFactorial k

Descending factorials compare like powers.

theorem Complexity.descFactorial_mul_factorial_sub {n k : ℕ} (hk : k ≤ n) : n.descFactorial k * (n - k).factorial = n.factorial

The descending factorial is a fraction of the factorial.

The (3 n / s)^s bound

theorem Complexity.pow_self_le_three_pow_mul_factorial (s : ℕ) : s ^ s ≤ 3 ^ s * s.factorial

s^s ≤ 3^s s!, the integer form of s! ≥ (s/e)^s.

theorem Complexity.choose_mul_pow_self_le (n s : ℕ) : n.choose s * s ^ s ≤ 3 ^ s * n ^ s

The (3 n / s)^s bound on a binomial coefficient.

The per-set estimate

theorem Complexity.two_pow_three_pow_le {s k : ℕ} (h9 : 9 * s ≤ 10 * k) : 2 ^ (2 * s) * 3 ^ (31 * s) ≤ 2 ^ (60 * k)

The numeric heart: 2^{2s} 3^{31s} ≤ 2^{60k} whenever 9 s ≤ 10 k.

theorem Complexity.key_estimate {n s k B : ℕ} (hs : 1 ≤ s) (hsn : 2 * s ≤ n) (h9 : 9 * s ≤ 10 * k) (hB : B * 2 ^ k * n ^ k ≤ 3 ^ s * s ^ k * n.factorial) : 2 ^ s * (n.choose s * B ^ 30) ≤ n.factorial ^ 30

The estimate for one vertex set, with the permutation count abstracted. The hypothesis is what PermCount supplies, in the form descFactorial and choose bounds put it; the conclusion leaves a factor 2^s of room for the union bound over all sets of size s.

theorem Complexity.count_bound {n s t : ℕ} (hsn : s ≤ n) (hts : t ≤ s) (hkn : s - t ≤ n) : s.choose t * s.descFactorial (s - t) * (n - (s - t)).factorial * 2 ^ (s - t) * n ^ (s - t) ≤ 3 ^ s * s ^ (s - t) * n.factorial

The counting hypothesis of key_estimate, as PermCount produces it.