Skip to content

feat(Geometry/Euclidean/Projection): characteristic property #30698

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open

feat(Geometry/Euclidean/Projection): characteristic property #30698

Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
c4f608e
feat(Geometry/Euclidean/Projection): characteristic property
jsm28 Oct 19, 2025
6fcc7d1
Use `Subtype.coe_inj`
jsm28 Oct 19, 2025
f84640a
Add version for point given in subtype
jsm28 Oct 19, 2025
29f4f21
Update Mathlib/Geometry/Euclidean/Projection.lean
jsm28 Oct 20, 2025
d061e26
Further simplify code
jsm28 Oct 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 30 additions & 0 deletions Mathlib/Geometry/Euclidean/Projection.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -276,6 +276,36 @@ theorem orthogonalProjection_vsub_orthogonalProjection (s : AffineSubspace ℝ P
rw [← neg_vsub_eq_vsub_rev, inner_neg_right,
orthogonalProjection_vsub_mem_direction_orthogonal s p c hc, neg_zero]

/-- The characteristic property of the orthogonal projection. This form is typically more
convenient to use than `inter_eq_singleton_orthogonalProjection`. -/
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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

@jsm28 jsm28 Oct 19, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

@eric-wieser eric-wieser Oct 19, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added that version and renamed this one.

constructor
· rintro rfl
exact ⟨orthogonalProjection_mem _, vsub_orthogonalProjection_mem_direction_orthogonal _ _⟩
· rintro ⟨hqs, hpq⟩
have hq : q ∈ mk' p s.directionᗮ := by
rwa [mem_mk', ← neg_mem_iff, neg_vsub_eq_vsub_rev]
suffices q ∈ ({(orthogonalProjection s p : P)} : Set P) by
simpa [eq_comm] using this
rw [← inter_eq_singleton_orthogonalProjection]
simp only [Set.mem_inter_iff, SetLike.mem_coe]
exact ⟨hqs, hq⟩

/-- A condition for two points to have the same orthogonal projection onto a given subspace. -/
lemma orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem {s : AffineSubspace ℝ P}
[Nonempty s] [s.direction.HasOrthogonalProjection] {p q : P} :
orthogonalProjection s p = orthogonalProjection s q ↔ p -ᵥ q ∈ s.directionᗮ := by
suffices (orthogonalProjection s p : P) = orthogonalProjection s q ↔
p -ᵥ q ∈ s.directionᗮ by
simpa using this
rw [orthogonalProjection_eq_iff_mem]
simp only [SetLike.coe_mem, true_and]
rw [← s.directionᗮ.add_mem_iff_left (x := p -ᵥ q)
(vsub_orthogonalProjection_mem_direction_orthogonal s q)]
simp

/-- Adding a vector to a point in the given subspace, then taking the
orthogonal projection, produces the original point if the vector was
in the orthogonal direction. -/
Expand Down
Loading