Zulip Chat Archive

Stream: maths

Topic: cheap IMO problem

Kevin Buzzard (Sep 25 2020 at 16:16):

IMO 1979 Q1:

 Let m and n be positive integers such that:

      m/n = 1 - 1/2 + 1/3 - 1/4 + ... - 1/1318 + 1/1319.

Prove that m is divisible by 1979.

SPOILER ALERT LINK IMO 1979 Q1 solution should be easy to formalise now we have p-adic valuation, right?

import tactic

import algebra.big_operators.basic

open_locale big_operators

def h : fin 1320 → ℚ := λ n, (-1)^((n : ℕ)+ 1)/n

open nat

instance foo : fact (prime 1979) := by norm_num

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ x, h x
→ 1979 ∣ p :=
begin
  sorry
end

They were chatting about it on the IMO stream.

Kevin Buzzard (Sep 25 2020 at 16:18):

There's probably a better way to state it.

Kevin Buzzard (Sep 25 2020 at 16:28):

import tactic

import algebra.big_operators.basic

open_locale big_operators

open nat

instance foo : fact (prime 1979) := by norm_num

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ n in finset.range 1320, (-1)^(n + 1) / n
→ 1979 ∣ p :=
begin
  sorry
end

is nicer.

Kevin Buzzard (Sep 25 2020 at 20:01):

I made a start but now I have to eat:

import tactic

import algebra.big_operators.ring

import data.nat.parity

open_locale big_operators

open finset

open nat

instance foo : fact (prime 1979) := by norm_num

open finset

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ n in finset.range 1320, (-1)^(n + 1) / n
→ 1979 ∣ p :=
begin
  let a : ℚ := ∑ n in range 1320, (-1)^(n + 1) / n,
  let b : ℚ := ∑ n in range 1320, 1 / n,
  -- b - a = 2(1/2+1/4+...+1318)
  -- = 1+1/2+1/3+...+1/659
  let c : ℚ := ∑ n in range 660, 1 / n,
  -- want b - a = c i.e. to formalise lines above
  let e : ℕ ↪ ℕ := ⟨λ n, 2 * n, λ a b, mul_left_cancel' (by norm_num)⟩,
  have h1 := sum_map (range 660) e (λ n, (1 : ℚ) / n),
  -- first goal b - a = c,
  -- hence a = sum from 660 to 1319
  -- then they cancel
  have h0 : b - a = c,
  calc b - a = ∑ n in range 1320, (1/n - (-1)^(n+1)/n) : by rw sum_sub_distrib
    ... = ∑ n in range 1320, ite (even n) (2/n) 0 : by {
      apply sum_congr rfl,
      rintros x hx,
      rw [pow_add, pow_one, mul_neg_one, neg_div, sub_neg_eq_add, ← _root_.add_div],
      split_ifs,
      { rcases h with ⟨n, rfl⟩,
        rw [pow_mul, pow_two],
        simp, norm_num },
      { rw not_even_iff at h,
        have h8 := nat.mod_add_div x 2,
        rw h at h8,
        suffices : (1 : ℚ) + (-1)^x = 0,
          rw this, simp,
        rw ← h8,
        simp [pow_add, pow_mul],
      }
    }
    ... = ∑ (x : ℕ) in filter even (range 1320), 2 / x : by rw sum_filter
    ... = ∑ (x : ℕ) in map e (range 660), (2 : ℚ) / x : by {
      apply sum_congr, swap, simp,
      apply finset.subset.antisymm,
        sorry,
      sorry
    }
    ... = c : sorry,
  sorry
end

Yakov Pechersky (Sep 27 2020 at 07:43):

Here's my fin powered attempt, I'm now struggling with collapsing the "telescoping" sum.

import tactic.ring_exp
import data.matrix.notation
import data.rat.cast

open_locale big_operators

def h {n : ℕ} : fin n → ℚ := λ k, (-1)^((k : ℕ)+ 1)/k

instance foo : fact (nat.prime 1979) := by norm_num

@[simp] lemma fin.coe_sub {n : ℕ} (x y : fin n) : (((x - y) : fin n) : ℕ) = (x : ℕ) - y :=
by { cases x, cases y, refl }

