Orthogonal projection

Stream: maths

[Heather Macbeth]

I'd like to redefine the orthogonal projection in an inner product space. Currently (docs#orthogonal_projection) the orthogonal projection from E to K is a linear map from E to E. It would be useful to me if it were instead a linear map from E to K. Here's a (un-golfed) branch experimenting with the change: branch#redefine-orthogonal-projection

Some consequences: Currently the junk value of the orthogonal projection (if K is not complete) is the identity map. This gets changed to be the zero map. This in turn causes problems in defining the affine orthogonal projection, because (lack of basepoints) there is no such thing as the zero map onto an affine subspace. So I keep the affine orthogonal projection in its old definition, a map from the full space to itself. This is a little inconsistent, but since practically all lemmas already required the hypothesis of completeness of the subspace, it doesn't affect many proofs.

Any comments, advice, preferences, objections?

[Yury G. Kudryashov]

E.g., you can assume [nonempty K] and use the const affine map.

[Heather Macbeth]

OK, I made a start on this, adding [nonempty K] as a precondition for the affine orthogonal projection, and fixing most of the sorries in geometry.euclidean.basic. But as I did this, the following thought occurred to me: one could instead require [complete_space K] as a precondition for both the standard and affine orthogonal projections, and then it wouldn't be necessary to define a junk value for the orthogonal projection at all. Any objections to this?

[Heather Macbeth]

The main issue is that this means using typeclass inference on a subtype ([nonempty K] rather than (K : set E).nonempty, [complete_space K] rather than is_complete (K : set E)), and I have somewhere picked up the impression that this is bad form.

[Joseph Myers]

Higher-level results using orthogonal projections, or using reflection in an affine subspace which is built on orthogonal projections, are less likely to have any hypotheses of things being complete or nonempty, as those things tend to follow from other hypotheses. E.g. geometry.euclidean.monge_point uses reflection, but never mentions complete or nonempty anywhere; various lemmas in geometry.euclidean.circumcenter also use reflection or orthogonal_projection without needing to mention that the subspace in question has the right properties. Can type class inference be made to deduce those properties for the spaces mentioned in lemma statements (affine_span of various finite nonempty sets of points, for example), so that it's still possible to write the existing higher-level lemma statements using those functions without needing to add extra type class hypotheses to those lemmas?

[Heather Macbeth]

@Joseph Myers thank you for thinking about this!

I was thinking that we could declare instances such as this:

instance (s : finset E) : complete_space (submodule.span 𝕜 (s : set E)) :=
@finite_dimensional.complete 𝕜 _ (submodule.span 𝕜 (s : set E)) _ _ _ (span_of_finite 𝕜 (finset.finite_to_set s))

(I wrote the "standard" rather than affine version because I am more familiar with that theory). I don't know if this is a dangerous instance in any way? It passes #lint.

[Heather Macbeth]

See the note at finite_dimensional.complete for why I'm a little hesitant about this instance -- but if I understand correctly, the unknown metavariable issue mentioned in that context would not apply here.

[Yury G. Kudryashov]

Yes, 𝕜 is already in the type.

[Heather Macbeth]

In fact, since the field is fixed to ℝ throughout the Euclidean geometry libraries, would it be safe to declare an instance like this?

import geometry.euclidean.basic

open affine_subspace finite_dimensional

variables {V : Type*} [inner_product_space ℝ V]
variables {P : Type*} [metric_space P] [normed_add_torsor V P]

include V

instance (s : affine_subspace ℝ P) [finite_dimensional ℝ s.direction] : complete_space s.direction :=
finite_dimensional.complete ℝ s.direction

[Yury G. Kudryashov]

Why do you need affine_subspace here? AFAIR, we already have an instance deducing complete_space V from finite_dimensional \R V

[Heather Macbeth]

There is docs#finite_dimensional.complete, but this is a lemma, not an instance, because of the unknown metavariable issue.

[Heather Macbeth]

I was saying that in contexts where the field is known, such as in the Euclidean geometry libraries, it seems it would be safe to upgrade it to an instance?

[Sebastien Gouezel]

Over the reals, it's already registered as an instance.

example {E : Type*} [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :
  complete_space E := by apply_instance

(through docs#finite_dimensional.proper_real). It also applies over the complexes as all the instances to see a complex vector space as a real vector space are already there:

example {E : Type*} [normed_group E] [normed_space ℂ E] [finite_dimensional ℂ E] :
  complete_space E := by apply_instance

[Sebastien Gouezel]

That's a pretty impressive instance search, by the way, and it only takes 68ms. Before the fork and Gabriel's work, I doubt it would have succeeded.

[Joseph Myers]

Thanks. Together with finite_dimensional instances such as those in linear_algebra.affine_space.finite_dimensional that ought to be able to deal with deducing complete_space where needed (but maybe more nonempty instances will be needed so that type class inference can deduce that affine subspaces are nonempty, so can be coerced to affine spaces, so that orthogonal projection onto them can be defined).

[Heather Macbeth]

#5408

[Heather Macbeth]

@Joseph Myers, could you look through this, in addition to whichever maintainer takes this on?