Theory IMO2019_Q4
section ‹Q4›
theory IMO2019_Q4
imports "Prime_Distribution_Elementary.More_Dirichlet_Misc"
begin
text ‹
Find all pairs ‹(k, n)› of positive integers such that $k! = \prod_{i=0}^{n-1} (2^n - 2^i)$.
›
subsection ‹Auxiliary facts›
lemma Sigma_insert: "Sigma (insert x A) f = (λy. (x, y)) ` f x ∪ Sigma A f"
by auto
lemma atLeastAtMost_nat_numeral:
"{(m::nat)..numeral k} =
(if m ≤ numeral k then insert (numeral k) {m..pred_numeral k} else {})"
by (auto simp: numeral_eq_Suc)
lemma greaterThanAtMost_nat_numeral:
"{(m::nat)<..numeral k} =
(if m < numeral k then insert (numeral k) {m<..pred_numeral k} else {})"
by (auto simp: numeral_eq_Suc)
lemma fact_ge_power:
fixes c :: nat
assumes "fact n0 ≥ c ^ n0" "c ≤ n0 + 1"
assumes "n ≥ n0"
shows "fact n ≥ c ^ n"
using assms(3,1,2)
proof (induction n rule: dec_induct)
case (step n)
have "c * c ^ n ≤ Suc n * fact n"
using step by (intro mult_mono) auto
thus ?case by simp
qed auto
lemma prime_multiplicity_prime:
fixes p q :: "'a :: factorial_semiring"
assumes "prime p" "prime q"
shows "multiplicity p q = (if p = q then 1 else 0)"
using assms by (auto simp: prime_multiplicity_other)
text ‹
We use Legendre's identity from the library. One could easily prove the property in question
without the library, but it probably still saves a few lines.
@{const legendre_aux} (related to Legendre's identity) is the multiplicity of a given prime
in the prime factorisation of ‹n!›.
›
lemma multiplicity_prime_fact:
fixes p :: nat
assumes "prime p"
shows "multiplicity p (fact n) = legendre_aux 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 ‹
The following are simple and trivial lower and upper bounds for @{const legendre_aux}:
›
lemma legendre_aux_ge:
assumes "prime p" "k ≥ 1"
shows "legendre_aux k p ≥ nat ⌊k / p⌋"
proof (cases "k ≥ p")
case True
have "(∑m∈{1}. nat ⌊k / real p ^ m⌋) ≤ (∑m | 0 < m ∧ real p ^ m ≤ k. nat ⌊k / real p ^ m⌋)"
using True finite_sum_legendre_aux[of p] assms by (intro sum_mono2) auto
with assms True show ?thesis by (simp add: legendre_aux_def)
next
case False
with assms have "k / p < 1" by (simp add: field_simps)
hence "nat ⌊k / p⌋ = 0" by simp
with False show ?thesis
by (simp add: legendre_aux_eq_0)
qed
lemma legendre_aux_less:
assumes "prime p" "k ≥ 1"
shows "legendre_aux k p < k / (p - 1)"
proof -
have "(λm. (k / p) * (1 / p) ^ m) sums ((k / p) * (1 / (1 - 1 / p)))"
using assms prime_gt_1_nat[of p] by (intro sums_mult geometric_sums) (auto simp: field_simps)
hence sums: "(λm. k / p ^ Suc m) sums (k / (p - 1))"
using assms prime_gt_1_nat[of p] by (simp add: field_simps of_nat_diff)
have "real (legendre_aux k p) = (∑m∈{0<..nat ⌊log (real p) k⌋}. of_int ⌊k / real p ^ m⌋)"
using assms by (simp add: legendre_aux_altdef1)
also have "… = (∑m<nat ⌊log (real p) k⌋. of_int ⌊k / real p ^ Suc m⌋)"
by (intro sum.reindex_bij_witness[of _ Suc "λi. i - 1"]) (auto simp flip: power_Suc)
also have "… ≤ (∑m<nat ⌊log (real p) k⌋. k / real p ^ Suc m)"
by (intro sum_mono) auto
also have "… < (∑m. k / real p ^ Suc m)"
using sums assms prime_gt_1_nat[of p]
by (intro sum_less_suminf) (auto simp: sums_iff intro!: divide_pos_pos)
also have "… = k / (p - 1)"
using sums by (simp add: sums_iff)
finally show ?thesis
using assms prime_gt_1_nat[of p] by (simp add: of_nat_diff)
qed
subsection ‹Main result›
text ‹
Now we move on to the main result: We fix two numbers ‹n› and ‹k› with the property
in question and derive facts from that.
The triangle number $T = n(n+1)/2$ is of particular importance here, so we introduce an
abbreviation for it.
›
context
fixes k n :: nat and rhs T :: nat
defines "rhs ≡ (∏i<n. 2 ^ n - 2 ^ i)"
defines "T ≡ (n * (n - 1)) div 2"
assumes pos: "k > 0" "n > 0"
assumes k_n: "fact k = rhs"
begin
text ‹
We can rewrite the right-hand side into a more convenient form:
›
lemma rhs_altdef: "rhs = 2 ^ T * (∏i=1..n. 2 ^ i - 1)"
proof -
have "rhs = (∏i<n. 2 ^ i * (2 ^ (n - i) - 1))"
by (simp add: rhs_def algebra_simps flip: power_add)
also have "… = 2 ^ (∑i<n. i) * (∏i<n. 2 ^ (n - i) - 1)"
by (simp add: prod.distrib power_sum)
also have "(∑i<n. i) = T"
unfolding T_def using Sum_Ico_nat[of 0 n] by (simp add: atLeast0LessThan)
also have "(∏i<n. 2 ^ (n - i) - 1) = (∏i=1..n. 2 ^ i - 1)"
by (rule prod.reindex_bij_witness[of _ "λi. n - i" "λi. n - i"]) auto
finally show ?thesis .
qed
text ‹
The multiplicity of 2 in the prime factorisation of the right-hand side is precisely ‹T›.
›
lemma multiplicity_2_rhs [simp]: "multiplicity 2 rhs = T"
proof -
have nz: "2 ^ i - 1 ≠ (0 :: nat)" if "i ≥ 1" for i
proof -
from ‹i ≥ 1› have "2 ^ 0 < (2 ^ i :: nat)"
by (intro power_strict_increasing) auto
thus ?thesis by simp
qed
have "multiplicity 2 rhs = T + multiplicity 2 (∏i=1..n. 2 ^ i - 1 :: nat)"
using nz by (simp add: rhs_altdef prime_elem_multiplicity_mult_distrib)
also have "multiplicity 2 (∏i=1..n. 2 ^ i - 1 :: nat) = 0"
by (intro not_dvd_imp_multiplicity_0) (auto simp: prime_dvd_prod_iff)
finally show ?thesis by simp
qed
text ‹
From Legendre's identities and the associated bounds, it can easily be seen that
‹⌊k/2⌋ ≤ T < k›:
›
lemma k_gt_T: "k > T"
proof -
have "T = multiplicity 2 rhs"
by simp
also have "rhs = fact k"
by (simp add: k_n)
also have "multiplicity 2 (fact k :: nat) = legendre_aux k 2"
by (simp add: multiplicity_prime_fact)
also have "… < k"
using legendre_aux_less[of 2 k] pos by simp
finally show ?thesis .
qed
lemma T_ge_half_k: "T ≥ k div 2"
proof -
have "k div 2 ≤ legendre_aux k 2"
using legendre_aux_ge[of 2 k] pos by simp linarith?
also have "… = multiplicity 2 (fact k :: nat)"
by (simp add: multiplicity_prime_fact)
also have "… = T" by (simp add: k_n)
finally show "T ≥ k div 2" .
qed
text ‹
It can also be seen fairly easily that the right-hand side is strictly smaller than $2^{n^2}$:
›
lemma rhs_less: "rhs < 2 ^ n⇧2"
proof -
have "rhs = 2 ^ T * (∏i=1..n. 2 ^ i - 1)"
by (simp add: rhs_altdef)
also have "(∏i=1..n. 2 ^ i - 1 :: nat) < (∏i=1..n. 2 ^ i)"
using pos by (intro prod_mono_strict[of 1]) auto
also have "… = (∏i=0..<n. 2 * 2 ^ i)"
by (intro prod.reindex_bij_witness[of _ Suc "λi. i - 1"]) (auto simp flip: power_Suc)
also have "… = 2 ^ n * 2 ^ (∑i=0..<n. i)"
by (simp add: power_sum prod.distrib)
also have "(∑i=0..<n. i) = T"
unfolding T_def by (simp add: Sum_Ico_nat)
also have "2 ^ T * (2 ^ n * 2 ^ T :: nat) = 2 ^ (2 * T + n)"
by (simp flip: power_add power_Suc add: algebra_simps)
also have "2 * T + n = n ^ 2"
by (cases "even n") (auto simp: T_def algebra_simps power2_eq_square)
finally show "rhs < 2 ^ n⇧2"
by simp
qed
text ‹
It is clear that $2^{n^2} \leq 8^T$ and that $8^T < T!$ if $T$ is sufficiently big.
In this case, `sufficiently big' means ‹T ≥ 20› and thereby ‹n ≥ 7›. We can therefore
conclude that ‹n› must be less than 7.
›
lemma n_less_7: "n < 7"
proof (rule ccontr)
assume "¬n < 7"
hence "n ≥ 7" by simp
have "T ≥ (7 * 6) div 2"
unfolding T_def using ‹n ≥ 7› by (intro div_le_mono mult_mono) auto
hence "T ≥ 21" by simp
from ‹n ≥ 7› have "(n * 2) div 2 ≤ T"
unfolding T_def by (intro div_le_mono) auto
hence "T ≥ n" by simp
from ‹T ≥ 21› have "sqrt (2 * pi * T) * (T / exp 1) ^ T ≤ fact T"
using fact_bounds[of T] by simp
have "fact T ≤ (fact k :: nat)"
using k_gt_T by (intro fact_mono) (auto simp: T_def)
also have "… = rhs" by fact
also have "rhs < 2 ^ n⇧2" by (rule rhs_less)
also have "n⇧2 = 2 * T + n"
by (cases "even n") (auto simp: T_def algebra_simps power2_eq_square)
also have "… ≤ 3 * T"
using ‹T ≥ n› by (simp add: T_def)
also have "2 ^ (3 * T) = (8 ^ T :: nat)"
by (simp add: power_mult)
finally have "fact T < (8 ^ T :: nat)"
by simp
moreover have "fact T ≥ (8 ^ T :: nat)"
by (rule fact_ge_power[of _ 20]) (use ‹T ≥ 21› in ‹auto simp: fact_numeral›)
ultimately show False by simp
qed
text ‹
We now only have 6 values for ‹n› to check. Together with the bounds that we obtained on ‹k›,
this only leaves a few combinations of ‹n› and ‹k› to check, and we do precisely that
and find that ‹n = k = 1› and ‹n = 2, k = 3› are the only possible combinations.
›
lemma n_k_in_set: "(n, k) ∈ {(1, 1), (2, 3)}"
proof -
define T' where "T' = (λn :: nat. n * (n - 1) div 2)"
define A :: "(nat × nat) set" where "A = (SIGMA n:{1..6}. {T' n<..2 * T' n + 1})"
define P where "P = (λ(n, k). fact k = (∏i<n. 2 ^ n - 2 ^ i :: nat))"
have [simp]: "{0<..Suc 0} = {1}" by auto
have "(n, k) ∈ Set.filter P A"
using k_n pos T_ge_half_k k_gt_T n_less_7
by (auto simp: A_def T'_def T_def Set.filter_def P_def rhs_def)
also have "Set.filter P A = {(1, 1), (2, 3)}"
by (simp add: P_def Set_filter_insert A_def atMost_nat_numeral atMost_Suc T'_def Sigma_insert
greaterThanAtMost_nat_numeral atLeastAtMost_nat_numeral lessThan_nat_numeral fact_numeral
cong: if_weak_cong)
finally show ?thesis .
qed
end
text ‹
Using this, deriving the final result is now trivial:
›
theorem "{(n, k). n > 0 ∧ k > 0 ∧ fact k = (∏i<n. 2 ^ n - 2 ^ i :: nat)} = {(1, 1), (2, 3)}"
(is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs" using n_k_in_set by blast
show "?rhs ⊆ ?lhs" by (auto simp: fact_numeral lessThan_nat_numeral)
qed
end