Criterion for equality in the triangle inequality for angles

Stream: new members

[Ilmārs Cīrulis]

Does this exist somewhere? I mean, proven either in "paper and pen" proof somewhere on the Internet or maybe even in Mathlib in some form.

It seems correct to me (at least in nondegenerate cases).

import Mathlib

open InnerProductGeometry
open scoped RealInnerProductSpace

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

theorem thm {x y z : V} (Hx : x ≠ 0) (Hy : y ≠ 0) (Hz : z ≠ 0) (Hxz: angle x z ≠ Real.pi) :
    (∃ (kx kz : ℝ), 0 ≤ kx ∧ 0 ≤ kz ∧ y = kx • x + kz • z) ↔
    angle x z = angle x y + angle y z := by

  sorry

[Kevin Buzzard]

I don't think it's right when z=-kx in general, where k is a positive constant? Your description of y only allows it to be on the line through x and z but it can be anywhere in the plane.

[Ilmārs Cīrulis]

Aha, that case must be excluded then. Thank you!

[Ilmārs Cīrulis]

Edited to add additional hypothesis, that angle x z can't be Real.pi.

[Ilmārs Cīrulis]

So far I have managed only to prove partial result for the direction from the left to right.
See here.

There's the statement of this result:

import Mathlib

namespace tinkering

open InnerProductGeometry
open scoped RealInnerProductSpace

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

lemma aux10 {x y z : V} (Hx : x ≠ 0) (Hy : y ≠ 0) (Hz : z ≠ 0)
    (kx kz : ℝ) (Hkx : 0 < kx) (Hkz : 0 < kz) :
    angle x y ≠ 0 → angle x y ≠ Real.pi →
    angle y z ≠ 0 → angle y z ≠ Real.pi →
    angle x z ≠ Real.pi →
    y = kx • x + kz • z →
    angle x y + angle y z ≤ Real.pi →
    angle x z = angle x y + angle y z := by
  sorry

end tinkering

[Ilmārs Cīrulis]

I'm sure there's some better ways to approach proof of the criterion, but I don't know them.
For now I'm just tinkering for fun of exploration.

[Ilmārs Cīrulis]

This angle x y + angle y z ≤ Real.pi is one annoying constraint, but I don't know how to get rid of it.

[Ilmārs Cīrulis]

Proved this (which allows to remove the constraint). :partying_face:

import Mathlib

open InnerProductGeometry
open scoped RealInnerProductSpace

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

lemma aux09_1 {x y z : V} (Hx : x ≠ 0) (Hy : y ≠ 0) (Hz : z ≠ 0)
    {kx kz : ℝ} (Hkx : 0 < kx) (Hkz : 0 < kz) :
    angle x z ≠ 0 →
    angle x z ≠ Real.pi → y = kx • x + kz • z → angle x y + angle y z ≤ Real.pi := by
  sorry

[Ilmārs Cīrulis]

And now removed all nondegeneracy constraints (except angle x z ≠ Real.pi) and finally proved the left to right direction of the criterion.

import Mathlib

open InnerProductGeometry
open scoped RealInnerProductSpace

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

lemma aux11 {x y z : V} (Hx : x ≠ 0) (Hy : y ≠ 0) (Hz : z ≠ 0)
    (kx kz : ℝ) (Hkx : 0 < kx) (Hkz : 0 < kz) :
    angle x z ≠ Real.pi → y = kx • x + kz • z →
    angle x z = angle x y + angle y z := by
  sorry

The incredibly messy current version of the proof is here

[Ilmārs Cīrulis]

Finished the proof of the criterion in the following form. :partying_face:
Now it is sorry free, but still a giant mess that I will need to fix/refactor/etc. :sweat_smile:

import Mathlib

open InnerProductGeometry
open scoped RealInnerProductSpace

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

theorem thm {x y z : V} (Hx : x ≠ 0) (Hy : y ≠ 0) (Hz : z ≠ 0) (Hxz : angle x z ≠ Real.pi) :
    (∃ (kx kz : ℝ), 0 ≤ kx ∧ 0 ≤ kz ∧ y = kx • x + kz • z) ↔
    angle x z = angle x y + angle y z := by
  sorry

[Ilmārs Cīrulis]

The proof, cleaned up but still a draft (needs better names, and few lemmas better places), takes about 400+ lines. Is this result useful for Mathlib?