lemma fin.coe_bit0 {n : ℕ} {x : fin n} (h : (bit0 x : ℕ) < n) : ((bit0 x : fin n) : ℕ) = bit0 x :=
by { cases x, exact nat.mod_eq_of_lt h }

lemma fin.coe_bit1 {n : ℕ} {x : fin (n + 2)} (h : (bit1 x : ℕ) < n + 2) :
  ((bit1 x : fin (n + 2)) : ℕ) = bit1 x :=
begin
  rw bit1 at h,
  simpa only [bit1, fin.coe_add,
              fin.coe_bit0 (lt_of_le_of_lt (nat.le_add_right _ _) h)] using nat.mod_eq_of_lt h,
end

section hF

variables {n : ℕ} (N : ℕ) (x : fin n)

def hF : ℚ := 1 / ((N + (x : ℕ)) : ℚ)

lemma shift : hF N.succ x.cast_succ = hF N x.succ :=
by { simp [hF], ring_exp }

lemma reduce : @hF n.succ N x.cast_succ = @hF n N x :=
by simp [hF]

lemma hreduce : h x.cast_succ.cast_succ = h x :=
by simp [h]

lemma h_to_hF : (∑ x : fin (N * 2), h x) = ∑ x : fin N, hF N x :=
begin
  induction N with N hN,
  { refl },
  symmetry,
  rw fin.sum_univ_cast_succ,
  simp_rw shift N,
  rw [←add_right_inj (hF N 0), ←add_assoc, ←fin.sum_univ_succ, fin.sum_univ_cast_succ],
  simp_rw reduce,
  symmetry,
  rw [nat.succ_mul, fin.sum_univ_cast_succ, fin.sum_univ_cast_succ],
  simp_rw hreduce,
  rw [hN, ←add_assoc, ←add_assoc, add_comm (hF _ _), add_assoc, add_assoc, add_assoc],
  congr' 1,
  rw ←add_assoc,
  congr,
  { have nh : (-1 : ℚ) ^ (N * 2 + 1) = -1,
    { rw [mul_comm],
      simp [pow_add, pow_mul] },
    have : (N : ℚ)⁻¹ = 2 / (N * 2),
      { norm_num [←one_div, mul_comm, div_mul_eq_div_mul_one_div] },
    norm_num [h, hF, nh, this],
    ring_exp },
  { have nh : (-1 : ℚ) ^ (N * 2 + 1 + 1) = 1,
    { rw [mul_comm],
      simp [pow_add, pow_mul] },
    norm_num [h, hF, nh],
    ring_exp }
end

end hF

section nums

lemma coe_659 : ((659 : fin 660) : ℕ) = 659 :=
begin
  rw [fin.coe_bit1, fin.coe_bit1, fin.coe_bit0, fin.coe_bit0, fin.coe_bit1,
      fin.coe_bit0, fin.coe_bit0, fin.coe_bit1, fin.coe_bit0],
  simp only [fin.coe_one],
  all_goals { dec_trivial }
end

lemma pos_660 : (0 : ℕ) < 660 := dec_trivial

lemma posQ_660 : (0 : ℚ) < 660 := nat.cast_lt.mpr pos_660

lemma expand (d : fin 660) : hF 660 d + hF 660 (659 - d) = 1979 / ((660 + d) * (1319 - d)) :=
begin
  obtain ⟨d, dlim⟩ := d,
  simp only [hF, one_div],
  rw inv_add_inv,
  simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk, fin.coe_sub, coe_659,
              nat.cast_sub (nat.le_of_succ_le_succ dlim), coe_coe],
  refine congr_arg2 has_div.div _ _,
  { rw add_assoc,
    rw add_comm,
    rw ←eq_sub_iff_add_eq,
    rw add_comm,
    rw add_assoc,
    norm_num },
  { rw add_sub,
    norm_num },
  { simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk],
    refine ne_of_gt (lt_of_lt_of_le posQ_660 _),
    exact le_add_of_nonneg_right (nat.cast_nonneg d) },
  { simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk],
    refine ne_of_gt (lt_of_lt_of_le posQ_660 _),
    exact le_add_of_nonneg_right (nat.cast_nonneg _) }
end

lemma sub_659 : fin.last 659 = (659 : fin 660) - (0 : fin 660) := rfl

