The two layers surrounding the majority threshold

The largest binomial coefficient is at least 2^n/(n+1), and its upper neighbor is at least half as large. This gives a logarithmic entropy deficit for both boundary layers, for even as well as odd input sizes.

theorem Complexity.BooleanAnalysis.le_majorityDeficitBound_internal (n : ℕ) : 128 ≤ majorityDeficitBound n

theorem Complexity.BooleanAnalysis.middle_choose_bound_internal (n : ℕ) : 2 ^ n ≤ (n + 1) * n.choose (n / 2)

theorem Complexity.BooleanAnalysis.next_middle_choose_bound_internal {n : ℕ} (hn : 2 ≤ n) : n.choose (n / 2) ≤ 2 * n.choose (n / 2 + 1)

theorem Complexity.BooleanAnalysis.weightLayer_deficit_internal {n r : ℕ} (hr : r ≤ n) (hcard : 2 ^ n ≤ 2 * (n + 1) * n.choose r) : (weightLayer n r).Nonempty ∧ uniformDeficit (weightLayer n r) ≤ majorityDeficitBound n

theorem Complexity.BooleanAnalysis.majority_layers_deficit_internal {n : ℕ} (hn : 2 ≤ n) : ((weightLayer n (n / 2)).Nonempty ∧ uniformDeficit (weightLayer n (n / 2)) ≤ majorityDeficitBound n) ∧ (weightLayer n (n / 2 + 1)).Nonempty ∧ uniformDeficit (weightLayer n (n / 2 + 1)) ≤ majorityDeficitBound n

theorem Complexity.BooleanAnalysis.popCount_update_true_internal {n : ℕ} (x : Fin n → Bool) (i : Fin n) (hi : x i = false) : popCount (Function.update x i true) = popCount x + 1

theorem Complexity.BooleanAnalysis.popCount_update_false_internal {n : ℕ} (x : Fin n → Bool) (i : Fin n) (hi : x i = true) : popCount (Function.update x i false) + 1 = popCount x