## Stream: new members

### Topic: Fiddly calculations.

#### Wrenna Robson (Nov 13 2020 at 13:16):

I'm trying to do another kata on uniform continuity. I have got to the point where I can see the end - but I'm tripping up on fiddly calculations. This is my file.

import data.real.basic

/-
Uniform continuity
A function f(x) is said to be uniform continuous if it is continuous
with the additional condition that the choice of δ depends on ε only
-/
def uniform_continuous (f : ℝ → ℝ) :=
∀ ε > 0, ∃ δ > 0, ∀ x y, abs (x - y) < δ → abs (f x - f y) < ε

/-
Lipschitz functions
A function f(x) is said to be Lipschitz if there is L s.t.
|f(x) - f(y)| ≤ L|x - y| for any x, y.
-/
def lipschitz (f : ℝ → ℝ) :=
∃ L, ∀ x y, abs (f x - f y) ≤ L * abs (x - y)

theorem uniform_continuous_of_lipschitz {f} (hf : lipschitz f) :
uniform_continuous f :=
begin
intros ε ε_pos,
cases hf with L hL,
have δ_pos : ε/(abs(L)+1) > 0,
{
apply div_pos ε_pos,
calc
0   ≤ abs L : by apply abs_nonneg
... < abs L + 1 : by linarith,

},
use ε/(abs(L)+1),
split,
exact δ_pos,
intros x y hxy,
specialize hL x y,
sorry,
end


I would prefer not to be messing around with specific axioms and was hoping linarith could do this for me, but it doesn't seem to. What's the nicest way to do this?

#### Wrenna Robson (Nov 13 2020 at 13:21):

