Proving triangle inequality

Stream: new members

[ambiso]

Hi,

I'm trying to prove a relatively simple inequality (that I hope to be true), and on the path to that I want to prove the triangle theorem.
Unfortunately, I'm kind of lost what tactics or existing theorems to use to help me get there.

This is the final theorem I want to prove:

theorem my_ineq (a b u t: ℚ) : (0≤a ∧ a≤1 ∧ 0≤b ∧ b≤1 ∧ 0≤u ∧ u≤1 ∧ 1≤t ∧ u≤a ∧ a≤t*u) → |a-b| ≤ |u-b| + (t-1)*u := by sorry

I currently have:

import data.rat.basic
import data.rat.order
import algebra.abs

#check (abs_add : ∀ a b : ℚ, |a + b| ≤ |a| + |b|)
theorem triangle_ineq (a b c : ℚ) : |a-b| ≤ |a-c| + |c-b| := by sorry

Can I use the abs_add proposition(?) to help me in the proof? Why does it not require any explicit proof for the #check?

I'd appreciate any help or pointers to relevant material that I can use.
I've completed parts of https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/, but have no experience in handling rationals. I was hoping the existing theorems could help me, but I failed to find e.g. the triangle inequality.

[Notification Bot]

This topic was moved here from #general > Proving triangle inequality by Eric Wieser.

[Eric Wieser]

Can I use the abs_add proposition(?) to help me in the proof?

Yes, definitely! What values do you want to use for a and b?

Why does it not require any explicit proof for the #check?

You gave the explicit proof, it was abs_add!

[Eric Wieser]

Perhaps this will help:

import data.rat.basic
import data.rat.order
import algebra.abs

theorem triangle_ineq (a b c : ℚ) : |a-b| ≤ |a-c| + |c-b| :=
begin
  have : ∀ a b : ℚ, |a + b| ≤ |a| + |b| := abs_add,
  -- now you have `abs_add` visible in your goal view, and can use the tactics
  -- you learnt from the natural number game
  sorry,
end