Skip to main content

Challenge 13: Reverse triangle inequality: ||x| - |y|| ≤ |x - y|

Also available in:

Español

Prove the reverse triangle inequality; that is, that for all real numbers \(x\) and \(y\), the following relation holds: \[ ||x| - |y|| ≤ |x - y| \]

To do so, complete the following Lean 4 theory:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (x y : ℝ)

example : |(|x| - |y|)| ≤ |x - y| :=
by sorry

1. Proof in natural language

To prove that \[ ||x| - |y|| ≤ |x - y| \] it suffices to prove these two inequalities \[ \begin{array}{l} |x| - |y| ≤ |x - y| \\ -(|x| - |y|) ≤ |x - y| \end{array} \]

The proof of the first one is \[ \begin{array}{llll} |x| - |y| &= |(x - y) + y| - |y| \\ &≤ (|x - y| + |y|) - |y| &&\text{[by the triangle inequality]}\\ &= |x - y| \end{array} \] and that of the second one is \[ \begin{array}{llll} -(|x| - |y|) &= |y| - |x| \\ &= |x - (x - y)| - |x| \\ &≤ (|x| + |x - y|) - |x| &&\text{[by the triangle inequality]}\\ &= |x - y| \end{array} \]

2. Proofs in Lean 4

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (x y : ℝ)

-- Proof 1
-- =======

example : |(|x| - |y|)| ≤ |x - y| :=
by
  grind

-- Proof 2
-- =======

example :
  |(|x| - |y|)| ≤ |x - y| :=
by
  rw [abs_le']
  -- ⊢ |x| - |y| ≤ |x - y| ∧ -(|x| - |y|) ≤ |x - y|
  constructor
  · -- ⊢ |x| - |y| ≤ |x - y|
    grind
  · -- ⊢ -(|x| - |y|) ≤ |x - y|
    grind

-- Proof 3
-- =======

example :
  |(|x| - |y|)| ≤ |x - y| :=
by
  rw [abs_le']
  -- ⊢ |x| - |y| ≤ |x - y| ∧ -(|x| - |y|) ≤ |x - y|
  constructor
  · -- ⊢ |x| - |y| ≤ |x - y|
    calc |x| - |y|
         = |(x - y) + y| - |y|   := by grind
       _ ≤ (|x - y| + |y|) - |y| := by grind
       _ = |x - y|               := by grind
  · -- ⊢ -(|x| - |y|) ≤ |x - y|
    calc -(|x| - |y|)
         = |y| - |x|             := by grind
       _ = |x - (x - y)| - |x|   := by grind
       _ ≤ (|x| + |x - y|) - |x| := by grind
       _ = |x - y|               := by grind

-- Proof 4
-- =======

example :
  |(|x| - |y|)| ≤ |x - y| :=
by
  rw [abs_le']
  -- ⊢ |x| - |y| ≤ |x - y| ∧ -(|x| - |y|) ≤ |x - y|
  constructor
  · -- ⊢ |x| - |y| ≤ |x - y|
    calc |x| - |y|
         = |(x - y) + y| - |y|   := by congr ; ring
       _ ≤ (|x - y| + |y|) - |y| := sub_le_sub_right (abs_add_le (x - y) y) |y|
       _ = |x - y|               := by ring
  · -- ⊢ -(|x| - |y|) ≤ |x - y|
    calc -(|x| - |y|)
         = |y| - |x|             := by ring
       _ = |x - (x - y)| - |x|   := by congr ; ring
       _ ≤ (|x| + |x - y|) - |x| := sub_le_sub_right (abs_sub x (x - y)) |x|
       _ = |x - y|               := by ring

-- Proof 5
-- =======

example :
  |(|x| - |y|)| ≤ |x - y| :=
by
  rw [abs_le']
  -- ⊢ |x| - |y| ≤ |x - y| ∧ -(|x| - |y|) ≤ |x - y|
  constructor
  · -- ⊢ |x| - |y| ≤ |x - y|
    calc |x| - |y|
         = |(x - y) + y| - |y|   := congrArg (|·| - |y|) (sub_add_cancel x y).symm
       _ ≤ (|x - y| + |y|) - |y| := sub_le_sub_right (abs_add_le (x - y) y) |y|
       _ = |x - y|               := add_sub_cancel_right |x - y| |y|
  · -- ⊢ -(|x| - |y|) ≤ |x - y|
    calc -(|x| - |y|)
         = |y| - |x|             := neg_sub |x| |y|
       _ = |x - (x - y)| - |x|   := congrArg (|·| - |x|) (sub_sub_self x y).symm
       _ ≤ (|x| + |x - y|) - |x| := sub_le_sub_right (abs_sub x (x - y)) |x|
       _ = |x - y|               := add_sub_cancel_left |x| |x - y|

-- Proof 6
-- =======

example : |(|x| - |y|)| ≤ |x - y| :=
abs_abs_sub_abs_le x y

-- Lemmas used
-- ===========

variable (f : ℝ → ℝ)
#check (abs_abs_sub_abs_le x y : |(|x| - |y|)| ≤ |x - y|)
#check (abs_add_le x y : |x + y| ≤ |x| + |y|)
#check (abs_le' : |x| ≤ y ↔ x ≤ y ∧ -x ≤ y)
#check (abs_sub x y : |x - y| ≤ |x| + |y|)
#check (add_sub_cancel_left x y : (x + y) - x = y)
#check (add_sub_cancel_right x y : (x + y) - y = x)
#check (congrArg f : x = y → f x = f y)
#check (neg_sub x y : -(x - y) = y - x)
#check (sub_add_cancel x y: (x - y) + y = x)
#check (sub_le_sub_right : x ≤ y → ∀ z, x - z ≤ y - z)
#check (sub_sub_self x y : x - (x - y) = y)

The following video explains step by step how the solutions are built:

You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.

3. Collaborative solutions

Have you found a proof that differs from the published ones? You can share it in the comments below by following these steps:

  • Write your proof in live.lean-lang.org and check that it compiles without errors.
  • Copy the code and post it in the comments of this entry, inside a Lean code block:
```lean
   -- your proof
```

Comments