Quelle  IMO2019_Q4.thy

(*
  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²"
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²"
    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²" by (rule rhs_less)
  also have "n² = 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 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 split_def
          del: Set.filter_eq 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