IMO 1972 B2

Stream: general

[Stanislas Polu]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Stanislas Polu]

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]

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]

Thanks!!

[Stanislas Polu]

Awesome to get me started :thank_you:

[Mario Carneiro]

I think there was a thread on this in the past

[Mario Carneiro]

I think I was thinking of another proof assistant ;)

[Stanislas Polu]

You have to start somewhere :)

[Patrick Massot]

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]

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

[Stanislas Polu]

Nice catch :)

[Ruben Van de Velde]

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]

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]

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

[Ruben Van de Velde]

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]

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

[Rob Lewis]

To prove hgy? It does for me.

[Ruben Van de Velde]

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

[Stanislas Polu]

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

[Bryan Gin-ge Chen]

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

[Patrick Massot]

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]

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]

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]

#3959

[Ruben Van de Velde]

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