From b7367ced63fa27ceffa3ff286e0765d7c37a1694 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 4 Sep 2023 01:28:44 -0500 Subject: [PATCH] =?UTF-8?q?feat:=20kernel=20of=20`orthogonalProjection=20K?= =?UTF-8?q?`=20is=20`K=E1=97=AE`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Analysis/InnerProductSpace/Projection.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index 4f238cdc4e181..35349905d6386 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -580,6 +580,17 @@ theorem orthogonalProjection_eq_self_iff {v : E} : (orthogonalProjection K v : E · simp #align orthogonal_projection_eq_self_iff orthogonalProjection_eq_self_iff +@[simp] +theorem orthogonalProjection_eq_zero_iff {v : E} : orthogonalProjection K v = 0 ↔ v ∈ Kᗮ := by + refine ⟨fun h ↦ ?_, fun h ↦ Subtype.eq <| eq_orthogonalProjection_of_mem_orthogonal + (zero_mem _) ?_⟩ + · simpa [h] using sub_orthogonalProjection_mem_orthogonal (K := K) v + · simpa + +@[simp] +theorem ker_orthogonalProjection : LinearMap.ker (orthogonalProjection K) = Kᗮ := by + ext; exact orthogonalProjection_eq_zero_iff + theorem LinearIsometry.map_orthogonalProjection {E E' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (p : Submodule 𝕜 E) [HasOrthogonalProjection p] [HasOrthogonalProjection (p.map f.toLinearMap)]