Fiddly calculations.

Stream: new members

[Wrenna Robson]

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]

(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]

linarith doesn't do it because it involves multiplication.

[Kevin Buzzard]

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]

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?

[Wrenna Robson]

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]

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

[Wrenna Robson]

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

[Patrick Massot]

@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

[Wrenna Robson]

Thank you!

[Sebastien Gouezel]

Or have a look at docs#lipschitz_with.uniform_continuous

[Wrenna Robson]

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

[Wrenna Robson]

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

[Mario Carneiro]

‹_› is shorthand for by assumption

[Mario Carneiro]

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

[Wrenna Robson]

Huh! Alright.

[Mario Carneiro]

tac1; tac2 runs tac2 on all subgoals produced by tac1

[Wrenna Robson]

Perfect. Thank you.

[Wrenna Robson]

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

[Wrenna Robson]

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]

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

[Wrenna Robson]

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

[Wrenna Robson]

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]

I'd say feel free to make new threads.