Theory Legendre_Factorial_Valuation
theory Legendre_Factorial_Valuation
imports Rational_Padic_Valuations "Prime_Number_Theorem.Prime_Counting_Functions"
begin
section ‹Legendre's formula for the ‹p›-adic valuation of
‹n!››
text ‹‹v⇩p(n!) = ∑⇩a⇩≥⇩1 ⌊n /
p⇧a⌋›, derived from the Legendre identity of the AFP entry
Prime\_Number\_Theorem, in the two forms used later: with the @{text legendre_aux}
function of that entry and with an explicit finite range of summation.›
text ‹Legendre's formula @{text "v_p(n!) = ∑_{a≥1} ⌊n/p^a⌋"};
exists as
@{text IMO2019_Q4.multiplicity_prime_fact} with @{text legendre_aux}.›
lemma legendre_fact:
fixes p :: nat
assumes "prime p"
shows "multiplicity p (fact n) = legendre_aux (real n) p"
proof (cases "p ≤ n")
case True
have "fact n = (∏p | prime p ∧ p ≤ n. p ^ legendre_aux n p)"
using legendre_identity'[of "real n"] by simp
also have "multiplicity p … = (∑q | prime q ∧
q ≤ n. multiplicity p (q ^ legendre_aux n q))"
using assms by (subst prime_elem_multiplicity_prod_distrib) auto
also have "… = (∑q∈{p}. legendre_aux n q)"
using assms ‹p ≤ n› prime_multiplicity_other[of p]
by (intro sum.mono_neutral_cong_right)
(auto simp: prime_elem_multiplicity_power_distrib prime_multiplicity_prime split: if_splits)
finally show ?thesis by simp
next
case False
hence "multiplicity p (fact n) = 0"
using assms by (intro not_dvd_imp_multiplicity_0) (auto simp: prime_dvd_fact_iff)
moreover from False have "legendre_aux (real n) p = 0"
by (intro legendre_aux_eq_0) auto
ultimately show ?thesis by simp
qed
text ‹Legendre's formula with any upper limit @{text "B ≥ n"} on the sum.›
lemma legendre_sum:
assumes "prime p" "n ≤ B"
shows "multiplicity p (fact n) = (∑ a = 1..B. n div p ^ a)"
proof -
have p2: "2 ≤ p" using prime_ge_2_nat[OF assms(1)] .
have "multiplicity p (fact n) = (∑ m | 0 < m ∧
real (p ^ m) ≤ real n. nat ⌊real n / real (p ^ m)⌋)"
using legendre_fact[OF assms(1), of n] assms(1) by (simp add: legendre_aux_def)
also have "… = (∑ m | 0 < m ∧ p ^ m ≤ n. n div p ^ m)"
proof (rule sum.cong)
show "{m. 0 < m ∧ real (p ^ m) ≤ real n} = {m. 0 < m ∧ p ^ m ≤ n}"
by (simp only: of_nat_le_iff)
next
fix m show "nat ⌊real n / real (p ^ m)⌋ = n div p ^ m"
by (simp only: floor_divide_of_nat_eq nat_int)
qed
also have "… = (∑ a = 1..B. n div p ^ a)"
proof (rule sum.mono_neutral_left)
show "{m. 0 < m ∧ p ^ m ≤ n} ⊆ {1..B}"
proof
fix m assume m: "m ∈ {m. 0 < m ∧ p ^ m ≤ n}"
have "m < 2 ^ m" by (rule less_exp)
also have "(2::nat) ^ m ≤ p ^ m" using p2 by (rule power_mono) simp
finally show "m ∈ {1..B}" using m assms(2) by auto
qed
next
show "∀i ∈ {1..B} - {m. 0 < m ∧ p ^ m ≤ n}. n div p ^ i = 0"
proof
fix i assume "i ∈ {1..B} - {m. 0 < m ∧ p ^ m ≤ n}"
hence "n < p ^ i" by auto
thus "n div p ^ i = 0" by (rule div_less)
qed
qed simp
finally show ?thesis .
qed
end