A square-root bound for the middle band

The elementary estimate (3m + 1) * centralBinom(m)^2 ≤ 16^m is enough to bound the middle binomial coefficient by 2^(2m+1) / sqrt(2m+1). No asymptotic estimate or Stirling formula is required.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.exceptional_card_le (m d : ℕ) : Nat.card (ExceptionalAtom m d) ≤ 2 * d * (2 * m + 1).choose m

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.centralBinom_sq_bound (m : ℕ) : (3 * ↑m + 1) * ↑m.centralBinom ^ 2 ≤ 16 ^ m

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.middle_choose_sq_bound (m : ℕ) : (2 * ↑m + 1) * ↑((2 * m + 1).choose m) ^ 2 ≤ (2 ^ (2 * m + 1)) ^ 2

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.middle_choose_le (m : ℕ) : ↑((2 * m + 1).choose m) ≤ 2 ^ (2 * m + 1) / √(2 * ↑m + 1)

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.exceptional_fraction_le (m d : ℕ) : ↑(Nat.card (ExceptionalAtom m d)) / 2 ^ (2 * m + 1) ≤ 2 * ↑d / √(2 * ↑m + 1)

The fraction of exceptional block generators is at most 2d / sqrt(2m+1).