feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality for angles

[LessnessRandomness]

This PR continues the work from #24206.

Original PR: #24206

[LessnessRandomness]

Comments from Original PR #24206

This section contains 10 comment(s) from the original PR, excluding bot comments.

---

@github-actions (2025-04-19 19:02 UTC):

PR summary 6a858d8eb6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (new file)	1798

---

Declarations diff

+ InnerProductGeometry.angle_triangle
+ angle_triangle
+ angle_triangle_aux2
+ angle_unit_left
+ angle_unit_right
+ inner_eq_neg_sq_norm_iff
+ inner_eq_sq_norm_iff
+ inner_orthoDir_nonneg
+ inner_orthoDir_zero
+ inner_product_of_units_as_cos
+ inner_sub_smul_eq_zero
+ neg_one_le_inner_unit_unit
+ norm_of_unit
+ orthoDir
+ orthoDir_aux_1
+ orthoDir_unit_left
+ orthoDir_unit_right
+ orthoDir_zero
+ sin_as_inner_product
+ unit
+ unit_eq_id_of_norm_one
+ unit_smul_of_pos
+ unit_unit
+ unit_zero
+ zero_orthoDir

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

@urkud (2025-04-28 05:21 UTC):
There is a competing PR #22265

---

@urkud (2025-04-28 05:24 UTC):
Please coordinate with @Timeroot on how to merge your PRs into 1 PR that gets reviewed&merged.

---

@LessnessRandomness (2025-05-03 19:54 UTC):
Right now Timeroot is very busy, we will talk/coordinate when they have free time (week or two later).

---

@Timeroot (2025-05-09 19:06 UTC):
Alright, I think Ilmārs's is sufficiently clean in terms of the imports that I don't have much to add from my proof - I did the add the EuclideanGeometry.angle_triangle version of the theorem, and did some (slightly opinionated) cleanup, hope that was welcome. :)

---

@LessnessRandomness (2025-05-13 12:43 UTC):
@jsm28 Hello! Busy right now :( will fix the problems starting from the weekend.

Thank you for your work!

---

@LessnessRandomness (2025-05-20 22:29 UTC):
Ok, so... I talked to @Timeroot and he agreed to take over this PR. I'm just too busy. :(

---

@Timeroot (2025-06-10 02:15 UTC):
I added my cleanup work, I have some things I'm not sure about regarding whether putting unit (or this other function, orthoDir) elsewhere in mathlib.

@jsm28 , @LessnessRandomness said he might have some time again, can you advise on the best ways to continue?

---

@LessnessRandomness (2025-06-10 22:53 UTC):
I will have time in July (probably all the month) or about three weeks from now.

---

@LessnessRandomness (2025-06-18 23:16 UTC):
Big thank you to @Timeroot!

It has happened that I'm free already.
@jsm28, what should I do next?

[github-actions]

PR summary 39996ca4db

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
17 files Mathlib.Analysis.Complex.Angle Mathlib.Geometry.Euclidean.Angle.Bisector Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Congruence Mathlib.Geometry.Euclidean.Simplex Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Triangle	1
Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (new file)	2087

---

Declarations diff

+ InnerProductGeometry.angle_le_angle_add_angle
+ angle_le_angle_add_angle
+ angle_le_angle_add_angle_of_norm_one
+ angle_normalize_left
+ angle_normalize_right
+ inner_eq_cos_angle_of_norm_one
+ inner_eq_neg_one_iff_of_norm_one
+ inner_self_eq_one_of_norm_one
+ neg_one_le_real_inner_of_norm_one
+ real_inner_le_one_of_norm_one

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[jsm28]

Next I suggest moving the more generally meaningful definitions and lemmas about vectors in inner product spaces, or in real normed spaces in general in the case of unit and many of its lemmas, to other files (existing or new), probably in a series of separate PRs that this one can then depend on. Note the point from previous discussion that unit (meaningful in any real normed space) should probably be renamed, and take care about the naming convention for these lemmas in general.

[LessnessRandomness]

unit is renamed to normalized.
Also did some renaming, trying to follow the Mathlib standards.

Now thinking about where and how to put different lemmas and defs into different files.

[LessnessRandomness]

1. I believe that lemmas about unit length vectors have no independent value, so in the end I decided to put them in the same file as the main result (in section named UnitVectorAngles). Am I right to do this?

2. The definition private noncomputable def ortho (y x : V) : V := x - ⟪x, y⟫ • y at Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean gives an useful vector and is meant only for unit length vector y. It can be thought as a part of Gram-Schmidt ortogonalization process, I believe, but I don't need the full Gram-Schmidt, imo, so I hope that this definition is okay.

[themathqueen]

Suggested change

	have H := neg_le_of_abs_le (abs_real_inner_le_norm x y)
	simp_all
	simpa [hx, hy] using neg_le_of_abs_le (abs_real_inner_le_norm x y)

[LessnessRandomness]

Thank you, @themathqueen!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[JovanGerb]

What happened here? Why is it now "criteion"?

[LessnessRandomness]

It seems that I accidentally deleted a letter during resolving merge conflict, most probably. Sorry.

[LessnessRandomness]

Great, I missed the second "Schwartz" that had to be changed to "Schwarz", too.

[JovanGerb]

I think this is a bit of a funny simp lemma. Could you put this in a separate PR and benchmark it to make sure it doesn't have a bad performance impact?

[LessnessRandomness]

Maybe some days (at most a week) later, as I've caught cold/flu/smth and can't think efficiently enough. :(
Still, how does one benchmark a PR?

[JovanGerb]

Ah that's too bad, I had a cold the last few days too!

To benchmark a PR, you simply write a comment saying !bench. A helpful bot will do everything for you and comment the results after about an hour.