Zulip Chat Archive

Stream: maths

Topic: cheap IMO problem


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 16:18):

There's probably a better way to state it.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 : )
:=

view this post on Zulip Kenny Lau (Sep 27 2020 at 09:58):

does by norm_num work?

view this post on Zulip Kevin Buzzard (Sep 27 2020 at 10:14):

I'm guessing no

view this post on Zulip Kevin Buzzard (Sep 27 2020 at 10:14):

But pari does it in a split second

view this post on Zulip 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

view this post on Zulip Miroslav Olšák (Sep 27 2020 at 13:09):

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

view this post on Zulip Scott Morrison (Sep 27 2020 at 13:17):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Sep 27 2020 at 15:27):

Can definitely be cleaned up.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 27 2020 at 15:44):

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

view this post on Zulip 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.

view this post on Zulip 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: May 10 2021 at 08:14 UTC