n-fold triangle inequality

Stream: new members

[Luigi Massacci]

Is there a nice way to one line something like this:

|a₁ + a₂ + ... + aₙ| ≤ |a₁| + |a₂| + ... + |aₙ| := by sorry

In my case n = 4 and it's only two calc lines manually, but maybe there's some tactic voodo to do that in one go.

[Ruben Van de Velde]

Does gcongr do it?

[Damiano Testa]

Not at a computer, but I would guess that something like repeat apply (abs_add_le ..).trans might work?

[Luigi Massacci]

Ruben Van de Velde said:

Does gcongr do it?

Assuming you do not mean something more sophisticated than this:

example (a b c d : ℝ) : |a + b + c + d| ≤ |a| + |b| + |c| + |d| := by
  gcongr

then the answer is gcongr did not make progress

@Damiano Testa repeat apply (abs_add ..).trans has the same effect as doing it once

[Damiano Testa]

Well, combining Ruben's suggestion with mine, you can do it as follows:

example (a b c d : ℝ) : |a + b + c + d| ≤ |a| + |b| + |c| + |d| := by
  repeat apply (abs_add_le ..).trans; gcongr; try exact abs_add a b

[Eric Wieser]

This works:

import Mathlib

open BigOperators
example (a b c d : ℝ) : |a + b + c + d| ≤ |a| + |b| + |c| + |d| := by
  simpa [Fin.sum_univ_succ, add_assoc] using Finset.abs_sum_le_sum_abs ![a, b, c, d] Finset.univ

[Luigi Massacci]

Damiano Testa said:

Well, combining Ruben's suggestion with mine, you can do it as follows:

example (a b c d : ℝ) : |a + b + c + d| ≤ |a| + |b| + |c| + |d| := by
  repeat apply (abs_add_le ..).trans; gcongr; try exact abs_add a b

And everyone lived happily ever after. Also thank you to @Eric Wieser