end nums

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ x : fin 1320, h x
→ 1979 ∣ p :=
begin
  intro F,
  rw (show 1320 = 660 * 2, by norm_num) at F,
  rw h_to_hF at F,
  rw fin.sum_univ_cast_succ at F,
  rw fin.sum_univ_succ at F,
  rw add_assoc at F,
  rw add_comm (∑ _, _) at F,
  rw ←add_assoc at F,
  rw sub_659 at F,
  rw fin.cast_succ_zero at F,
  rw expand 0 at F,
  sorry,
end

Miroslav Olšák (Sep 27 2020 at 09:48):

As we were discussing that it could be just easily canlculated, how could one prove that?:

example : (∑ n in finset.range 1320, ((-1)^(n + 1) / n : ℚ))
=
(9712435370176457211789032112275705035436058023056668172162691122769643536134963388887418503518212227707181887399284421324209991580261372180881066042267340013822543021630993790301871917306672479003742347731906894502206611684973377349822140727866748793472314555146081954133359219693224842345716201562838113110488664229990443258508595332395129617286143580898566908128232436187466371871641095608257859832669859587159077972843255741143946005144546720084104126426401254209483858435525146637078869452056788708944608960016712180409515668301909686056363654039823351264466923197720153813
/
14004426370194880461934343682044774391282833031127910746297786781959105584828861694180270900155320736866485178357969757814225700469374818454186270560156419686116542029027696742870488277713573014598870206397512488706141517193426122086231634178080237723065448682598131182597623527313179068878231298472650458406330723014358986732179004322578669107971003162372262774921109835980551500767898797452304799628071849186633284721093163439037683000781898695594646092124867941059532453140720984993275703737648888419223774236963722967299484493466538792766661068428697404447683623975519360000 : ℚ)
:=

Kenny Lau (Sep 27 2020 at 09:58):

does by norm_num work?

Kevin Buzzard (Sep 27 2020 at 10:14):

I'm guessing no

Kevin Buzzard (Sep 27 2020 at 10:14):

But pari does it in a split second

Rob Lewis (Sep 27 2020 at 10:20):

In principle this works -- it reduces things to the scope of norm_num. But norm_num uses too much memory for VSCode. Maybe if you run it with a higher memory limit, or do something clever to simplify intermediate steps, you could make it work. (Not in a split second.)

import algebra.big_operators.finsupp data.rat

open_locale big_operators

example : (∑ n in finset.range 1320, ((-1)^(n + 1) / n : ℚ))
=
(9712435370176457211789032112275705035436058023056668172162691122769643536134963388887418503518212227707181887399284421324209991580261372180881066042267340013822543021630993790301871917306672479003742347731906894502206611684973377349822140727866748793472314555146081954133359219693224842345716201562838113110488664229990443258508595332395129617286143580898566908128232436187466371871641095608257859832669859587159077972843255741143946005144546720084104126426401254209483858435525146637078869452056788708944608960016712180409515668301909686056363654039823351264466923197720153813
/
14004426370194880461934343682044774391282833031127910746297786781959105584828861694180270900155320736866485178357969757814225700469374818454186270560156419686116542029027696742870488277713573014598870206397512488706141517193426122086231634178080237723065448682598131182597623527313179068878231298472650458406330723014358986732179004322578669107971003162372262774921109835980551500767898797452304799628071849186633284721093163439037683000781898695594646092124867941059532453140720984993275703737648888419223774236963722967299484493466538792766661068428697404447683623975519360000 : ℚ)
:=
begin
  iterate 1320
  { transitivity,
    apply finset.sum_range_succ,
    rw ← eq_sub_iff_add_eq' },
  rw finset.sum_range_zero,
  simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_add, nat.cast_zero, nat.cast_one],
  -- norm_num1,
end

Miroslav Olšák (Sep 27 2020 at 13:09):

Would it be possible to tell lean to just call #eval to the first expression?

Scott Morrison (Sep 27 2020 at 13:17):

Sure. But #eval is just a calculator; no proofs attached.

Yakov Pechersky (Sep 27 2020 at 15:27):

All that's left to do is change the divisibility goal to be on Q instead of N:

import tactic.ring_exp
import data.matrix.notation
import data.rat.cast

