Integer binomial gap estimate

Blueprint node C02: with 2 ≤ d, 2 ≤ q and 8 * d ^ 2 ≤ r ≤ q, writing T = r * (q - 1) - 1 and U = q * (r - 1) + d * (q - 1), one has T ≤ U, U - T ≤ d * q, and r * Nat.choose (U + d) d ≤ (r + 4 * d ^ 2) * Nat.choose (T + d) d. For 1 ≤ k ≤ d one also has Nat.choose (T + k) k ≤ q ^ k * Nat.choose (r + k - 1) k.

theorem Nikodym.LowerBound.T_le_U {d q r : ℕ} (hd : 2 ≤ d) (hq : 2 ≤ q) (hr : 8 * d ^ 2 ≤ r) : r * (q - 1) - 1 ≤ q * (r - 1) + d * (q - 1)

Blueprint C02: T ≤ U.

theorem Nikodym.LowerBound.U_sub_T_le {d q r : ℕ} (hd : 2 ≤ d) (hq : 2 ≤ q) (hr : 8 * d ^ 2 ≤ r) (hrq : r ≤ q) : q * (r - 1) + d * (q - 1) - (r * (q - 1) - 1) ≤ d * q

Blueprint C02: U - T ≤ d * q.

theorem Nikodym.LowerBound.r_mul_choose_le {d q r : ℕ} (hd : 2 ≤ d) (hq : 2 ≤ q) (hr : 8 * d ^ 2 ≤ r) (hrq : r ≤ q) : r * (q * (r - 1) + d * (q - 1) + d).choose d ≤ (r + 4 * d ^ 2) * (r * (q - 1) - 1 + d).choose d

Blueprint C02: r * Nat.choose (U + d) d ≤ (r + 4 * d ^ 2) * Nat.choose (T + d) d.

theorem Nikodym.LowerBound.choose_T_le {d q r : ℕ} (hd : 2 ≤ d) (hq : 2 ≤ q) (hr : 8 * d ^ 2 ≤ r) {k : ℕ} : (r * (q - 1) - 1 + k).choose k ≤ q ^ k * (r + k - 1).choose k

Blueprint C02: Nat.choose (T + k) k ≤ q ^ k * Nat.choose (r + k - 1) k.