strict triangle inequality in Euclidean space

Stream: Is there code for X?

[David Renshaw]

This proof, that affine independence implies a strict triangle inequality, is much longer than I had initially hoped it would be. I feel like I might be missing something in the AffineIndependent API.

Does anyone have any ideas about how to simplify the proof?

import Mathlib.Analysis.Convex.StrictConvexBetween
import Mathlib.Geometry.Euclidean.Triangle
import Mathlib.Tactic

example (T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))) :
    dist (T.points 0) (T.points 1) <
       dist (T.points 1) (T.points 2) + dist (T.points 0) (T.points 2) := by
  let a := dist (T.points 1) (T.points 2)
  let b := dist (T.points 0) (T.points 2)
  let c := dist (T.points 0) (T.points 1)
  have h10 : c ≤ a + b := by
    have := dist_triangle (T.points 0) (T.points 2) (T.points 1)
    rw [dist_comm (T.points 2)] at this
    linarith
  suffices H : c ≠ a + b from lt_of_le_of_ne h10 H
  intro H
  symm at H
  unfold a b c at *
  rw [dist_comm (T.points 0), dist_comm (T.points 0)] at H
  rw [dist_add_dist_eq_iff] at H
  rw [←mem_segment_iff_wbtw] at H
  simp only [segment, Fin.isValue, exists_and_left, Set.mem_setOf_eq] at H
  obtain ⟨a, ha1, t, ht, ha3, ha4⟩ := H
  let w : Fin 3 -> ℝ
    | 0 => t
    | 1 => a
    | 2 => -1
  have hw0 : ∑ i : Fin 3, w i = 0 := by
    rw [Fin.sum_univ_three]
    simp only [w]
    linarith
  have hw1 : ∑ i, w i • T.points i = 0 := by
    rw [Fin.sum_univ_three]
    simp only [w, neg_smul, one_smul]
    rw [add_comm] at ha4
    exact add_neg_eq_zero.mpr ha4
  have h2 := AffineIndependent.eq_zero_of_sum_eq_zero T.independent hw0 hw1
  by_cases ht0 : t = 0
  · specialize h2 1 (by decide)
    simp only [w] at h2
    linarith
  · specialize h2 0 (by decide)
    simp only [w] at h2
    contradiction

[Eric Wieser]

Is this the same result that was posted about recently in another thread, which was also the same as another older thread?

[David Renshaw]

Maybe! Do you have a link?

[Eric Wieser]

#new members > Proved triangle inequality for angles @ 💬 and #22265, but I now see these are not the same.

[Eric Wieser]

I should have a much shorter proof in a few minutes

[Eric Wieser]

import Mathlib.Analysis.Convex.StrictConvexBetween
import Mathlib.Geometry.Euclidean.Triangle
import Mathlib.Tactic

variable {P V} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]

theorem dist_strict_triangle {ι} (i j k : ι) (h : Function.Injective ![i, j, k]) (T : ι → P) (hT : AffineIndependent ℝ T) :
    dist (T i) (T k) < dist (T i) (T j) + dist (T j) (T k) := by
  refine lt_of_le_of_ne' (dist_triangle _ _ _) ?_
  intro H
  rw [dist_add_dist_eq_iff] at H
  replace hT := hT.comp_embedding ⟨_, h⟩
  rw [affineIndependent_iff_not_collinear, Set.range_comp] at hT
  apply hT; clear hT
  convert H.symm.collinear using 1
  simp [Set.image_insert_eq]

[Eric Wieser]

Or maybe a more convenient form:

theorem AffineIndependent.dist_strict_triangle {Ti Tj Tk : P} (hT : AffineIndependent ℝ ![Ti, Tj, Tk]) :
    dist (Ti) (Tk) < dist (Ti) (Tj) + dist (Tj) (Tk) := by
  refine lt_of_le_of_ne' (dist_triangle _ _ _) ?_
  intro H
  rw [dist_add_dist_eq_iff] at H
  rw [affineIndependent_iff_not_collinear] at hT
  apply hT; clear hT
  convert H.symm.collinear using 1
  simp [Set.image_insert_eq]

theorem AffineIndependent.dist_strict_triangle' {ι} (i j k : ι) (h : Function.Injective ![i, j, k]) (T : ι → P) (hT : AffineIndependent ℝ T) :
    dist (T i) (T k) < dist (T i) (T j) + dist (T j) (T k) := by
  refine AffineIndependent.dist_strict_triangle ?_
  convert hT.comp_embedding ⟨_, h⟩ using 1
  exact FinVec.map_eq _ ![i, j, k]

[Eric Wieser]

Probably @Joseph Myers has opinions on what the best way to state this is

[David Renshaw]

Wow! Works well for me: https://github.com/dwrensha/compfiles/commit/55df28bb39309c5c78103d590da53e0d42fd3325

Thank you!

[David Renshaw]

I opened #24104 with @Eric Wieser 's two new theorems.

[David Renshaw]

On further reflection, I prefer Eric's initial suggestion, with a single dist_strict_triangle theorem. I've updated to pull request to reflect that preference.

[Eric Wieser]

I think probably we should have both; one is easier for forwards reasoning, the other backwards

[Eric Wieser]

There's perhaps the argument that they should be stated with Collinear instead