(In a sense the fact that the Lipshitz definition here doesn't explictly require L to be non-negative is part of the issue...)

#### Kevin Buzzard (Nov 13 2020 at 17:06):

linarith doesn't do it because it involves multiplication.

#### Kevin Buzzard (Nov 13 2020 at 17:13):

What's the maths proof here?

    calc abs (f x - f y) ≤ L * abs (x - y) : hL
...                  < L * (ε / (abs L + 1)) : sorry
...                  = ε * (L / (abs L + 1)) : by field_simp; ring
...                  < ε : sorry


finishes it modulo the two sorries, but to prove the sorries I guess you need that L>0. From hL we see that if L<0 then abs(x-y) is going to have to be 0 meaning x=y and in this case we can solve the goal directly. If L=0 then we can solve the goal using hL, and if L>0 then the calc route above will work.

#### Kevin Buzzard (Nov 13 2020 at 17:32):

theorem uniform_continuous_of_lipschitz {f} (hf : lipschitz f) :
uniform_continuous f :=
begin
intros ε ε_pos,
cases hf with L hL,
have δ_pos : ε/(abs(L)+1) > 0,
{
apply div_pos ε_pos,
calc
0   ≤ abs L : by apply abs_nonneg
... < abs L + 1 : by linarith,

},
use ε/(abs(L)+1),
split,
exact δ_pos,
intros x y hxy,
specialize hL x y,
rcases lt_trichotomy L 0 with (hneg | rfl | hpos),
{ -- L < 0
suffices : abs (x - y) = 0,
{ rw [abs_eq_zero, sub_eq_zero] at this,
rw this,
convert ε_pos,
simp },
by_contra non0,
have hxy3 : 0 ≤ abs (x - y) := abs_nonneg (x - y),
rw le_iff_eq_or_lt at hxy3,
cases hxy3, exact non0 hxy3.symm,
have hnonsense : (0 : ℝ) < 0 := calc
(0 : ℝ) ≤ abs (f x - f y) : abs_nonneg _
...     ≤ L * abs (x - y) : hL
... < 0 : mul_neg_of_neg_of_pos hneg hxy3,
exact lt_irrefl 0 hnonsense },
{ -- L = 0
rw zero_mul at hL,
linarith },
{ -- L > 0
have hL2 : L / (abs L + 1) < 1,
rw [div_lt_one, abs_of_pos hpos], linarith,
calc abs (f x - f y) ≤ L * abs (x - y) : hL
...                  < L * (ε / (abs L + 1)) : by rwa mul_lt_mul_left hpos
...                  = ε * (L / (abs L + 1)) : by field_simp; ring
...                  < ε * 1 : by rwa mul_lt_mul_left ε_pos
...                  = ε : mul_one _ }
end


Did I miss a trick?

#### Wrenna Robson (Nov 13 2020 at 19:18):

This is quite similar to what I did in the end.

theorem uniform_continuous_of_lipschitz {f} (hf : lipschitz f) :
uniform_continuous f :=
begin
intros ε ε_pos,
cases hf with L hL,
have abs_L_plus_1_pos : 0 < abs L + 1,
{
calc
0   ≤ abs L : by apply abs_nonneg
... < abs L + 1 : by linarith,
},
have δ_pos : ε/(abs(L)+1) > 0, from div_pos ε_pos abs_L_plus_1_pos,
use [ε/(abs(L)+1), δ_pos],
intros x y hxy,
specialize hL x y,
have h1 : L * abs (x - y) ≤ (abs L + 1) * abs (x - y),
{
apply mul_le_mul_of_nonneg_right,
calc
L   ≤ abs L : le_abs_self L
... ≤ abs L + 1 : by linarith,
apply abs_nonneg,
},
have h2 : (abs L + 1) * abs (x - y) < (abs L + 1) * ( ε / (abs L + 1) ),
{
apply mul_lt_mul_of_pos_left,
assumption,
assumption,
},
have h3 : (abs L + 1) * ( ε / (abs L + 1) ) = ε,
{
apply mul_div_cancel',
linarith,
},
linarith,
end


#### Wrenna Robson (Nov 13 2020 at 19:18):

As you can see I really don't like calc mode...

#### Wrenna Robson (Nov 13 2020 at 19:26):

You can avoid worrying about the sign of L, though.

#### Patrick Massot (Nov 13 2020 at 19:57):

@Wrenna Robson you can learn some compression tricks from this version of your proof:

theorem uniform_continuous_of_lipschitz {f} (hf : lipschitz f) :
uniform_continuous f :=
begin
intros ε ε_pos,
cases hf with L hL,
have abs_L_plus_1_pos : 0 < abs L + 1, by linarith [abs_nonneg L],
use [ε/(abs(L)+1), div_pos ε_pos (by linarith [abs_nonneg L])],
intros x y hxy,
have h1 : L * abs (x - y) ≤ (abs L + 1) * abs (x - y),
{ apply mul_le_mul_of_nonneg_right ;
linarith [le_abs_self L, abs_nonneg (x - y)] },
have h2 : (abs L + 1) * abs (x - y) < (abs L + 1) * ( ε / (abs L + 1) ),
from mul_lt_mul_of_pos_left ‹_› ‹_›,
have h3 : (abs L + 1) * ( ε / (abs L + 1) ) = ε,
from mul_div_cancel' _ (by linarith),
linarith [hL x y]
end


Thank you!

#### Sebastien Gouezel (Nov 13 2020 at 19:59):

Or have a look at docs#lipschitz_with.uniform_continuous

#### Wrenna Robson (Nov 13 2020 at 20:02):

@Patrick Massot Two things I don't follow there.

#### Wrenna Robson (Nov 13 2020 at 20:02):

What does the semicolon do, and what are the ‹_› doing?

#### Mario Carneiro (Nov 13 2020 at 20:07):

‹_› is shorthand for by assumption

#### Mario Carneiro (Nov 13 2020 at 20:08):

i.e. assumption as a term instead of a tactic

Huh! Alright.

#### Mario Carneiro (Nov 13 2020 at 20:08):

tac1; tac2 runs tac2 on all subgoals produced by tac1

#### Wrenna Robson (Nov 13 2020 at 20:08):

Perfect. Thank you.

#### Wrenna Robson (Nov 13 2020 at 20:09):

And thank you for your patience. I'm continuing to really enjoy Lean!

#### Wrenna Robson (Nov 13 2020 at 21:20):

I do struggle a bit with converting "well, I can just see how I'd do that in words" into the Lean-world: currently bumping at another kata to do with primes which is like that.

#### Wrenna Robson (Nov 13 2020 at 21:21):

I can see why all the things I need to be true are true to give me my result.

#### Wrenna Robson (Nov 13 2020 at 21:25):

But actually, mmm, showing them in good order in Lean... a trickier task!

#### Wrenna Robson (Nov 13 2020 at 21:43):

If I have other questions on different kata, is it better etiquette here to start a new thread or continue this one? (Ironically I sent this twice...)

#### Bryan Gin-ge Chen (Nov 13 2020 at 21:48):

I'd say feel free to make new threads.

Last updated: May 12 2021 at 23:13 UTC