I put it in this in this branch of Mathlib fork for now (continued from the #26129): https://github.com/LessnessRandomness/mathlib4/tree/triangle_theorem_for_angles_advanced

[Jovan Gerbscheid]

Sounds like a nice result for mathlib. Although 400+ lines sounds like quite a lot for this.

[Ilmārs Cīrulis]

Yeah, I agree. I imagine that there definitely could be a shorter proof or at least parts of the proof by someone better at math.

(Also, it's down to about 360 lines now, because I had the same lemma twice. :sweat:)

[Jakub Nowak]

Isn't this generalization of InnerProductGeometry.angle_eq_angle_add_add_angle_add?
I feel like your theorem could be proved by induction on kx and kz and applications of InnerProductGeometry.angle_eq_angle_add_add_angle_add.

[Ilmārs Cīrulis]

O, taking a look!

[Ilmārs Cīrulis]

Wait, induction on kx and kz? I'm missing something possibly, but they are real numbers.

[Jakub Nowak]

Ah, sorry, nvm, I thought these are natural numbers.

[Jakub Nowak]

InnerProductGeometry.angle_eq_angle_add_add_angle_add is the same as your theorem for kx = kz = 1. I don't see how you could use it to prove your more general version, but maybe you could look at the proof to look for ideas how to make your proof simpler.

[Jakub Nowak]

Actually, it's only one implication of your theorem.
The angle x z = angle x y + angle y z → ∃ (kx kz : ℝ), 0 ≤ kx ∧ 0 ≤ kz ∧ y = kx • x + kz • z part sounds harder and I don't think there's anything like this in mathlib.

[Jovan Gerbscheid]

Yes I think one direction is an easy consequence of this lemma that I added recently, InnerProductGeometry.angle_eq_angle_add_add_angle_add. For the other direction I don't have too many ideas :)

[Ilmārs Cīrulis]

What's the proof sketch for this easy consequence? That should shorten my proof, then.

Sorry for being lazy or smth. :sweat_smile:

[Jakub Nowak]

Jovan Gerbscheid said:

Yes I think one direction is an easy consequence of this lemma that I added recently, InnerProductGeometry.angle_eq_angle_add_add_angle_add. For the other direction I don't have too many ideas :)

That was my first thought too, but now I can't see how to prove ∀ (kx ky : ℝ), 0 ≤ kx → 0 ≤ ky → angle x y = angle x (kx • x + ky • y) + angle y (kx • x + ky • y) just from angle x y = angle x (x + y) + angle y (x + y).

[Jakub Nowak]

Although, maybe it's not too hard to modify the proof of InnerProductGeometry.angle_eq_angle_add_add_angle_add to handle these additional coefficients?

[Jovan Gerbscheid]

We can substitute x := kx • x and y := ky • y, into the lemma, which I think essentially gives the result. Because scaling by a positive amount doesn't change the angle. And we should case split on kx being 0, and on ky being zero.

[Ilmārs Cīrulis]

Ok, let's try it. :) Will report soon.

[Jakub Nowak]

Ah, yes, you get angle (kx • x) (ky • y) = angle (kx • x) (kx x + ky • y) + angle (ky • y) (kx • x + ky • y) and it should just simp to angle x y = angle x (kx • x + ky • y) + angle y (kx • x + ky • y) because of InnerProductGeometry.angle_smul_right_of_pos and InnerProductGeometry.angle_smul_left_of_pos.
Smart! :D

[Ilmārs Cīrulis]

Nice, it works

Big thanks, that massively shortens the proof! :heart:

[Ilmārs Cīrulis]

Simultaneously happy and, dunno, humbled? :D

[Ilmārs Cīrulis]

About 180 lines less.

[Ilmārs Cīrulis]

Woop! :partying_face: Grinded the criterion theorem together with #26129 (which it is built on) down to 280 lines.

[Ilmārs Cīrulis]

Now the size seems reasonable. Thank you all again! :)

[Jovan Gerbscheid]

Does this mean you have refactored the code in #26129 so that it makes more sense to have a combined PR, or is it still separate?

[Ilmārs Cīrulis]

It would make some sense to have a combined PR, I believe, but for now it (the criterion part) still lives in the https://github.com/leanprover-community/mathlib4/compare/master...LessnessRandomness:mathlib4:triangle_theorem_for_angles_advanced branch

[Ilmārs Cīrulis]

It was one big mess at the start, that's the reason.

[Ilmārs Cīrulis]

I mean, it lives there as a combination that builds on the PR, in the same file (but is not a PR itself yet).

[Jovan Gerbscheid]

I made #32100 which proves one direction of this equality criterion, using the approach I described above. I also added a proof_wanted for the bidirectional version. Do you agree with this version?

[Ilmārs Cīrulis]

Yes, I agree. :slight_smile:

[Ilmārs Cīrulis]

Ok, then I wait for the #32100 to be merged into Mathlib and then try my best with a new PR that fills that `proof_wanted'.

[Ilmārs Cīrulis]

Was a bit impatient and tried to make a PR (#32116) that depends on #32100. Looks like it is okay, I believe?... :sweat_smile:

[Ruben Van de Velde]

Looks like you did it right, yes