## 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


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

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 _ _
... = 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 _ _
... = 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,
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


#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,
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