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

#### 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: Aug 03 2023 at 10:10 UTC