open_locale big_operators

def h {n : ℕ} : fin n → ℚ := λ k, (-1)^((k : ℕ)+ 1)/k

instance foo : fact (nat.prime 1979) := by norm_num

@[simp] lemma fin.coe_sub {n : ℕ} (x y : fin n) : (((x - y) : fin n) : ℕ) = (x : ℕ) - y :=
by { cases x, cases y, refl }

lemma fin.coe_bit0 {n : ℕ} {x : fin n} (h : (bit0 x : ℕ) < n) : ((bit0 x : fin n) : ℕ) = bit0 x :=
by { cases x, exact nat.mod_eq_of_lt h }

lemma fin.coe_bit1 {n : ℕ} {x : fin (n + 2)} (h : (bit1 x : ℕ) < n + 2) :
  ((bit1 x : fin (n + 2)) : ℕ) = bit1 x :=
begin
  rw bit1 at h,
  simpa only [bit1, fin.coe_add,
              fin.coe_bit0 (lt_of_le_of_lt (nat.le_add_right _ _) h)] using nat.mod_eq_of_lt h,
end

lemma nat.le_add (n m : ℕ) : n ≤ n + m :=
nat.le.intro rfl

section hF

variables {n : ℕ} (N : ℕ) (x : fin n)

def hF : ℚ := 1 / ((N + (x : ℕ)) : ℚ)

lemma shift : hF N.succ x.cast_succ = hF N x.succ :=
by { simp [hF], ring_exp }

lemma shift' : hF (N + 1) x.cast_succ = hF N x.succ :=
by { simp [hF], ring_exp }

lemma reduce : @hF n.succ N x.cast_succ = @hF n N x :=
by simp [hF]

lemma hreduce : h x.cast_succ.cast_succ = h x :=
by simp [h]

lemma h_to_hF : (∑ x : fin (N * 2), h x) = ∑ x : fin N, hF N x :=
begin
  induction N with N hN,
  { refl },
  symmetry,
  rw fin.sum_univ_cast_succ,
  simp_rw shift N,
  rw [←add_right_inj (hF N 0), ←add_assoc, ←fin.sum_univ_succ, fin.sum_univ_cast_succ],
  simp_rw reduce,
  symmetry,
  rw [nat.succ_mul, fin.sum_univ_cast_succ, fin.sum_univ_cast_succ],
  simp_rw hreduce,
  rw [hN, ←add_assoc, ←add_assoc, add_comm (hF _ _), add_assoc, add_assoc, add_assoc],
  congr' 1,
  rw ←add_assoc,
  congr,
  { have nh : (-1 : ℚ) ^ (N * 2 + 1) = -1,
    { rw [mul_comm],
      simp [pow_add, pow_mul] },
    have : (N : ℚ)⁻¹ = 2 / (N * 2),
      { norm_num [←one_div, mul_comm, div_mul_eq_div_mul_one_div] },
    norm_num [h, hF, nh, this],
    ring_exp },
  { have nh : (-1 : ℚ) ^ (N * 2 + 1 + 1) = 1,
    { rw [mul_comm],
      simp [pow_add, pow_mul] },
    norm_num [h, hF, nh],
    ring_exp }
end

end hF

section nums

lemma coe_659 : ((659 : fin 660) : ℕ) = 659 :=
begin
  rw [fin.coe_bit1, fin.coe_bit1, fin.coe_bit0, fin.coe_bit0, fin.coe_bit1,
      fin.coe_bit0, fin.coe_bit0, fin.coe_bit1, fin.coe_bit0],
  simp only [fin.coe_one],
  all_goals { dec_trivial }
end

lemma pos_660 : (0 : ℕ) < 660 := dec_trivial

lemma posQ_660 : (0 : ℚ) < 660 := nat.cast_lt.mpr pos_660

