Proved triangle inequality for angles

Stream: new members

[Ilmārs Cīrulis]

Finally proved triangle inequality (which is marked TODO) from https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.html

import Mathlib.Data.Real.StarOrdered
import Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic


open InnerProductGeometry


variable {V: Type}
variable [NormedAddCommGroup V]
variable [InnerProductSpace ℝ V]

noncomputable def unit (x: V): V := ‖x‖⁻¹ • x

theorem norm_of_unit {x: V} (H: x ≠ 0): ‖unit x‖ = 1 := by
  unfold unit; rw [norm_smul]; simp
  have H0: ‖x‖ ≠ 0 := by simp; exact H
  field_simp

theorem inner_product_of_units_as_cos {x y: V} (Hx: ‖x‖ = 1) (Hy: ‖y‖ = 1):
    @inner ℝ V _ x y = Real.cos (angle x y) := by
  rw [cos_angle, Hx, Hy]; simp

theorem inner_sq_of_unit {x: V} (Hx: ‖x‖ = 1): inner x x = (1: ℝ) := by
  rw [inner_eq_one_iff_of_norm_one Hx Hx]

theorem aux0 {x y: V} (Hx: ‖x‖ = 1) (Hy: ‖y‖ = 1):
    let u := unit (x - @inner ℝ V _ x y • y)
    inner x u ^ 2 + inner x y ^ 2 = (1: ℝ) := by
  intro u; unfold u unit
  rw [real_inner_smul_right, inner_sub_right, real_inner_smul_right]
  obtain H | H := em (x = y)
  . rw [H]; rw [inner_sq_of_unit Hy]; simp
  . obtain H0 | H0 := em (x = - y)
    . rw [H0]; simp; rw [inner_sq_of_unit Hy]; simp
    . rw [inner_sq_of_unit Hx]
      have H1: ‖x - @inner ℝ V _ x y • y‖ ≠ 0 := by
        simp; intro H2; rw [sub_eq_zero] at H2
        rw [H2, norm_smul, Hy] at Hx
        simp at Hx
        apply eq_or_eq_neg_of_abs_eq at Hx
        obtain Hx | Hx := Hx
        . rw [Hx] at H2; simp at H2; tauto
        . rw [Hx] at H2; simp at H2; tauto
      field_simp; rw [<- real_inner_self_eq_norm_sq]
      rw [inner_sub_left, inner_sub_right, inner_sub_right]
      rw [real_inner_smul_right, real_inner_smul_left]
      rw [real_inner_smul_right, real_inner_smul_left]
      rw [real_inner_comm x y]
      rw [inner_sq_of_unit Hx, inner_sq_of_unit Hy]
      ring

theorem aux1 {x y: V} (Hx: ‖x‖ = 1) (Hy: ‖y‖ = 1):
    (0: ℝ) ≤ inner x (unit (x - @inner ℝ V _ x y • y)) := by
  unfold unit; rw [real_inner_smul_right]
  have H := norm_nonneg (x - @inner ℝ V _ x y • y)
  apply inv_nonneg_of_nonneg at H
  apply mul_nonneg H ?_
  rw [inner_sub_right, real_inner_smul_right, inner_sq_of_unit Hx, <- sq]
  simp; rw [inner_product_of_units_as_cos Hx Hy]
  exact Real.abs_cos_le_one (angle x y)

