IMO 2019-4
import ring_theory.multiplicity algebra.big_operators tactic.default data.rat.basic | |
.two_adic_val_fact | |
/- two_adic_val_fact.lean is located here: | |
https://gist.githubusercontent.com/kbuzzard/4ca88f429bda4744fd038f7471ebfb67/raw/5fa02ec9f5f2b5edf5020cb20c44167a648e0514/two_adic_val_fact.lean | |
-/ | |
universe variables u v | |
open finset | |
lemma prod_nat_cast {α β} [comm_semiring β] (s : finset α) (f : α → ℕ) : | |
↑(s.prod f) = s.prod (λa, f a : α → β) := | |
(prod_hom _).symm | |
instance int.coe.is_monoid_hom : is_monoid_hom (coe : ℕ → ℤ) := | |
{ map_one := int.coe_nat_one, map_mul := int.coe_nat_mul } | |
lemma prod_nat_cast_int {α} (s : finset α) (f : α → ℕ) : | |
↑(s.prod f) = s.prod (λa, f a : α → ℤ) := | |
(prod_hom _).symm | |
lemma nat_prime_iff_prime (n : ℕ) : nat.prime n ↔ prime n := | |
nat.prime_iff_prime | |
lemma int.coe_nat_prime (n : ℕ) : prime (n : ℤ) ↔ prime n := | |
by { rw [← nat.prime_iff_prime_int, nat_prime_iff_prime] } | |
lemma ne_zero_of_prime {α} [comm_semiring α] {p : α} (hp : prime p) : p ≠ 0 := | |
hp.1 | |
lemma not_unit_of_prime {α} [comm_semiring α] {p : α} (hp : prime p) : ¬ is_unit p := | |
hp.2.1 | |
namespace nat | |
lemma monotone_fact : monotone fact := λ n m, fact_le | |
lemma fact_lt {n m : ℕ} (h0 : 0 < n) : n.fact < m.fact ↔ n < m := | |
begin | |
split; intro h, | |
{ rw [← not_le], intro hmn, apply not_le_of_lt h (fact_le hmn) }, | |
{ have : ∀(n : ℕ), 0 < n → n.fact < n.succ.fact, | |
{ intros k hk, rw [fact_succ, succ_mul, lt_add_iff_pos_left], | |
apply mul_pos hk (fact_pos k) }, | |
induction h generalizing h0, | |
{ exact this _ h0, }, | |
{ refine lt_trans (h_ih h0) (this _ _), exact lt_trans h0 (lt_of_succ_le h_a) }} | |
end | |
lemma one_lt_fact {n : ℕ} : 1 < n.fact ↔ 1 < n := | |
by { convert fact_lt _, refl, norm_num } | |
lemma fact_eq_one {n : ℕ} : n.fact = 1 ↔ n ≤ 1 := | |
begin | |
split; intro h, | |
{ rw [← not_lt, ← one_lt_fact, h], apply lt_irrefl }, | |
{ cases h with h h, refl, cases h, refl } | |
end | |
lemma fact_inj {n m : ℕ} (h0 : 1 < n.fact) : n.fact = m.fact ↔ n = m := | |
begin | |
split; intro h, | |
{ rcases lt_trichotomy n m with hnm|hnm|hnm, | |
{ exfalso, rw [← fact_lt, h] at hnm, exact lt_irrefl _ hnm, | |
rw [one_lt_fact] at h0, exact lt_trans (by norm_num) h0 }, | |
{ exact hnm }, | |
{ exfalso, rw [← fact_lt, h] at hnm, exact lt_irrefl _ hnm, | |
rw [h, one_lt_fact] at h0, exact lt_trans (by norm_num) h0 }}, | |
{ rw h } | |
end | |
/- The `n+1`-st triangle number is `n` more than the `n`-th triangle number -/ | |
lemma triangle_succ (n : ℕ) : (n + 1) * ((n + 1) - 1) / 2 = n * (n - 1) / 2 + n := | |
begin | |
rw [← add_mul_div_left, mul_comm 2 n, ← mul_add, nat.add_sub_cancel, mul_comm], | |
cases n; refl, norm_num | |
end | |
lemma reflect_lt {α β} [linear_order α] [preorder β] {f : α → β} (hf : monotone f) | |
{x x' : α} (h : f x < f x') : x < x' := | |
by { rw [← not_le], intro h', apply not_le_of_lt h, exact hf h' } | |
lemma ne_of_eq_monotone {α} [preorder α] {f : ℕ → α} (hf : monotone f) | |
(x x' : ℕ) {y : α} (h1 : f x < y) (h2 : y < f (x + 1)) : f x' ≠ y := | |
by { rintro rfl, apply not_le_of_lt (reflect_lt hf h1), exact le_of_lt_succ (reflect_lt hf h2) } | |
end nat | |
/- this is also true for a ordered commutative multiplicative monoid -/ | |
lemma prod_nonneg {α : Type u} {β : Type v} [decidable_eq α] [linear_ordered_comm_ring β] | |
{s : finset α} {f : α → β} (h0 : ∀(x ∈ s), 0 ≤ f x) : 0 ≤ s.prod f := | |
begin | |
induction s using finset.induction with a s has ih h, | |
{ simp [zero_le_one] }, | |
{ simp [has], apply mul_nonneg, apply h0 a (mem_insert_self a s), | |
exact ih (λ x H, h0 x (mem_insert_of_mem H)) } | |
end | |
/- this is also true for a ordered commutative multiplicative monoid -/ | |
lemma prod_pos {α : Type u} {β : Type v} [decidable_eq α] [linear_ordered_comm_ring β] | |
{s : finset α} {f : α → β} (h0 : ∀(x ∈ s), 0 < f x) : 0 < s.prod f := | |
begin | |
induction s using finset.induction with a s has ih h, | |
{ simp [zero_lt_one] }, | |
{ simp [has], apply mul_pos, apply h0 a (mem_insert_self a s), | |
exact ih (λ x H, h0 x (mem_insert_of_mem H)) } | |
end | |
/- this is also true for a ordered commutative multiplicative monoid -/ | |
lemma prod_le_prod {α : Type u} {β : Type v} [decidable_eq α] [linear_ordered_comm_ring β] | |
{s : finset α} {f g : α → β} (h0 : ∀(x ∈ s), 0 ≤ f x) (h1 : ∀(x ∈ s), f x ≤ g x) : | |
s.prod f ≤ s.prod g := | |
begin | |
induction s using finset.induction with a s has ih h, | |
{ simp }, | |
{ simp [has], apply mul_le_mul, | |
exact h1 a (mem_insert_self a s), | |
apply ih (λ x H, h0 _ _) (λ x H, h1 _ _); exact (mem_insert_of_mem H), | |
apply prod_nonneg (λ x H, h0 x (mem_insert_of_mem H)), | |
apply le_trans (h0 a (mem_insert_self a s)) (h1 a (mem_insert_self a s)) } | |
end | |
namespace roption | |
lemma some_ne_none {α} (x : α) : some x ≠ none := | |
by { intro h, change none.dom, rw [← h], trivial } | |
lemma ne_none_iff {α} {o : roption α} : o ≠ none ↔ ∃x, o = some x := | |
begin | |
split, | |
{ rw [ne, eq_none_iff], intro h, push_neg at h, cases h with x hx, use x, rwa [eq_some_iff] }, | |
{ rintro ⟨x, rfl⟩, apply some_ne_none } | |
end | |
end roption | |
namespace enat | |
open roption | |
instance : has_mul enat := ⟨λ x y, ⟨x.dom ∧ y.dom, λ h, get x h.1 * get y h.2⟩⟩ | |
instance : comm_monoid enat := | |
{ mul := (*), | |
one := (1), | |
mul_comm := λ x y, roption.ext' and.comm (λ _ _, mul_comm _ _), | |
one_mul := λ x, roption.ext' (true_and _) (λ _ _, one_mul _), | |
mul_one := λ x, roption.ext' (and_true _) (λ _ _, mul_one _), | |
mul_assoc := λ x y z, roption.ext' and.assoc (λ _ _, mul_assoc _ _ _) } | |
@[simp] lemma get_mul {x y : enat} (h : (x * y).dom) : get (x * y) h = x.get h.1 * y.get h.2 := rfl | |
protected lemma finset.sum {α : Type u} [decidable_eq α] (s : finset α) (f : α → ℕ) : | |
s.sum (λ x, (f x : enat)) = (s.sum f : ℕ) := | |
begin | |
induction s using finset.induction with a s has ih h, | |
{ simp }, | |
{ simp [has, ih] } | |
end | |
lemma top_eq_none : (⊤ : enat) = none := rfl | |
lemma ne_top_iff {x : enat} : x ≠ ⊤ ↔ ∃(n : ℕ), x = n := roption.ne_none_iff | |
lemma ne_top_of_lt {x y : enat} (h : x < y) : x ≠ ⊤ := | |
ne_of_lt $ lt_of_lt_of_le h lattice.le_top | |
protected lemma add_lt_add_right {x y z : enat} (h : x < y) (hz : z ≠ ⊤) : x + z < y + z := | |
begin | |
rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩, | |
rcases ne_top_iff.mp hz with ⟨k, rfl⟩, | |
induction y using enat.cases_on with n, | |
{ rw [top_add], apply_mod_cast coe_lt_top }, | |
norm_cast at h, apply_mod_cast add_lt_add_right h | |
end | |
protected lemma add_lt_add_iff_right {x y z : enat} (hz : z ≠ ⊤) : x + z < y + z ↔ x < y := | |
⟨lt_of_add_lt_add_right', λ h, enat.add_lt_add_right h hz⟩ | |
protected lemma add_lt_add_iff_left {x y z : enat} (hz : z ≠ ⊤) : z + x < z + y ↔ x < y := | |
by simpa using enat.add_lt_add_iff_right hz | |
protected lemma lt_add_iff_pos_right {x y : enat} (hx : x ≠ ⊤) : x < x + y ↔ 0 < y := | |
by { conv_rhs { rw [← enat.add_lt_add_iff_left hx] }, rw [add_zero] } | |
lemma lt_add_one {x : enat} (hx : x ≠ ⊤) : x < x + 1 := | |
by { rw [enat.lt_add_iff_pos_right hx], norm_cast, norm_num } | |
lemma le_of_lt_add_one {x y : enat} (h : x < y + 1) : x ≤ y := | |
begin | |
induction y using enat.cases_on with n, apply lattice.le_top, | |
rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩, | |
apply_mod_cast nat.le_of_lt_succ, apply_mod_cast h | |
end | |
lemma add_one_le_of_lt {x y : enat} (h : x < y) : x + 1 ≤ y := | |
begin | |
induction y using enat.cases_on with n, apply lattice.le_top, | |
rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩, | |
apply_mod_cast nat.succ_le_of_lt, apply_mod_cast h | |
end | |
lemma add_one_le_iff_lt {x y : enat} (hx : x ≠ ⊤) : x + 1 ≤ y ↔ x < y := | |
begin | |
split, swap, exact add_one_le_of_lt, | |
intro h, rcases ne_top_iff.mp hx with ⟨m, rfl⟩, | |
induction y using enat.cases_on with n, apply coe_lt_top, | |
apply_mod_cast nat.lt_of_succ_le, apply_mod_cast h | |
end | |
lemma lt_add_one_iff_lt {x y : enat} (hx : x ≠ ⊤) : x < y + 1 ↔ x ≤ y := | |
begin | |
split, exact le_of_lt_add_one, | |
intro h, rcases ne_top_iff.mp hx with ⟨m, rfl⟩, | |
induction y using enat.cases_on with n, { rw [top_add], apply coe_lt_top }, | |
apply_mod_cast nat.lt_succ_of_le, apply_mod_cast h | |
end | |
end enat | |
lemma pow_dvd_pow_iff {α} [integral_domain α] {x : α} {n m : ℕ} (h0 : x ≠ 0) (h1 : ¬ is_unit x) : | |
x ^ n ∣ x ^ m ↔ n ≤ m := | |
begin | |
split, | |
{ intro h, rw [← not_lt], intro hmn, apply h1, | |
have : x * x ^ m ∣ 1 * x ^ m, | |
{ rw [← pow_succ, one_mul], exact dvd_trans (pow_dvd_pow _ (nat.succ_le_of_lt hmn)) h }, | |
rwa [mul_dvd_mul_iff_right, ← is_unit_iff_dvd_one] at this, apply pow_ne_zero m h0 }, | |
{ apply pow_dvd_pow } | |
end | |
namespace multiplicity | |
section | |
variables {α : Type u} {β : Type v} [decidable_eq α] [integral_domain β] | |
[decidable_rel ((∣) : β → β → Prop)] | |
lemma finset.prod {p : β} (hp : prime p) (s : finset α) (f : α → β) : | |
multiplicity p (s.prod f) = s.sum (λ x, multiplicity p (f x)) := | |
begin | |
induction s using finset.induction with a s has ih h, | |
{ simp [one_right (not_unit_of_prime hp)] }, | |
{ simp [has, multiplicity.mul hp, ih] } | |
end | |
end | |
section | |
variables {α : Type u} [comm_semiring α] [decidable_rel ((∣) : α → α → Prop)] | |
lemma multiplicity_lt_iff_neg_dvd {a b : α} {k : ℕ} : | |
multiplicity a b < (k : enat) ↔ ¬ a ^ k ∣ b := | |
by { rw [pow_dvd_iff_le_multiplicity, not_le] } | |
end | |
section | |
variables {α : Type u} [integral_domain α] [decidable_rel ((∣) : α → α → Prop)] | |
lemma multiplicity_add_of_gt {p a b : α} (h : multiplicity p b < multiplicity p a) : | |
multiplicity p (a + b) = multiplicity p b := | |
begin | |
apply le_antisymm, | |
{ apply enat.le_of_lt_add_one, | |
cases enat.ne_top_iff.mp (enat.ne_top_of_lt h) with k hk, | |
rw [hk], rw_mod_cast [multiplicity_lt_iff_neg_dvd], intro h_dvd, | |
rw [← dvd_add_iff_right] at h_dvd, | |
apply multiplicity.is_greatest _ h_dvd, rw [hk], apply_mod_cast nat.lt_succ_self, | |
rw [pow_dvd_iff_le_multiplicity, enat.coe_add, ← hk], exact enat.add_one_le_of_lt h }, | |
{ convert min_le_multiplicity_add, rw [min_eq_right (le_of_lt h)] } | |
end | |
lemma multiplicity_sub_of_gt {p a b : α} (h : multiplicity p b < multiplicity p a) : | |
multiplicity p (a - b) = multiplicity p b := | |
by { rw [sub_eq_add_neg, multiplicity_add_of_gt]; rwa [multiplicity.neg] } | |
lemma multiplicity_add_eq_min {p a b : α} (h : multiplicity p a ≠ multiplicity p b) : | |
multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b) := | |
begin | |
rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with hab|hab|hab, | |
{ rw [add_comm, multiplicity_add_of_gt hab, min_eq_left], exact le_of_lt hab }, | |
{ contradiction }, | |
{ rw [multiplicity_add_of_gt hab, min_eq_right], exact le_of_lt hab}, | |
end | |
-- lemma multiplicity_pow {p a : α} (n : ℕ) (hp : prime p) : | |
-- multiplicity p (a ^ n) = multiplicity p a * n := | |
-- begin | |
-- sorry | |
-- end | |
lemma multiplicity_pow_self {p : α} (hu : ¬ is_unit p) (h0 : p ≠ 0) (n : ℕ) : | |
multiplicity p (p ^ n) = n := | |
by { rw [eq_some_iff], use dvd_refl _, rw [pow_dvd_pow_iff h0 hu], apply nat.not_succ_le_self } | |
lemma multiplicity_pow_self_of_prime {p : α} (hp : prime p) (n : ℕ) : | |
multiplicity p (p ^ n) = n := | |
multiplicity_pow_self (not_unit_of_prime hp) (ne_zero_of_prime hp) n | |
end | |
variables {p : ℕ} | |
lemma multiplicity_two_fact_int_lt {n : ℕ} (hn : n > 0) : multiplicity 2 (n.fact : ℤ) < n := | |
by simpa [int.coe_nat_multiplicity] using multiplicity_two_fact_lt n (ne_of_gt hn) | |
end multiplicity | |
open multiplicity | |
/- This proof has to be written carefully so that we don't get a timeout -/ | |
lemma IMO2019_4_n_eq_6 : 2 ^ (6 * 6) < nat.fact (6 * (6 - 1) / 2) := | |
begin | |
have h1 : nat.fact (6 * (6 - 1) / 2) = 1307674368000, | |
{ norm_num, repeat {rw [← nat.add_one]}, norm_num }, | |
have h2 : 2 ^ (6 * 6) = 68719476736, | |
{ change 2 ^ 36 = _, repeat { rw [nat.pow_succ] }, norm_num }, | |
rw [h1, h2], norm_num, | |
end | |
theorem IMO2019_4_upper_bound {k n : ℕ} (hk : k > 0) | |
(h : (k.fact : ℤ) = (range n).prod (λ i, 2 ^ n - 2 ^ i)) : n < 6 := | |
begin | |
have prime_2 : prime (2 : ℤ), | |
{ show prime ((2:ℕ) : ℤ), rw [← nat.prime_iff_prime_int], exact nat.prime_two }, | |
have h2 : n * (n - 1) / 2 < k, | |
{ rw [← enat.coe_lt_coe], convert multiplicity_two_fact_int_lt hk, symmetry, | |
rw [h, multiplicity.finset.prod prime_2, ← sum_range_id, ← enat.finset.sum], | |
apply sum_congr rfl, intros i hi, | |
rw [multiplicity_sub_of_gt, multiplicity_pow_self_of_prime prime_2], | |
rwa [multiplicity_pow_self_of_prime prime_2, multiplicity_pow_self_of_prime prime_2, | |
enat.coe_lt_coe, ←mem_range], | |
apply_instance }, | |
rw [←not_le], intro hn, | |
apply ne_of_lt _ h.symm, | |
suffices : ((range n).prod (λ i, 2 ^ n) : ℤ) < ↑k.fact, | |
{ apply lt_of_le_of_lt _ this, apply prod_le_prod, | |
{ intros, rw [sub_nonneg], apply pow_le_pow, norm_num, apply le_of_lt, rwa [← mem_range] }, | |
{ intros, apply sub_le_self, apply pow_nonneg, norm_num }}, | |
suffices : 2 ^ (n * n) < (n * (n - 1) / 2).fact, | |
{ rw [prod_const, card_range, ← pow_mul], rw [← int.coe_nat_lt_coe_nat_iff] at this, | |
convert lt_trans this _, norm_cast, rwa [int.coe_nat_lt_coe_nat_iff, nat.fact_lt], | |
refine nat.div_pos _ (by norm_num), | |
refine le_trans _ (mul_le_mul hn (nat.pred_le_pred hn) (zero_le _) (zero_le _)), | |
norm_num }, | |
refine nat.le_induction IMO2019_4_n_eq_6 _ n hn, | |
intros n' hn' ih, | |
have h5 : 1 ≤ 2 * n', | |
{ apply nat.succ_le_of_lt, apply mul_pos, norm_num, | |
exact lt_of_lt_of_le (by norm_num) hn' }, | |
have : 2 ^ (2 + 2) ≤ (n' * (n' - 1) / 2).succ, | |
{ change nat.succ (6 * (6 - 1) / 2) ≤ _, | |
apply nat.succ_le_succ, apply nat.div_le_div_right, | |
exact mul_le_mul hn' (nat.pred_le_pred hn') (zero_le _) (zero_le _) }, | |
rw [nat.triangle_succ], apply lt_of_lt_of_le _ nat.fact_mul_pow_le_fact, | |
refine lt_of_le_of_lt _ (mul_lt_mul ih (nat.pow_le_pow_of_le_left this _) | |
(nat.pow_pos (by norm_num) _) (zero_le _)), | |
rw [← nat.pow_mul, ← nat.pow_add], apply nat.pow_le_pow_of_le_right, norm_num, | |
rw [add_mul 2 2], | |
convert (add_le_add_left (add_le_add_left h5 (2 * n')) (n' * n')) using 1, ring | |
end | |
theorem IMO2019_4 {k n : ℕ} : k > 0 → n > 0 → | |
((nat.fact k : ℤ) = (range n).prod (λ i, 2 ^ n - 2 ^ i) ↔ (k, n) = (1, 1) ∨ (k, n) = (3, 2)) := | |
begin | |
intros hk hn, split, swap, | |
{ rintro (h|h); simp [prod.ext_iff] at h; rcases h with ⟨rfl, rfl⟩; | |
norm_num [prod_range_succ, nat.succ_mul] }, | |
intro h, | |
have := IMO2019_4_upper_bound hk h, | |
rcases lt_or_eq_of_le (nat.le_of_lt_succ this) with this|rfl, | |
rcases lt_or_eq_of_le (nat.le_of_lt_succ this) with this|rfl, | |
rcases lt_or_eq_of_le (nat.le_of_lt_succ this) with this|rfl, | |
rcases lt_or_eq_of_le (nat.le_of_lt_succ this) with this|rfl, | |
rcases lt_or_eq_of_le (nat.le_of_lt_succ this) with this|rfl, | |
{ exfalso, apply not_le_of_lt this, exact nat.succ_le_of_lt hn }, | |
{ left, congr, norm_num at h, norm_cast at h, rw [nat.fact_eq_one] at h, apply antisymm h, | |
apply nat.succ_le_of_lt hk }, | |
{ right, congr, norm_num [prod_range_succ] at h, norm_cast at h, rw [← nat.fact_inj], exact h, | |
rw [h], norm_num }, | |
all_goals { exfalso, norm_num [prod_range_succ] at h, norm_cast at h, }, | |
{ refine nat.ne_of_eq_monotone nat.monotone_fact 5 _ _ _ h, | |
all_goals { norm_num, repeat {rw [← nat.add_one]}, norm_num }}, | |
{ refine nat.ne_of_eq_monotone nat.monotone_fact 7 _ _ _ h, | |
all_goals { norm_num, repeat {rw [← nat.add_one]}, norm_num }}, | |
{ refine nat.ne_of_eq_monotone nat.monotone_fact 10 _ _ _ h, | |
all_goals { norm_num, repeat {rw [← nat.add_one]}, norm_num }}, | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment