Ortogonal projection of point onto line/plane/etc.

Stream: new members

[Ilmārs Cīrulis]

What's the idiomatic way to define, for example, orthogonal projection of a point onto line through two different points? Or the projection of a point onto plane, formed by three points not on the same line?

Should I go through vectors and use Submodule.starProjection or maybe Submodule.orthogonalProjection? I'm still figuring them out.

[Ilmārs Cīrulis]

If I didn't mess it up, then the case of two points / line should be something like this:

import Mathlib

noncomputable def projection_of_point (A B1 B2 : EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) :=
  B1 + (ℝ ∙ (B2 -ᵥ B1)).starProjection (A -ᵥ B1)

[Ilmārs Cīrulis]

And something like this in the second case? :thinking:

import Mathlib

noncomputable def projection_of_point_onto_plane (A B1 B2 B3 : EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) :=
  B1 + (Submodule.span ℝ {B2 -ᵥ B1, B3 -ᵥ B1}).starProjection (A -ᵥ B1)

[Ilmārs Cīrulis]

Is is, probably, a case of #xy problem, because I'm thinking about https://en.wikipedia.org/wiki/Geometric_mean_theorem of right triangle.

[Joseph Myers]

For projection onto an affine subspace you want docs#EuclideanGeometry.orthogonalProjection - the case of a line has its own notation for the affine span line[ℝ, A, B] for the line through A and B, for more general sets of points you can use affineSpan (or create new notation plane[ℝ, A, B, C] for the span of three points if you want that case a lot, I suppose).