(* File: IMO2019_Q4.thy Author: Manuel Eberl, TU München *) 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› (* TODO: Move stuff from this section? *) 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!›. › (* TODO: Move? *) 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) 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