feat(Geometry/Euclidean/Projection): characteristic property

[jsm28]

Add a lemma

lemma orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s]
    [s.direction.HasOrthogonalProjection] {p q : P} :
    orthogonalProjection s p = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ := by

that gives the characteristic property of the orthogonal projection in a more convenient form to use than the existing
inter_eq_singleton_orthogonalProjection (from which it is derived).

Deduce a lemma orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem about equality of two projections onto the same subspace.

---

[github-actions]

PR summary 8aa3ccd118

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ coe_orthogonalProjection_eq_iff_mem
+ orthogonalProjection_eq_iff_mem
+ orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem

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

[eric-wieser]

If this spelling is the more convenient one, should orthogonalProjection have been defined somehow in terms of this specification instead? If you think the answer is yes, can you add a TODO?

[jsm28]

In my view, the right way to redefine orthogonalProjection is in #27378 (which may have been abandoned by the author). But any definition in terms of orthogonal projection for submodules is unlikely to achieve the nicest form of the characteristic property.

[eric-wieser]

Is there a version of this without the coercion on the LHS?

[jsm28]

I'm not sure what that would look like; if you say q is in the subtype of s then you remove q ∈ s from the RHS but now need a coercion to subtract from p and then assert membership of s.directionᗮ, and that's a slightly different lemma statement but it's not obvious there are any particular advantages to it.

[eric-wieser]

Indeed I'm thinking of orthogonalProjection s p = q ↔ p -ᵥ (q : P) ∈ s.directionᗮ :=, which seems like it's vaguely useful in that it is simpler. Certainly I'm not saying we should drop your current version.

That would also cause your lemma to gain a coe_ prefix, which is probably a good idea anyway.

[jsm28]

Added that version and renamed this one.