English
For prime p, and hnb: log_p(n+k) < b, the p-adic exponent of (n+k choose k) equals the cardinality of {i ∈ Ico(1,b) | p^i ≤ k % p^i + n % p^i}.
Русский
Для простого p и hnb: log_p(n+k) < b, показатель p в (n+k) над k равен кардиналу множества {i ∈ Ico(1,b) | p^i ≤ k mod p^i + n mod p^i}.
LaTeX
$$$ (n+k)\\choose k .factorization\\ p = \\#\\{ i ∈ \\mathrm{Ico}(1,b) \\mid p^i ≤ k \\% p^i + n \\% p^i \\}. $$$
Lean4
theorem factorization_choose_of_lt_three_mul (hp' : p ≠ 2) (hk : p ≤ k) (hk' : p ≤ n - k) (hn : n < 3 * p) :
(choose n k).factorization p = 0 := by
rcases em' p.Prime with hp | hp
· exact factorization_eq_zero_of_non_prime (choose n k) hp
rcases lt_or_ge n k with hnk | hkn
· simp [choose_eq_zero_of_lt hnk]
simp only [factorization_choose hp hkn (Nat.lt_add_one _), card_eq_zero, filter_eq_empty_iff, mem_Ico, not_le,
and_imp]
intro i hi₁ hi
rcases eq_or_lt_of_le hi₁ with (rfl | hi)
· rw [pow_one, ← add_lt_add_iff_left (2 * p), ← succ_mul, two_mul, add_add_add_comm]
exact
lt_of_le_of_lt
(add_le_add (add_le_add_right (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk)) (k % p))
(add_le_add_right (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk')) ((n - k) % p)))
(by rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn])
· replace hn : n < p ^ i := by
have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm
calc
n < 3 * p := hn
_ ≤ p * p := (mul_le_mul_right' this p)
_ = p ^ 2 := (sq p).symm
_ ≤ p ^ i := pow_right_mono₀ hp.one_lt.le hi
rwa [mod_eq_of_lt (lt_of_le_of_lt hkn hn), mod_eq_of_lt (lt_of_le_of_lt tsub_le_self hn), add_tsub_cancel_of_le hkn]
