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