feat(Geometry/Euclidean/SignedDist): signedDist between two points

[JovanGerb]

This PR defines signedDist, the signed distance between two points.

It redefines signedInfDist so that it uses signedDist.

The motivation is to use this in IMO2020Q6. Additionally this definition will be useful for properly reasoning about the power of a point

#mathlib4 > Signed distance between points

some comments:

• should signedDistLinear be private?
• should signedDist and signedInfDist be made continuous bunled maps in this PR?
• I'm not too happy about the hypothesis in signedDist_congr (h : ∃ r > (0 : ℝ), r • v = w). This relationship between v and w is a symmetric one that should have some API around it, similar to SameRay. It could also be spelled as (ℝ≥0 ∙ v) = ℝ≥0 ∙ w

---

[github-actions]

PR summary c35fbb5256

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ abs_signedDist_eq_dist_iff_vsub_mem_span
+ abs_signedDist_le_dist
+ signedDist
+ signedDist_anticomm
+ signedDist_apply
+ signedDist_apply_apply
+ signedDist_apply_linear
+ signedDist_apply_linear_apply
+ signedDist_congr
+ signedDist_eq_dist_iff_vsub_mem_span
+ signedDist_eq_zero_of_orthogonal
+ signedDist_le_dist
+ signedDist_left_congr
+ signedDist_linear_apply
+ signedDist_linear_apply_apply
+ signedDist_neg
+ signedDist_right_congr
+ signedDist_self
+ signedDist_smul
+ signedDist_triangle
+ signedDist_triangle_left
+ signedDist_triangle_right
+ signedDist_vadd_left
+ signedDist_vadd_left_swap
+ signedDist_vadd_right
+ signedDist_vadd_right_swap
+ signedDist_vadd_vadd
+ signedDist_vsub_self
+ signedDist_vsub_self_rev
+ signedDist_zero
+ signedInfDist_def
+ signedInfDist_eq_signedDist
+ signedInfDist_eq_signedDist_orthogonalProjection
+ signedInfDist_singleton
- signedInfDist_apply
- signedInfDist_linear
- signedInfDist_linear_apply

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).

[leanprover-community-bot-assistant]

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

[JovanGerb]

This has moved to #27260