Zulip Chat Archive

Stream: general

Topic: IMO 1972 B2


Stanislas Polu (Aug 26 2020 at 07:41):

Hi! I'm a beginner to Lean and want to prove IMO 1972 B2 (which was used to compare various formal systems at ICMS 2006 to compare various systems). I formalized the statement as follows:

example
  (f :   )
  (g:   )
  (hf1 :  x,  y, (f (x+y) + f(x-y)) = 2 * f(x) * f(y))
  (hf2 :  y, |f(y)|  1)
  (hf3 :  x, f(x)  0) :
   y, |g(y)|  1 :=
begin
  sorry
end

I'm a bit stuck as I'd like to have a way to calculate/operate with the supremum of f or I can only find is_sub in mathlib. What would be a good way to have k : ℝ such that k is the supremum of f and prove that it's in ℝ because f is bounded? Also is is_lub (f '' ℝ) k the correct way to say that k is the supremum of a real function f? Thanks for your help :thank_you:

Johan Commelin (Aug 26 2020 at 07:45):

@Stanislas Polu Hi, does your code typecheck in Lean? Which imports do you use?

Johan Commelin (Aug 26 2020 at 07:45):

I don't know the analysis part too well, but for me the | .. | didn't work after importing data.real.basic.

Johan Commelin (Aug 26 2020 at 07:46):

I believe that we always use \|| .. \|| for norms

Stanislas Polu (Aug 26 2020 at 07:46):

Ah sorry yeah, I started working at the end of the tutorials, so this might not be totally legit in mathlib; there |..| is defined. I will definitely translate to mathlib :+1:

Johan Commelin (Aug 26 2020 at 07:53):

Here's a start:

import data.real.pi

example (f g :   )
  (hf1 :  x,  y, (f (x+y) + f(x-y)) = 2 * f(x) * f(y))
  (hf2 :  y, f(y)  1)
  (hf3 :  x, f(x)  0)
  (y : ) :
  g(y)  1 :=
begin
  classical,
  let k :  := Sup (set.range f),
  have hk := real.Sup_def (set.range f),
  have h1 :  x : , x  set.range f,
  { use f 0, exact set.mem_range_self 0, },
  have h2 :  x : ,  y  set.range f, y  x,
  { sorry },
  -- useful lemmas: real.Sup_le real.le_Sup, etc...
end

Stanislas Polu (Aug 26 2020 at 07:54):

Thanks!!

Stanislas Polu (Aug 26 2020 at 07:54):

Awesome to get me started :thank_you:

Mario Carneiro (Aug 26 2020 at 07:58):

I think there was a thread on this in the past

Mario Carneiro (Aug 26 2020 at 08:00):

I think I was thinking of another proof assistant ;)

Stanislas Polu (Aug 26 2020 at 08:01):

You have to start somewhere :)

Patrick Massot (Aug 26 2020 at 08:18):

The absolute values bars in the tutorials project means abs: https://github.com/leanprover-community/tutorials/blob/master/src/solutions/tuto_lib.lean#L12 There is no other trick involved here.

Ruben Van de Velde (Aug 26 2020 at 09:20):

Might be easier to prove if you change f(y) to g(y) in hf1

Stanislas Polu (Aug 26 2020 at 09:33):

Nice catch :)

Ruben Van de Velde (Aug 26 2020 at 12:37):

I wrote an awful proof:

import data.real.basic
import analysis.normed_space.basic

example (f g :   )
  (hf1 :  x,  y, (f (x+y) + f(x-y)) = 2 * f(x) * g(y))
  (hf2 :  y, f(y)  1)
  (hf3 :  x, f(x)  0)
  (y : ) :
  g(y)  1 :=