lemma expand (d : fin 660) : hF 660 d + hF 660 (659 - d) = 1979 / ((660 + d) * (1319 - d)) :=
begin
  obtain ⟨d, dlim⟩ := d,
  simp only [hF, one_div],
  rw inv_add_inv,
  simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk, fin.coe_sub, coe_659,
              nat.cast_sub (nat.le_of_succ_le_succ dlim), coe_coe],
  refine congr_arg2 has_div.div _ _,
  { rw add_assoc,
    rw add_comm,
    rw ←eq_sub_iff_add_eq,
    rw add_comm,
    rw add_assoc,
    norm_num },
  { rw add_sub,
    norm_num },
  { simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk],
    norm_cast,
    exact ne_of_gt (lt_of_lt_of_le pos_660 (nat.le_add 660 d)) },
  { simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk],
    refine ne_of_gt (lt_of_lt_of_le posQ_660 _),
    exact le_add_of_nonneg_right (nat.cast_nonneg _) }
end

lemma expand' (d : ℕ) (h : d < 331) :
(∑ x : fin (d * 2), hF (990 - d) x) = ∑ x : fin d, ((1979 : ℚ) / ((990 + (x : ℕ)) * (989 - (x : ℕ)))) :=
begin
  induction d with d hd,
  { rw zero_mul,
    simp only [fin.sum_univ_zero] },
  { have h' := nat.lt_of_succ_lt h,
    have h'' := nat.mul_lt_mul h' (le_refl 2) (by dec_trivial),
    have h''' := nat.mul_lt_mul h (le_refl 2) (by dec_trivial),
    rw nat.succ_mul at h''',
    rw nat.succ_mul,
    rw fin.sum_univ_succ,
    rw fin.sum_univ_cast_succ,
    rw add_comm,
    rw add_assoc,
    simp_rw ←shift',
    simp_rw reduce,
    have : 990 - d.succ + 1 = 990 - d,
      { rw ←nat.sub_sub_assoc,
        refl,
        refine le_of_lt (lt_trans h _),
        norm_num,
        exact nat.succ_pos' },
    rw this,
    clear this,
    rw hd h',
    rw fin.sum_univ_cast_succ,
    congr' 1,
    simp only [hF, one_div, add_zero, fin.coe_zero, nat.succ_sub_succ_eq_sub, fin.coe_last, nat.cast_bit0, nat.cast_zero,
 nat.cast_one, nat.cast_mul],
    rw mul_two,
    rw ←add_assoc,
    norm_cast,
    have le990 : d ≤ 990,
      { refine le_of_lt (lt_trans h' _),
        norm_num },
    have le989 : d ≤ 989,
      { refine le_of_lt (lt_trans h' _),
        norm_num },
    rw nat.sub_add_cancel le990,
    rw inv_add_inv,
    refine congr_arg2 has_div.div _ _,
    { norm_cast,
      rw add_assoc,
      rw nat.add_sub_cancel' le989,
      norm_num },
    { norm_cast },
    { rw nat.cast_ne_zero,
      refine ne_of_gt (lt_of_lt_of_le _ (nat.le_add 990 d)),
      norm_num },
    { rw nat.cast_ne_zero,
      refine ne_of_gt _,
      refine nat.sub_pos_of_lt _,
      refine lt_trans h' _,
      norm_num } }
end

lemma sub_659 : fin.last 659 = (659 : fin 660) - (0 : fin 660) := rfl

end nums

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ x : fin 1320, h x
→ 1979 ∣ p :=
begin
  intro F,
  rw (show 1320 = 660 * 2, by norm_num) at F,
  rw h_to_hF at F,
  rw (show 660 = 330 * 2, by norm_num) at F,
  have : ∀ x : fin (330 * 2), hF (330 * 2) x = hF (990 - 330) x,
    { intro x,
      simp_rw (show 330 * 2 = 990 - 330, by norm_num) },
  simp_rw this at F,
  rw expand' 330 (by norm_num) at F,
  simp_rw division_def at F,
  rw ←finset.mul_sum at F,
  set S := (∑ (x : fin 330), (((990 : ℚ) + x) * (989 - x))⁻¹) with hS,
  simp_rw [coe_coe] at hS,
  rw ←hS at F,
  sorry
  /-
p q : ℕ,
this : ∀ (x : fin (330 * 2)), hF (330 * 2) x = hF (990 - 330) x,
S : ℚ := ∑ (x : fin 330), ((990 + ↑x) * (989 - ↑x))⁻¹,
hS : S = ∑ (x : fin 330), ((990 + ↑↑x) * (989 - ↑↑x))⁻¹,
F : ↑p * (↑q)⁻¹ = 1979 * S
⊢ 1979 ∣ p
-/

end

Yakov Pechersky (Sep 27 2020 at 15:27):

Can definitely be cleaned up.

Kevin Buzzard (Sep 27 2020 at 15:44):

I tried with the finset approach (no fin) and it ended up looking like this:

import tactic
import algebra.big_operators.ring
import data.nat.parity
import data.finset.intervals
import data.padics.hensel

open_locale big_operators

open finset

open nat

instance foo : fact (nat.prime 1979) := by norm_num

open finset

--example (k : Type) [comm_ring k] (a b : k) : k := a - b

namespace imo1979q1

-- some constants
@[reducible] def a : ℚ := ∑ n in range 1320, (-1)^(n + 1) / n
@[reducible] def b : ℚ := ∑ n in range 1320, 1 / n
@[reducible] def c : ℚ := ∑ n in range 660, 1 / n
@[reducible] def d : ℚ := ∑ n in Ico 660 1320, 1 / n
@[reducible] def e : ℚ := ∑ n in range 330, 1 / (n + 660)
@[reducible] def f : ℚ := ∑ n in range 330, 1 / (1319 - n)

/-
  We start with some lemmas:

  Lemma 1 : b - a = c
  Lemma 2 : c + d = b (and hence a = d)
  Lemma 3 : d = e + f

  Then we prove the theorem, by showing the 1979-adic
  valuation of e + f is positive.
-/

@[reducible] def double : ℕ ↪ ℕ := ⟨λ n, 2 * n, λ a b, mul_left_cancel' (by norm_num)⟩
--@[reducible] def
lemma lemma1 : b - a = c :=
  calc b - a = ∑ n in range 1320, (1/n - (-1)^(n+1)/n) : by rw sum_sub_distrib
    ... = ∑ n in range 1320, ite (even n) (2/n) 0 : by {
      apply sum_congr rfl,
      rintros x hx,
      rw [pow_add, pow_one, mul_neg_one, neg_div, sub_neg_eq_add, ← _root_.add_div],
      split_ifs,
      { rcases h with ⟨n, rfl⟩,
        rw [pow_mul, pow_two],
        simp, norm_num },
      { rw not_even_iff at h,
        have h8 := nat.mod_add_div x 2,
        rw h at h8,
        suffices : (1 : ℚ) + (-1)^x = 0,
          rw this, simp,
        rw ← h8,
        simp [pow_add, pow_mul],
      }
    }
    ... = ∑ (x : ℕ) in filter even (range 1320), 2 / x : by rw sum_filter
    ... = ∑ (x : ℕ) in map double (range 660), (2 : ℚ) / x : by {
      -- extract_goal, -- problem not observed
      apply sum_congr, swap, simp,
      apply finset.subset.antisymm,
      { --extract_goal, -- problem not observed
        intros x hx,
        rw mem_filter at hx,
        rcases hx with ⟨hx1, m, rfl⟩,
        rw mem_map,
        --extract_goal, -- problem not observed
        -- uncommenting this times out
        -- use m,                          -- << timeout
         existsi m, -- works fine
         existsi _, refl,
         rw mem_range at hx1 ⊢,
         linarith },
      { intros x hx,
        rw mem_filter,
        rw mem_map at hx,
        rcases hx with ⟨a, ha, rfl⟩,
        split,
        { rw mem_range at ha ⊢,
          change 2 * a < 1320,
          linarith },
        { existsi a,
          refl
        }
      }
    }
    ... = c : by {
      rw sum_map (range 660) double (λ n, (2 : ℚ) / n),
      apply sum_congr, refl, -- is there a better way?
      intros x hx,
      show (2 : ℚ) / (2 * x : ℕ) = _,
      push_cast,
      change (2 : ℚ) / (2 * x) = 1 / x,
      generalize h : (x : ℚ) = q,
      by_cases hq : q = 0,
        rw hq, ring,
      field_simp [hq] }

lemma lemma2 : c + d = b :=
begin
  unfold c d b,
  simp only [← Ico.zero_bot],
  rw ← sum_union,
  { apply sum_congr,
    { ext x,
      suffices : x < 660 ∨ 660 ≤ x ∧ x < 1320 ↔ x < 1320,
        simpa,
      split,
      { rintro (a | ⟨b, c⟩); linarith },
      { intro hx,
        cases lt_or_le x 660,
        { left, assumption },
        { right, cc } } },
    { intros, refl } },
  apply Ico.disjoint_consecutive
end

lemma corollary3 : a = d :=
begin
  apply add_left_cancel, swap, exact c,
  rw lemma2,
  rw ← lemma1,
  apply sub_add_cancel,
end

lemma lemma4 : e + f = d :=
begin
  unfold d e f,
  rw (Ico.zero_bot 330).symm,
  have h : ∑ (n : ℕ) in Ico 0 330, (1 : ℚ) / (n + 660) =
    ∑ (m : ℕ) in Ico 660 990, (1 : ℚ) / m,
  {
    rw ←Ico.image_add 0 330 660,
    rw sum_image,
    { apply sum_congr, refl,
      intros, simp [add_comm] },
    { intros x hx y hy,
      exact (add_right_inj 660).mp }
  },
  rw h, clear h,
  have h : ∑ (n : ℕ) in Ico 0 330, (1 : ℚ) / (1319 - n) =
    ∑ (m : ℕ) in Ico 990 1320, (1 : ℚ) / m,
  { have h2 : image (λ (j : ℕ), 1319 - j) (Ico 0 330) =
      Ico (990) (1320),
    { rw Ico.image_const_sub, refl, linarith },
    rw ← h2,
    rw sum_image,
    { apply sum_congr, refl,
      intros,
      apply congr_arg,
      rw nat.cast_sub, norm_cast,
      rw Ico.mem at H,
      cases H, linarith },
    { intros x hx y hy,
      intro h,
      rw [Ico.zero_bot, mem_range] at hx hy,
      rw nat.sub_eq_iff_eq_add (show x ≤ 1319, by linarith) at h,
      rw nat.sub_add_eq_add_sub (show y ≤ 1319, by linarith) at h,
      symmetry' at h,
      rw nat.sub_eq_iff_eq_add at h, swap, linarith,
      exact (add_right_inj 1319).mp h }
  },
  rw h, clear h,
  rw ←sum_union,
  { apply sum_congr,
    { apply Ico.union_consecutive; linarith },
    { intros, refl } },
  { apply Ico.disjoint_consecutive }
end

lemma lemma5 : ∀ n ∈ range 330, ∥ (((1 / (n + 660) + 1 / (1319 - n)) : ℚ) : ℚ_[1979]) ∥ < 1 :=
begin
  intros n hn,
  rw mem_range at hn,
  have h1 : (n : ℚ) + 660 ≠ 0,
    apply ne_of_gt,
    norm_cast, simp,
  have h2 : (1319 : ℚ) - n ≠ 0,
    have h3 : (n : ℚ) < 330, norm_cast, exact hn,
    linarith,
  let p : ℕ := 1979,
  have h3 : (1 : ℚ) / (n + 660) + 1 / (1319 - n) = 1979 / ((n + 660) * (1319 - n)),
    field_simp [h1, h2],
    generalize : (n : ℚ) = q,
    ring,
  rw h3, clear h3,
  push_cast,
  rw normed_field.norm_div,
  rw normed_field.norm_mul,
  rw div_lt_one,
    sorry,
  sorry,
end



theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ n in finset.range 1320, (-1)^(n + 1) / n
→ 1979 ∣ p :=
begin
  change _ = a → _,
  rw corollary3,
  rw ← lemma4,
  intro h,
  unfold e f at h,
  rw ← sum_add_distrib at h,

  sorry
end

end imo1979q1

I'm not finished either -- I'm at the same place as you in fact.

Kevin Buzzard (Sep 27 2020 at 15:44):

I just decided it was time I learnt about how sums work in Lean nowadays :-)

Yakov Pechersky (Sep 27 2020 at 15:50):

I think the solution for my approach is to somehow identify q with the product of 660 to 1320. And then push the casts to remove the casts to Q and make everything statements about N.

Kevin Buzzard (Sep 27 2020 at 15:51):

My gut feeling is that using p-adic norm should make life easier; you don't have to deal with the denominator that way.

Last updated: Dec 20 2023 at 11:08 UTC