theorem sin_as_inner_product {x y: V} (Hx: ‖x‖ = 1) (Hy: ‖y‖ = 1):
    let u := unit (x - @inner ℝ V _ x y • y)
    @inner ℝ V _ x u = Real.sin (angle x y) := by
  intro u; unfold u
  have H0 := aux0 Hx Hy; simp at H0
  nth_rw 2 [inner_product_of_units_as_cos Hx Hy] at H0
  rw [Real.cos_sq'] at H0
  have H0: Real.sin (angle x y) ^ 2 = inner x (unit (x - @inner ℝ V _ x y • y)) ^ 2 := by
    linarith
  rw [sq_eq_sq_iff_abs_eq_abs, ] at H0
  rw [abs_of_nonneg (aux1 Hx Hy)] at H0
  rw [abs_of_nonneg (sin_angle_nonneg x y)] at H0
  exact H0.symm

theorem aux3 {x y: V} (Hx: ‖x‖ = 1) (Hy: ‖y‖ = 1) (H: inner x y = (1: ℝ)):
    x = y := by
  rw [inner_product_of_units_as_cos Hx Hy] at H
  rw [cos_eq_one_iff_angle_eq_zero] at H
  rw [angle_eq_zero_iff] at H
  obtain ⟨H, r, H0, H1⟩ := H
  rw [H1, norm_smul, Hx] at Hy; simp at Hy
  rw [abs_of_pos H0] at Hy
  rw [Hy] at H1; simp at H1; exact H1.symm

theorem aux4 {x y: V} (Hx: ‖x‖ = 1) (Hy: ‖y‖ = 1) (H: inner x y = (-1: ℝ)):
    x = - y := by
  rw [inner_product_of_units_as_cos Hx Hy] at H
  rw [cos_eq_neg_one_iff_angle_eq_pi] at H
  rw [angle_eq_pi_iff] at H
  obtain ⟨H, r, H0, H1⟩ := H
  rw [H1, norm_smul, Hx] at Hy; simp at Hy
  rw [abs_of_neg H0, neg_eq_iff_eq_neg] at Hy
  rw [Hy] at H1; simp at H1; rw [H1]; simp

theorem aux5 {x y: V} (Hx: ‖x‖ = 1) (Hy: ‖y‖ = 1):
    let u := unit (x - @inner ℝ V _ x y • y)
    x = Real.cos (angle x y) • y + Real.sin (angle x y) • u := by
  simp; rw [<- sin_as_inner_product Hx Hy, <- inner_product_of_units_as_cos Hx Hy]
  unfold unit
  rw [real_inner_smul_right]
  rw [inner_sub_right, real_inner_smul_right]
  rw [inner_sq_of_unit Hx, <- sq]
  rw [<- smul_assoc]
  obtain H | H := em (‖x - @inner ℝ V _ x y • y‖ = 0)
  . rw [H]; simp
    simp at H; rw [sub_eq_zero] at H; exact H
  . field_simp
    rw [<- sq, <- real_inner_self_eq_norm_sq]
    rw [inner_sub_left, inner_sub_right, inner_sub_right]
    rw [real_inner_smul_left, real_inner_smul_right]
    rw [real_inner_smul_left, real_inner_smul_right]
    rw [real_inner_comm x y]
    rw [inner_sq_of_unit Hx, inner_sq_of_unit Hy]
    simp
    have H1: inner x y ≠ (1: ℝ) := by
      intro H2; apply H; simp; rw [H2]; simp; rw [sub_eq_zero]
      apply aux3 Hx Hy H2
    have H2: inner x y ≠ (-1: ℝ) := by
      intro H3; apply H; simp; rw [H3]; simp
      rw [add_eq_zero_iff_eq_neg]
      apply aux4 Hx Hy H3
    rw [<- sq]
    have H3: (1: ℝ) - inner x y ^ 2 ≠ 0 := by
      intro H3; rw [sub_eq_zero] at H3; symm at H3
      simp at H3; tauto
    field_simp

theorem aux6 (x: V) {y: V} (Hy: ‖y‖ = 1):
    let u := unit (x - @inner ℝ V _ x y • y)
    inner y u = (0: ℝ) := by
  simp; unfold unit; rw [real_inner_smul_right]; simp
  rw [inner_sub_right, real_inner_smul_right]
  rw [inner_sq_of_unit Hy, real_inner_comm x y]; simp

theorem aux7 {x y: ℝ} (Hx: x ∈ Set.Icc 0 Real.pi) (Hy: y ∈ Set.Icc 0 Real.pi) (H: Real.cos x ≤ Real.cos y):
    y ≤ x := by
  rw [<- Real.arccos_cos Hy.1 Hy.2, <- Real.arccos_cos Hx.1 Hx.2]
  obtain H0 | H0 := eq_or_lt_of_le H
  . rw [<- Real.arccos_cos Hy.1 Hy.2, <- Real.arccos_cos Hx.1 Hx.2, H0]
  . apply (Real.strictAntiOn_arccos (Real.cos_mem_Icc x) (Real.cos_mem_Icc y)) at H0
    linarith

theorem aux8 {x y: ℝ} (Hx: x ∈ Set.Icc (-1) 1) (Hy: y ∈ Set.Icc (-1) 1):
    x * y ∈ Set.Icc (-1) 1 := by
  obtain ⟨Hx1, Hx2⟩ := Hx
  obtain ⟨Hy1, Hy2⟩ := Hy
  constructor <;> nlinarith

theorem aux9 {x y: V} (Hx: x ≠ 0) (Hy: y ≠ 0):
    angle x y = angle (unit x) (unit y) := by
  have H: 0 < ‖x‖⁻¹ := by simp; exact Hx
  have H0: 0 < ‖y‖⁻¹ := by simp; exact Hy
  unfold unit; rw [angle_smul_left_of_pos _ _ H, angle_smul_right_of_pos _ _ H0]

theorem aux10 (x y: V): (-1: ℝ) ≤ inner (unit x) (unit y) := by
  obtain H | H := em (x = 0)
  . rw [H]; unfold unit; simp
  . obtain H0 | H0 := em (y = 0)
    . rw [H0]; unfold unit; simp
    . rw [inner_product_of_units_as_cos (norm_of_unit H) (norm_of_unit H0)]
      apply Real.neg_one_le_cos

theorem angle_triangle_for_units {x y z: V} (Hx: ‖x‖ = 1) (Hy: ‖y‖ = 1) (Hz: ‖z‖ = 1):
    angle x z ≤ angle x y + angle y z := by
  obtain H | H := em (angle x y + angle y z ≤ Real.pi)
  . have H0: 0 ≤ angle x y + angle y z := by linarith [angle_nonneg x y, angle_nonneg y z]
    have H1: @inner ℝ V _ x z = inner x z := by rfl
    nth_rw 2 [aux5 Hx Hy] at H1
    nth_rw 2 [aux5 Hz Hy] at H1
    rw [inner_add_left, inner_add_right, inner_add_right] at H1
    rw [real_inner_smul_left, real_inner_smul_right] at H1
    rw [inner_sq_of_unit Hy] at H1; simp at H1
    rw [real_inner_smul_left, real_inner_smul_right] at H1
    rw [aux6 z Hy] at H1; simp at H1
    rw [real_inner_smul_left, real_inner_smul_right] at H1
    rw [real_inner_comm y, aux6 x Hy] at H1; simp at H1
    rw [real_inner_smul_left, real_inner_smul_right] at H1
    have H2 := aux10 (x - @inner ℝ V _ x y • y) (z - @inner ℝ V _ z y • y)
    have H3: 0 ≤ Real.sin (angle x y) * Real.sin (angle y z) :=
      (mul_nonneg (sin_angle_nonneg x y) (sin_angle_nonneg y z))
    have H4: Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z) := by
      rw [Real.cos_add, <- inner_product_of_units_as_cos Hx Hz, H1, angle_comm z y]; simp
      rw [add_assoc, le_add_iff_nonneg_right, <- mul_assoc]
      rw [<- mul_add_one]
      apply (mul_nonneg H3); linarith
    apply aux7 ⟨H0, H⟩ ⟨angle_nonneg x z, angle_le_pi x z⟩ H4
  . linarith [angle_le_pi x z]

