Zulip Chat Archive

Stream: new members

Topic: Fiddly calculations.


view this post on Zulip 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?

view this post on Zulip 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...)

view this post on Zulip Kevin Buzzard (Nov 13 2020 at 17:06):

linarith doesn't do it because it involves multiplication.

view this post on Zulip 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.

view this post on Zulip 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,
        exact add_pos_of_nonneg_of_pos (abs_nonneg _) zero_lt_one,
      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?

view this post on Zulip 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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 19:18):

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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 19:26):

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

view this post on Zulip 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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 19:57):

Thank you!

view this post on Zulip Sebastien Gouezel (Nov 13 2020 at 19:59):

Or have a look at docs#lipschitz_with.uniform_continuous

view this post on Zulip Wrenna Robson (Nov 13 2020 at 20:02):

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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 20:02):

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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 20:07):

‹_› is shorthand for by assumption

view this post on Zulip Mario Carneiro (Nov 13 2020 at 20:08):

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

view this post on Zulip Wrenna Robson (Nov 13 2020 at 20:08):

Huh! Alright.

view this post on Zulip Mario Carneiro (Nov 13 2020 at 20:08):

tac1; tac2 runs tac2 on all subgoals produced by tac1

view this post on Zulip Wrenna Robson (Nov 13 2020 at 20:08):

Perfect. Thank you.

view this post on Zulip Wrenna Robson (Nov 13 2020 at 20:09):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Wrenna Robson (Nov 13 2020 at 21:25):

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

view this post on Zulip 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...)

view this post on Zulip 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