From 966e0cf0685c9cedf8a3283ac69eef4d5f2eaca2 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 25 Jan 2023 20:47:30 +0000 Subject: [PATCH] refactor(number_theory/primorial): split the proof, golf it (#18238) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add `nat.prime.dvd_choose`, delete less general `dvd_choose_of_middling_prime`. * Add `primorial_pos`, `primorial_add`, `primorial_add_dvd`, and `primorial_add_le`. * Golf some proofs. Here is a proof of `dvd_choose_of_middling_prime` based on `nat.prime.dvd_choose`: ```lean open nat lemma dvd_choose_of_middling_prime (p : ℕ) (is_prime : nat.prime p) (m : ℕ) (p_big : m + 1 < p) (p_small : p ≤ 2 * m + 1) : p ∣ choose (2 * m + 1) (m + 1) := is_prime.dvd_choose p_big (by simpa [two_mul] using p_big.le) p_small ``` Forward-ported in leanprover-community/mathlib4#1770 --- src/algebra/char_p/basic.lean | 3 +- src/data/nat/choose/dvd.lean | 31 ++-- src/number_theory/primorial.lean | 135 ++++++------------ .../polynomial/eisenstein/is_integral.lean | 7 +- 4 files changed, 60 insertions(+), 116 deletions(-) diff --git a/src/algebra/char_p/basic.lean b/src/algebra/char_p/basic.lean index de1806499b205..600f16288cfe3 100644 --- a/src/algebra/char_p/basic.lean +++ b/src/algebra/char_p/basic.lean @@ -144,8 +144,7 @@ begin { intros b h1 h2, suffices : (p.choose b : R) = 0, { rw this, simp }, rw char_p.cast_eq_zero_iff R p, - refine nat.prime.dvd_choose_self (pos_iff_ne_zero.mpr h2) _ (fact.out _), - rwa ← finset.mem_range }, + exact nat.prime.dvd_choose_self (fact.out _) h2 (finset.mem_range.1 h1) }, { intro h1, contrapose! h1, rw finset.mem_range, diff --git a/src/data/nat/choose/dvd.lean b/src/data/nat/choose/dvd.lean index 11c3114090e97..3adae6d9f24aa 100644 --- a/src/data/nat/choose/dvd.lean +++ b/src/data/nat/choose/dvd.lean @@ -19,26 +19,23 @@ open_locale nat namespace prime -lemma dvd_choose_add {p a b : ℕ} (hap : a < p) (hbp : b < p) (h : p ≤ a + b) - (hp : prime p) : p ∣ choose (a + b) a := -have h₁ : p ∣ (a + b)!, from hp.dvd_factorial.2 h, -have h₂ : ¬p ∣ a!, from mt hp.dvd_factorial.1 (not_le_of_gt hap), -have h₃ : ¬p ∣ b!, from mt hp.dvd_factorial.1 (not_le_of_gt hbp), -by - rw [← choose_mul_factorial_mul_factorial (le.intro rfl), mul_assoc, hp.dvd_mul, hp.dvd_mul, - add_tsub_cancel_left a b] at h₁; - exact h₁.resolve_right (not_or_distrib.2 ⟨h₂, h₃⟩) - -lemma dvd_choose_self {p k : ℕ} (hk : 0 < k) (hkp : k < p) (hp : prime p) : - p ∣ choose p k := +lemma dvd_choose_add {p a b : ℕ} (hp : prime p) (hap : a < p) (hbp : b < p) (h : p ≤ a + b) : + p ∣ choose (a + b) a := begin - have r : k + (p - k) = p, - by rw [← add_tsub_assoc_of_le (nat.le_of_lt hkp) k, add_tsub_cancel_left], - have e : p ∣ choose (k + (p - k)) k, - by exact dvd_choose_add hkp (nat.sub_lt (hk.trans hkp) hk) (by rw r) hp, - rwa r at e, + have h₁ : p ∣ (a + b)!, from hp.dvd_factorial.2 h, + rw [← add_choose_mul_factorial_mul_factorial, ← choose_symm_add, hp.dvd_mul, hp.dvd_mul, + hp.dvd_factorial, hp.dvd_factorial] at h₁, + exact (h₁.resolve_right hbp.not_le).resolve_right hap.not_le end +lemma dvd_choose {p a b : ℕ} (hp : prime p) (ha : a < p) (hab : b - a < p) (h : p ≤ b) : + p ∣ choose b a := +have a + (b - a) = b := nat.add_sub_of_le (ha.le.trans h), +this ▸ hp.dvd_choose_add ha hab (this.symm ▸ h) + +lemma dvd_choose_self {p k : ℕ} (hp : prime p) (hk : k ≠ 0) (hkp : k < p) : p ∣ choose p k := +hp.dvd_choose hkp (nat.sub_lt ((zero_le _).trans_lt hkp) hk.bot_lt) le_rfl + end prime end nat diff --git a/src/number_theory/primorial.lean b/src/number_theory/primorial.lean index 9e8a6174d748d..f216faaed13a3 100644 --- a/src/number_theory/primorial.lean +++ b/src/number_theory/primorial.lean @@ -1,13 +1,13 @@ /- Copyright (c) 2020 Patrick Stevens. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Patrick Stevens +Authors: Patrick Stevens, Yury Kudryashov -/ import algebra.big_operators.associated import data.nat.choose.sum +import data.nat.choose.dvd import data.nat.parity import data.nat.prime -import tactic.ring_exp /-! # Primorial @@ -30,105 +30,54 @@ open_locale big_operators nat def primorial (n : ℕ) : ℕ := ∏ p in (filter nat.prime (range (n + 1))), p local notation x`#` := primorial x -lemma primorial_succ {n : ℕ} (n_big : 1 < n) (r : n % 2 = 1) : (n + 1)# = n# := +lemma primorial_pos (n : ℕ) : 0 < n# := +prod_pos $ λ p hp, (mem_filter.1 hp).2.pos + +lemma primorial_succ {n : ℕ} (hn1 : n ≠ 1) (hn : odd n) : (n + 1)# = n# := begin refine prod_congr _ (λ _ _, rfl), - rw [range_succ, filter_insert, if_neg (λ h, _)], - have two_dvd : 2 ∣ n + 1 := dvd_iff_mod_eq_zero.mpr (by rw [← mod_add_mod, r, mod_self]), - linarith [(h.dvd_iff_eq (nat.bit0_ne_one 1)).mp two_dvd], + rw [range_succ, filter_insert, if_neg (λ h, odd_iff_not_even.mp hn _)], + exact (h.even_sub_one $ mt succ.inj hn1) end -lemma dvd_choose_of_middling_prime (p : ℕ) (is_prime : nat.prime p) (m : ℕ) - (p_big : m + 1 < p) (p_small : p ≤ 2 * m + 1) : p ∣ choose (2 * m + 1) (m + 1) := +lemma primorial_add (m n : ℕ) : + (m + n)# = m# * ∏ p in filter nat.prime (Ico (m + 1) (m + n + 1)), p := begin - have m_size : m + 1 ≤ 2 * m + 1 := le_of_lt (lt_of_lt_of_le p_big p_small), - have s : ¬(p ∣ (m + 1)!), - { intros p_div_fact, - exact lt_le_antisymm p_big (is_prime.dvd_factorial.mp p_div_fact), }, - have t : ¬(p ∣ (2 * m + 1 - (m + 1))!), - { intros p_div_fact, - refine lt_le_antisymm (lt_of_succ_lt p_big) _, - convert is_prime.dvd_factorial.mp p_div_fact, - rw [two_mul, add_assoc, nat.add_sub_cancel] }, - have expanded : - choose (2 * m + 1) (m + 1) * (m + 1)! * (2 * m + 1 - (m + 1))! = (2 * m + 1)! := - @choose_mul_factorial_mul_factorial (2 * m + 1) (m + 1) m_size, - have p_div_big_fact : p ∣ (2 * m + 1)! := (prime.dvd_factorial is_prime).mpr p_small, - rw [←expanded, mul_assoc] at p_div_big_fact, - obtain p_div_choose | p_div_facts : p ∣ choose (2 * m + 1) (m + 1) ∨ p ∣ _! * _! := - (prime.dvd_mul is_prime).1 p_div_big_fact, - { exact p_div_choose, }, - cases (prime.dvd_mul is_prime).1 p_div_facts, - exacts [(s h).elim, (t h).elim], + rw [primorial, primorial, ← Ico_zero_eq_range, ← prod_union, ← filter_union, + Ico_union_Ico_eq_Ico], + exacts [zero_le _, add_le_add_right (nat.le_add_right _ _) _, + disjoint_filter_filter $ Ico_disjoint_Ico_consecutive _ _ _] end -lemma primorial_le_4_pow : ∀ (n : ℕ), n# ≤ 4 ^ n -| 0 := le_rfl -| 1 := le_of_inf_eq rfl -| (n + 2) := - match nat.mod_two_eq_zero_or_one (n + 1) with - | or.inl n_odd := - match nat.even_iff.2 n_odd with - | ⟨m, twice_m⟩ := - have recurse : m + 1 < n + 2 := by linarith, - begin - calc (n + 2)# - = ∏ i in filter nat.prime (range (2 * m + 2)), i : by simpa [two_mul, ←twice_m] - ... = ∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2) ∪ range (m + 2)), i : - begin - rw [range_eq_Ico, finset.union_comm, finset.Ico_union_Ico_eq_Ico], - { exact bot_le }, - { simpa only [add_le_add_iff_right, two_mul] using nat.le_add_left m m }, - end - ... = ∏ i in (filter nat.prime (finset.Ico (m + 2) (2 * m + 2)) - ∪ (filter nat.prime (range (m + 2)))), i : - by rw filter_union - ... = (∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2)), i) - * (∏ i in filter nat.prime (range (m + 2)), i) : - begin - apply finset.prod_union, - have disj : disjoint (finset.Ico (m + 2) (2 * m + 2)) (range (m + 2)), - { simp only [finset.disjoint_left, and_imp, finset.mem_Ico, not_lt, - finset.mem_range], - intros _ pr _, exact pr, }, - exact finset.disjoint_filter_filter disj, - end - ... ≤ (∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2)), i) * 4 ^ (m + 1) : - nat.mul_le_mul_left _ (primorial_le_4_pow (m + 1)) - ... ≤ (choose (2 * m + 1) (m + 1)) * 4 ^ (m + 1) : - begin - have s : ∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2)), - i ∣ choose (2 * m + 1) (m + 1), - { refine prod_primes_dvd (choose (2 * m + 1) (m + 1)) _ _, - { intros a, rw [finset.mem_filter, nat.prime_iff], apply and.right, }, - { intros a, rw finset.mem_filter, - intros pr, - rcases pr with ⟨ size, is_prime ⟩, - simp only [finset.mem_Ico] at size, - rcases size with ⟨ a_big , a_small ⟩, - exact dvd_choose_of_middling_prime a is_prime m a_big - (nat.lt_succ_iff.mp a_small), }, }, - have r : ∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2)), - i ≤ choose (2 * m + 1) (m + 1), - { refine @nat.le_of_dvd _ _ _ s, - exact @choose_pos (2 * m + 1) (m + 1) (by linarith), }, - exact nat.mul_le_mul_right _ r, - end - ... = (choose (2 * m + 1) m) * 4 ^ (m + 1) : by rw choose_symm_half m - ... ≤ 4 ^ m * 4 ^ (m + 1) : nat.mul_le_mul_right _ (choose_middle_le_pow m) - ... = 4 ^ (2 * m + 1) : by ring_exp - ... = 4 ^ (n + 2) : by rw [two_mul, ←twice_m], - end - end - | or.inr n_even := +lemma primorial_add_dvd {m n : ℕ} (h : n ≤ m) : (m + n)# ∣ m# * choose (m + n) m := +calc (m + n)# = m# * ∏ p in filter nat.prime (Ico (m + 1) (m + n + 1)), p : + primorial_add _ _ +... ∣ m# * choose (m + n) m : + mul_dvd_mul_left _ $ prod_primes_dvd _ (λ k hk, (mem_filter.1 hk).2.prime) $ λ p hp, begin - obtain one_lt_n | n_le_one : 1 < n + 1 ∨ n + 1 ≤ 1 := lt_or_le 1 (n + 1), - { rw primorial_succ one_lt_n n_even, - calc (n + 1)# - ≤ 4 ^ n.succ : primorial_le_4_pow (n + 1) - ... ≤ 4 ^ (n + 2) : pow_le_pow (by norm_num) (nat.le_succ _), }, - { have n_zero : n = 0 := eq_bot_iff.2 (succ_le_succ_iff.1 n_le_one), - norm_num [n_zero, primorial, range_succ, prod_filter, nat.not_prime_zero, nat.prime_two] }, + rw [mem_filter, mem_Ico] at hp, + exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1)) + (nat.lt_succ_iff.1 hp.1.2) end +lemma primorial_add_le {m n : ℕ} (h : n ≤ m) : (m + n)# ≤ m# * choose (m + n) m := +le_of_dvd (mul_pos (primorial_pos _) (choose_pos $ nat.le_add_right _ _)) (primorial_add_dvd h) + +lemma primorial_le_4_pow (n : ℕ) : n# ≤ 4 ^ n := +begin + induction n using nat.strong_induction_on with n ihn, + cases n, { refl }, + rcases n.even_or_odd with (⟨m, rfl⟩ | ho), + { rcases m.eq_zero_or_pos with rfl | hm, { dec_trivial }, + calc (m + m + 1)# = (m + 1 + m)# : by rw [add_right_comm] + ... ≤ (m + 1)# * choose (m + 1 + m) (m + 1) : primorial_add_le m.le_succ + ... = (m + 1)# * choose (2 * m + 1) m : by rw [choose_symm_add, two_mul, add_right_comm] + ... ≤ 4 ^ (m + 1) * 4 ^ m : + mul_le_mul' (ihn _ $ succ_lt_succ $ (lt_add_iff_pos_left _).2 hm) (choose_middle_le_pow _) + ... ≤ 4 ^ (m + m + 1) : by rw [← pow_add, add_right_comm] }, + { rcases decidable.eq_or_ne n 1 with rfl | hn, + { dec_trivial }, + { calc (n + 1)# = n# : primorial_succ hn ho + ... ≤ 4 ^ n : ihn n n.lt_succ_self + ... ≤ 4 ^ (n + 1) : pow_le_pow_of_le_right four_pos n.le_succ } } end diff --git a/src/ring_theory/polynomial/eisenstein/is_integral.lean b/src/ring_theory/polynomial/eisenstein/is_integral.lean index 9287f49e81052..79c85cb016f1a 100644 --- a/src/ring_theory/polynomial/eisenstein/is_integral.lean +++ b/src/ring_theory/polynomial/eisenstein/is_integral.lean @@ -54,10 +54,9 @@ begin rw [lcoeff_apply, ← C_eq_nat_cast, C_mul_X_pow_eq_monomial, coeff_monomial] }, rw [nat_degree_comp, show (X + 1 : ℤ[X]) = X + C 1, by simp, nat_degree_X_add_C, mul_one, nat_degree_cyclotomic, nat.totient_prime hp.out] at hi, - simp only [lt_of_lt_of_le hi (nat.sub_le _ _), sum_ite_eq', mem_range, - if_true, ideal.submodule_span_eq, ideal.mem_span_singleton], - exact int.coe_nat_dvd.2 - (nat.prime.dvd_choose_self (nat.succ_pos i) (lt_tsub_iff_right.1 hi) hp.out) }, + simp only [hi.trans_le (nat.sub_le _ _), sum_ite_eq', mem_range, if_true, + ideal.submodule_span_eq, ideal.mem_span_singleton, int.coe_nat_dvd], + exact hp.out.dvd_choose_self i.succ_ne_zero (lt_tsub_iff_right.1 hi) }, { rw [coeff_zero_eq_eval_zero, eval_comp, cyclotomic_prime, eval_add, eval_X, eval_one, zero_add, eval_geom_sum, one_geom_sum, ideal.submodule_span_eq, ideal.span_singleton_pow, ideal.mem_span_singleton],