theorem angle_triangle (x y z: V): angle x z ≤ angle x y + angle y z := by
  obtain H | H := em (x = 0)
  . rw [H]; simp; apply angle_nonneg
  . obtain H0 | H0 := em (y = 0)
    . rw [H0]; simp; apply angle_le_pi
    . obtain H1 | H1 := em (z = 0)
      . rw [H1]; simp; apply angle_nonneg
      . rw [aux9 H H1, aux9 H H0, aux9 H0 H1]
        have Hx := norm_of_unit H
        have Hy := norm_of_unit H0
        have Hz := norm_of_unit H1
        apply angle_triangle_for_units Hx Hy Hz

[Ilmārs Cīrulis]

I don't know if it is good enough to put into Mathlib, though. But at least it's done. :partying_face:

Now I can go to sleep. Finally. :D :sweat_smile:

[Joseph Myers]

Does this have lighter import dependencies than #22265 (which currently puts this inequality in a separate file to avoid large import increases for code not needing this lemma)?

[Ilmārs Cīrulis]

O, that's the another approach (using fact that determinant of Gram matrix), which definitely makes for much shorter proof.

I believe that "my" proof is lighter (but longer), as it doesn't use any facts about matrices/linear algebra and doesn't need import Mathlib.LinearAlgebra.Matrix.PosDef.

[Ilmārs Cīrulis]

I found my approach through math.stackexchange.com which also lead me to these lecture notes

Same as author of #22265 , I had trouble proving it myself.

[Ilmārs Cīrulis]

#24206 - made my PR too