From c4f608e00fcbdcad32609e1970a334ee2c7161f7 Mon Sep 17 00:00:00 2001 From: Joseph Myers Date: Sun, 19 Oct 2025 21:39:41 +0000 Subject: [PATCH 1/5] feat(Geometry/Euclidean/Projection): characteristic property MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add a lemma ```lean 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). --- Mathlib/Geometry/Euclidean/Projection.lean | 30 ++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/Mathlib/Geometry/Euclidean/Projection.lean b/Mathlib/Geometry/Euclidean/Projection.lean index 510b163cb5b479..32cf838cd329f1 100644 --- a/Mathlib/Geometry/Euclidean/Projection.lean +++ b/Mathlib/Geometry/Euclidean/Projection.lean @@ -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 + 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. -/ From 6fcc7d172bbb84ed9c049115eaf08546f3893307 Mon Sep 17 00:00:00 2001 From: Joseph Myers Date: Sun, 19 Oct 2025 23:15:28 +0000 Subject: [PATCH 2/5] Use `Subtype.coe_inj` --- Mathlib/Geometry/Euclidean/Projection.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Projection.lean b/Mathlib/Geometry/Euclidean/Projection.lean index 32cf838cd329f1..254b4e14a9145f 100644 --- a/Mathlib/Geometry/Euclidean/Projection.lean +++ b/Mathlib/Geometry/Euclidean/Projection.lean @@ -297,10 +297,7 @@ lemma orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s] 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] + rw [← Subtype.coe_inj, 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)] From f84640a21fd18b6685281120ba080dce751c7aa7 Mon Sep 17 00:00:00 2001 From: Joseph Myers Date: Sun, 19 Oct 2025 23:51:42 +0000 Subject: [PATCH 3/5] Add version for point given in subtype --- Mathlib/Geometry/Euclidean/Projection.lean | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Projection.lean b/Mathlib/Geometry/Euclidean/Projection.lean index 254b4e14a9145f..ac65b2b8999f8b 100644 --- a/Mathlib/Geometry/Euclidean/Projection.lean +++ b/Mathlib/Geometry/Euclidean/Projection.lean @@ -276,9 +276,10 @@ 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] +/-- The characteristic property of the orthogonal projection, for a point given in the underlying +space. This form is typically more convenient to use than +`inter_eq_singleton_orthogonalProjection`. -/ +lemma coe_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 constructor @@ -293,11 +294,19 @@ lemma orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s] simp only [Set.mem_inter_iff, SetLike.mem_coe] exact ⟨hqs, hq⟩ +/-- The characteristic property of the orthogonal projection, for a point given in the relevant +subspace. 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 : P} {q : s} : + orthogonalProjection s p = q ↔ p -ᵥ q ∈ s.directionᗮ := by + simpa using coe_orthogonalProjection_eq_iff_mem (s := s) (p := p) (q := (q : P)) + /-- 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 - rw [← Subtype.coe_inj, orthogonalProjection_eq_iff_mem] + rw [← Subtype.coe_inj, coe_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)] From 29f4f21dcc551e3d8eeae51f2643f5253ef8d0ae Mon Sep 17 00:00:00 2001 From: Joseph Myers Date: Mon, 20 Oct 2025 00:04:46 +0000 Subject: [PATCH 4/5] Update Mathlib/Geometry/Euclidean/Projection.lean Co-authored-by: Eric Wieser --- Mathlib/Geometry/Euclidean/Projection.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Euclidean/Projection.lean b/Mathlib/Geometry/Euclidean/Projection.lean index ac65b2b8999f8b..43ffd883ff197c 100644 --- a/Mathlib/Geometry/Euclidean/Projection.lean +++ b/Mathlib/Geometry/Euclidean/Projection.lean @@ -306,7 +306,7 @@ lemma orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s] 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 - rw [← Subtype.coe_inj, coe_orthogonalProjection_eq_iff_mem] + rw [Subtype.ext_iff, coe_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)] From d061e2671dc668d1e8129246b3fce5e1170feebc Mon Sep 17 00:00:00 2001 From: Joseph Myers Date: Mon, 20 Oct 2025 00:09:06 +0000 Subject: [PATCH 5/5] Further simplify code --- Mathlib/Geometry/Euclidean/Projection.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Projection.lean b/Mathlib/Geometry/Euclidean/Projection.lean index 43ffd883ff197c..66955266b520db 100644 --- a/Mathlib/Geometry/Euclidean/Projection.lean +++ b/Mathlib/Geometry/Euclidean/Projection.lean @@ -306,9 +306,7 @@ lemma orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s] 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 - rw [Subtype.ext_iff, coe_orthogonalProjection_eq_iff_mem] - simp only [SetLike.coe_mem, true_and] - rw [← s.directionᗮ.add_mem_iff_left (x := p -ᵥ q) + rw [orthogonalProjection_eq_iff_mem, ← s.directionᗮ.add_mem_iff_left (x := p -ᵥ q) (vsub_orthogonalProjection_mem_direction_orthogonal s q)] simp