begin
  classical,
  set S := set.range (λ x, f x),
  set k :  := Sup S,
  have h1 :  x,  y  S, y  x,
  { use 1,
    intros fz zs,
    obtain z, rfl := zs,
    apply hf2 },
  have h2 :  x, f x  k,
  {
    intro x,
    apply real.le_Sup,
    { assumption },
    { apply set.mem_range_self, },
  },
  have h3 : 0 < k,
  { obtain x, hx := hf3,
    calc 0
        < f x : norm_pos_iff.mpr hx
    ...  k : h2 x,
  },
  have h4 :  x : , x  S,
  { use f 0, exact set.mem_range_self 0, },
  have h5 :  x, _,
  { intro x,
    calc 2 * (f x * g y)
        = 2 * f x * g y : by simp [real.norm_eq_abs, abs_mul, mul_assoc]
    ... = f (x + y) + f (x - y) : by rw hf1
    ...  f (x + y) + f (x - y) : norm_add_le _ _
    ...  k + k : add_le_add (h2 _) (h2 _)
    ... = 2 *k : (two_mul _).symm,
  },
  have h5':  (x : ), f x * g y  k,
  {
    intro x,
    apply (mul_le_mul_left zero_lt_two).mp (h5 x),
  },

  by_contra,
  push_neg at a,

  set k' := k / g y,
  have h6 :  x, f x  k',
  { intros x,
    rw le_div_iff,
    { apply h5', },
    exact trans zero_lt_one a, },
  have h7 : k' < k,
  { rw div_lt_iff,
    apply lt_mul_of_one_lt_right 0 < k a,
    exact trans zero_lt_one a },
  have h8 : k  k',
  { apply real.Sup_le_ub _ h4,
    rintros y' yy, rfl,
    apply h6,
  },
  apply lt_irrefl k',
  calc k'
      < k : _
  ...  k' : _
end

Stanislas Polu (Aug 27 2020 at 14:33):

Slightly refactored proof but still structurally the same:

import data.real.basic
import analysis.normed_space.basic

example (f g :   )
  (hf1 :  x,  y, (f(x+y) + f(x-y)) = 2 * f(x) * g(y))
  (hf2 :  y, f(y)  1)
  (hf3 :  x, f(x)  0)
  (y : ) :
  g(y)  1 :=
begin
  classical,
  set S := set.range (λ x, f x),
  let k :  := Sup (S),

  have hk₁ :  x, f x  k,
  { have h :  x,  y  S, y  x,
    { use 1,
      intros _ hy,
      rw set.mem_range at hy,
      rcases hy with z, rfl,
      exact hf2 z,
    },
    intro x,
    exact real.le_Sup S h (set.mem_range_self x),
  },
  have hk₂ :  x, _,
  { intro x,
    calc 2 * (f x * g y)
        = 2 * f x * g y : by simp [real.norm_eq_abs, abs_mul, mul_assoc]
    ... = f (x + y) + f (x - y) : by rw hf1
    ...  f (x + y) + f (x - y) : norm_add_le _ _
    ...  k + k : add_le_add (hk₁ _) (hk₁ _)
    ... = 2 * k : (two_mul _).symm,
  },

  by_contra hneg,
  push_neg at hneg,
  set k' := k / g y,

  have H₁ : k' < k,
  { have h₁ : 0 < k,
    { obtain x, hx := hf3,
      calc 0
          < f x : norm_pos_iff.mpr hx
     ...  k : hk₁ x },
    rw div_lt_iff,
    apply lt_mul_of_one_lt_right h₁ hneg,
    exact trans zero_lt_one hneg },

  have H₂ : k  k',
  { have h₁ :  x : , x  S,
    { use f 0, exact set.mem_range_self 0, },
    have h₂ :  x, f x  k',
    { intros x,
      rw le_div_iff,
      { apply (mul_le_mul_left zero_lt_two).mp (hk₂ x) },
      { exact trans zero_lt_one hneg } },
    apply real.Sup_le_ub _ h₁,
    rintros y' yy, rfl,
    exact h₂ yy },

  apply lt_irrefl k',
  calc k'
      < k : H₁
  ...  k' : H₂,
end

Stanislas Polu (Aug 27 2020 at 14:34):

I'd be very curious to get feedback on how to make it more concise, if anybody has any.

Ruben Van de Velde (Aug 27 2020 at 15:17):

I played around with it some more, with more backwards reasoning:

import data.real.basic
import analysis.normed_space.basic

example (f g :   )
  (hf1 :  x,  y, (f (x+y) + f(x-y)) = 2 * f(x) * g(y))
  (hf2 :  y, f(y)  1)
  (hf3 :  x, f(x)  0)
  (y : ) :
  g(y)  1 :=
begin
  set S := set.range (λ x, f x),
  set k :  := Sup S,
  have h :  x, f x  k := λ x, real.le_Sup S 1, set.forall_range_iff.mpr hf2 $ set.mem_range_self x,

  by_contra a,
  push_neg at a,
  have hgy : 0 < g y := trans zero_lt_one a,

  set k' := k / g y,
  apply lt_irrefl k',
  apply lt_of_lt_of_le,
  { refine (div_lt_iff hgy).mpr (lt_mul_of_one_lt_right _ a),
    obtain x, hx := hf3,
    exact lt_of_lt_of_le (norm_pos_iff.mpr hx) (h x) },
  { apply real.Sup_le_ub S f 0, set.mem_range_self 0,
    rw set.forall_range_iff,
    intro x,
    rw [le_div_iff hgy, mul_le_mul_left zero_lt_two],
    calc 2 * (f x * g y)
        = 2 * f x * g y : by simp [real.norm_eq_abs, abs_mul, mul_assoc]
    ... = f (x + y) + f (x - y) : by rw hf1
    ...  f (x + y) + f (x - y) : norm_add_le _ _
    ...  k + k : add_le_add (h _) (h _)
    ... = 2 * k : (two_mul _).symm },
end

Ruben Van de Velde (Aug 27 2020 at 15:23):

Btw, I was hoping linarith could solve 0 < ∥g y∥ given 1 < ∥g y∥, but apparently not. Should it?

Rob Lewis (Aug 27 2020 at 15:41):

To prove hgy? It does for me.

Ruben Van de Velde (Aug 27 2020 at 15:42):

Now it does for me too. I wonder what went wrong before

Stanislas Polu (Aug 27 2020 at 15:57):

Fantastic! Do people find the term proofs more readable with practice?

Bryan Gin-ge Chen (Aug 27 2020 at 15:59):

In my case at least, "more readable", but still not really "readable".

Patrick Massot (Aug 27 2020 at 16:49):

Ruben, when you hit something that looks like an API hole, it's even nicer if you try to fix it by opening a mathlib PR. It seems your desperately missed:

lemma real.le_supr {ι : Type*} {f : ι  } {b : } (h :  i, f i  b) (i) : f i  supr f :=
begin
  apply real.le_Sup,
  { use b,
    rintros - z, rfl,
    exact h _ },
  exact set.mem_range_self i,
end

lemma real.supr_le_ub {ι : Type*} [nonempty ι] {f : ι  } {b : } (h :  i, f i  b) : supr f  b :=
begin
  apply real.Sup_le_ub,
  inhabit ι,
  use [f $ default ι, set.mem_range_self _],
  rintros - z, rfl,
  apply h
end

Ideally a PR would of course also include the infi variants.

Ruben Van de Velde (Aug 27 2020 at 16:55):

Oh, I started from Johan's code and didn't think of using supr at all, I'll take a look at those

Patrick Massot (Aug 27 2020 at 16:56):

I just tried to write a readable proof (using the above lemmas).

example (f g :   )
  (hf1 :  x,  y, (f (x+y) + f(x-y)) = 2 * f(x) * g(y))
  (hf2 :  y, |f(y)|  1)
  (hf3 :  x, f(x)  0)
  (y : ) :
  |g(y)|  1 :=
begin
  obtain x, hx := hf3,
  set k := supr (λ x, |f x|),
  have h :  x, |f x|  k := real.le_supr hf2,
  by_contradiction H, push_neg at H,
  have hgy : 0 < |g y|,
    by linarith,
  have k_pos : 0 < k := lt_of_lt_of_le (norm_pos_iff.mpr hx) (h x),
  have : k / |g y| < k := (div_lt_iff hgy).mpr (lt_mul_of_one_lt_right k_pos H),
  have : k  k / |g y|,
  { suffices :  x, |f x|  k / |g y|, from real.supr_le_ub this,
    intro x,
    suffices : 2 * (|f x| * |g y|)  2 * k,
      by rwa [le_div_iff hgy, mul_le_mul_left zero_lt_two],
    calc 2 * (|f x| * |g y|)
        = |2 * f x * g y|           : by simp [abs_mul, mul_assoc]
    ... = |f (x + y) + f (x - y)|   : by rw hf1
    ...  |f (x + y)| + |f (x - y)| : abs_add _ _
    ...  2 * k                     : by linarith [h (x+y), h (x -y)] },
  linarith
end

Ruben Van de Velde (Aug 27 2020 at 19:58):

#3959

Ruben Van de Velde (Aug 28 2020 at 09:42):

I realized the hf2 hypothesis is unnecessarily strong - we only need that |f| is bounded from above, and that formulation lets us use le_csupr directly:

example (f g :   )
  (hf1 :  x,  y, (f (x+y) + f(x-y)) = 2 * f(x) * g(y))
  (hf2 : bdd_above (set.range (λ x, |f x|)))
  (hf3 :  x, f(x)  0)
  (y : ) :
  |g(y)|  1 :=
begin
  obtain x, hx := hf3,
  set k := supr (λ x, |f x|),
  have h :  x, |f x|  k := le_csupr hf2,
  by_contradiction H, push_neg at H,
  have hgy : 0 < |g y|,
    by linarith,
  have k_pos : 0 < k := lt_of_lt_of_le (norm_pos_iff.mpr hx) (h x),
  have : k / |g y| < k := (div_lt_iff hgy).mpr (lt_mul_of_one_lt_right k_pos H),
  have : k  k / |g y|,
  { suffices :  x, |f x|  k / |g y|, from csupr_le this,
    intro x,
    suffices : 2 * (|f x| * |g y|)  2 * k,
      by rwa [le_div_iff hgy, mul_le_mul_left zero_lt_two],
    calc 2 * (|f x| * |g y|)
        = |2 * f x * g y|           : by simp [abs_mul, mul_assoc]
    ... = |f (x + y) + f (x - y)|   : by rw hf1
    ...  |f (x + y)| + |f (x - y)| : abs_add _ _
    ...  2 * k                     : by linarith [h (x+y), h (x -y)] },
  linarith
end

Last updated: Dec 20 2023 at 11:08 UTC