# Zulip Chat Archive

## Stream: general

### Topic: linarith failure

#### Patrick Massot (Mar 05 2019 at 19:48):

@Rob Lewis Is the following expected?

example {K d : ℝ} (h : 0 ≤ K) (h' : 0 ≤ d) : 0 ≤ 2*K*d := begin -- linarith, fails :-( :-( :-( suffices : 0*0*0 ≤ 2*K*d, by simpa using this, apply mul_le_mul ; try { linarith }, apply mul_le_mul ; linarith , end

#### Kenny Lau (Mar 05 2019 at 19:48):

`mul_le_mul`

isn't linear is it

#### Patrick Massot (Mar 05 2019 at 19:51):

I thought `lin`

in `linarith`

stands for "life is nice"

#### Rob Lewis (Mar 05 2019 at 19:53):

I think the `try {linarith}`

line should be able to kill all the subgoals. It should recognize 0*0 as 0. Not sure what's failing, I'll take a look at it when I have time.

#### Rob Lewis (Mar 05 2019 at 19:53):

`try {simp; linarith}`

works for now.

#### Rob Lewis (Mar 05 2019 at 19:54):

And it certainly shouldn't work without you applying the first `mul_le_mul`

, as Kenny points out that isn't a linear goal.

#### Rob Lewis (Mar 05 2019 at 19:55):

Or, rather, `apply mul_le_mul; simp; linarith`

in the second line finishes the proof.

#### Patrick Massot (Mar 05 2019 at 19:58):

Thanks. I still wish we have better tools for such things, but linarith already goes a long way

#### Patrick Massot (Mar 05 2019 at 20:07):

My Lean day has been all about wishing computation were easy in Lean. I got upset and forced my way through the computation. It reminds me of my old chain rule days

#### Patrick Massot (Mar 05 2019 at 20:23):

The result is at: https://gist.github.com/PatrickMassot/82c69e2d4c30d0b7121f9fd46b5deed1 I'd be interested in a golfed version, if someone wants to practice computing in Lean. The main definition is:

open set variables {α : Type*} {β : Type*} [metric_space α] [metric_space β] def lipschitz_on_with (s : set α) (K : ℝ) (f : α → β) := 0 ≤ K ∧ ∀x y ∈ s, dist (f x) (f y) ≤ K * dist x y example (K : ℝ) (f : α → β) : lipschitz_with K f ↔ lipschitz_on_with univ K f := ⟨λ ⟨hK, h⟩, ⟨hK, λ x y _ _, h x y⟩, λ ⟨hK, h⟩, ⟨hK, λ x y, h x y (mem_univ x) (mem_univ y)⟩⟩

and the goal is to prove that any map which is K-Lipschitz on a ball extends to a map which globally 2K-Lipschitz

variables {E : Type*} [normed_space ℝ E] {F : Type*} [normed_space ℝ F] lemma lipschitz_extend_from_ball {a : E} {r : ℝ} {K : ℝ} {f : E → F} (h : lipschitz_on_with (closed_ball a r) K f) : ∃ g : E → F, (∀ x ∈ closed_ball a r, g x = f x) ∧ lipschitz_with (2*K) g

The motivation was a nice proof of the inverse function theorem. But much of the niceness of this proof relies on the fact that proving the above lemma is trivial. With a 200 lines long proof the lemma, the inverse function theorem proof looks less nice.

#### Rob Lewis (Mar 05 2019 at 21:49):

The 0*0 bug was easy, it's fixed now.

#### Rob Lewis (Mar 05 2019 at 21:53):

Although, now that I look at your original problem again, I think this would have worked even without the fix.

example {K d : ℚ} (h : 0 ≤ K) (h' : 0 ≤ d) : 0 ≤ 2*K*d := begin suffices : 0*0 ≤ 2*K*d, by simpa using this, apply mul_le_mul; linarith end

Last updated: May 13 2021 at 18:26 UTC