Kummer formulas for central binomial coefficients

Kummer's digit-sum formula is specialized to Nat.centralBinom. The resulting bridge turns digit and carry estimates into divisibility statements.

theorem GKPCarry.sub_one_mul_padicValNat_centralBinom (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (p - 1) * padicValNat p n.centralBinom = 2 * (p.digits n).sum - (p.digits (2 * n)).sum

Kummer's digit-sum formula specialized to central binomial coefficients.

theorem GKPCarry.pow_dvd_centralBinom_of_digit_excess {p n e : ℕ} [hp : Fact (Nat.Prime p)] (h : (p - 1) * e ≤ 2 * (p.digits n).sum - (p.digits (2 * n)).sum) : p ^ e ∣ n.centralBinom

A lower bound on Kummer's digit excess gives divisibility by a prime power.

theorem GKPCarry.two_mul_padicValNat_three_centralBinom (n : ℕ) : 2 * padicValNat 3 n.centralBinom = 2 * (Nat.digits 3 n).sum - (Nat.digits 3 (2 * n)).sum

The ternary specialization of the central-binomial digit formula.