Skip to content

Instantly share code, notes, and snippets.

@fpvandoorn

fpvandoorn/imo2019_4.lean

Last active Aug 2, 2019
Embed
What would you like to do?
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 : 12 * 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
You can’t perform that action at this time.