Skip to content

Commit 4b30dc1

Browse files
committed
chore(Analysis/InnerProductSpace/Projection): split file (#27851)
Splitting long file `Analysis.InnerProductSpace.Projection`: - Projection/Minimal: contains the Hilbert projection theorem and minimizer characterization. - Projection/Basic: contains the definitions for `HasOrthogonalProjection`, `othogonalProjection`, `starProjection` and pretty much everything concerning those. - Projection/Reflection: everything about `Submodule.reflection`. - Projection/Submodule: stuff like `K ⊔ Kᗮ = ⊤` for when `K` admits an orthogonal projection. - Projection/FiniteDimensional: stuff about orthogonal projections on finite-dimensional spaces (but also some lemmas that doesn't use `FiniteDimensional`). Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>
1 parent ed755e7 commit 4b30dc1

File tree

15 files changed

+1813
-1697
lines changed

15 files changed

+1813
-1697
lines changed

Mathlib.lean

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1638,7 +1638,11 @@ import Mathlib.Analysis.InnerProductSpace.Orthonormal
16381638
import Mathlib.Analysis.InnerProductSpace.PiL2
16391639
import Mathlib.Analysis.InnerProductSpace.Positive
16401640
import Mathlib.Analysis.InnerProductSpace.ProdL2
1641-
import Mathlib.Analysis.InnerProductSpace.Projection
1641+
import Mathlib.Analysis.InnerProductSpace.Projection.Basic
1642+
import Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
1643+
import Mathlib.Analysis.InnerProductSpace.Projection.Minimal
1644+
import Mathlib.Analysis.InnerProductSpace.Projection.Reflection
1645+
import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
16421646
import Mathlib.Analysis.InnerProductSpace.Rayleigh
16431647
import Mathlib.Analysis.InnerProductSpace.Semisimple
16441648
import Mathlib.Analysis.InnerProductSpace.Spectrum

Mathlib/Analysis/InnerProductSpace/Dual.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2020 Frédéric Dupuis. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Frédéric Dupuis
55
-/
6-
import Mathlib.Analysis.InnerProductSpace.Projection
6+
import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
77
import Mathlib.Analysis.Normed.Module.Dual
88
import Mathlib.Analysis.Normed.Group.NullSubmodule
99
import Mathlib.Topology.Algebra.Module.PerfectPairing

Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yury Kudryashov. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov
55
-/
6-
import Mathlib.Analysis.InnerProductSpace.Projection
6+
import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
77
import Mathlib.Dynamics.BirkhoffSum.NormedSpace
88

99
/-!

Mathlib/Analysis/InnerProductSpace/PiL2.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Joseph Myers, Sébastien Gouëzel, Heather Macbeth
55
-/
6-
import Mathlib.Analysis.InnerProductSpace.Projection
6+
import Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
77
import Mathlib.Analysis.Normed.Lp.PiLp
88
import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
99
import Mathlib.LinearAlgebra.UnitaryGroup

Mathlib/Analysis/InnerProductSpace/Projection.lean

Lines changed: 0 additions & 1689 deletions
This file was deleted.

Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean

Lines changed: 674 additions & 0 deletions
Large diffs are not rendered by default.

Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean

Lines changed: 406 additions & 0 deletions
Large diffs are not rendered by default.
Lines changed: 316 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,316 @@
1+
/-
2+
Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Zhouhang Zhou, Frédéric Dupuis, Heather Macbeth
5+
-/
6+
import Mathlib.Analysis.InnerProductSpace.Basic
7+
import Mathlib.Analysis.SpecificLimits.Basic
8+
9+
/-!
10+
# Existence of minimizers (Hilbert projection theorem)
11+
12+
This file shows the existence of minimizers (also known as the Hilbert projection theorem).
13+
This is the key tool that is used to define `Submodule.orthogonalProjection` in
14+
`Mathlib/Analysis/InnerProductSpace/Projection/Basic`.
15+
-/
16+
17+
variable {𝕜 E F : Type*} [RCLike 𝕜]
18+
variable [NormedAddCommGroup E] [NormedAddCommGroup F]
19+
variable [InnerProductSpace 𝕜 E] [InnerProductSpace ℝ F]
20+
21+
local notation "⟪" x ", " y "⟫" => inner 𝕜 x y
22+
local notation "absR" => @abs ℝ _ _
23+
24+
open Topology RCLike Real Filter InnerProductSpace
25+
26+
-- FIXME this monolithic proof causes a deterministic timeout with `-T50000`
27+
-- It should be broken in a sequence of more manageable pieces,
28+
-- perhaps with individual statements for the three steps below.
29+
/-- **Existence of minimizers**, aka the **Hilbert projection theorem**.
30+
31+
Let `u` be a point in a real inner product space, and let `K` be a nonempty complete convex subset.
32+
Then there exists a (unique) `v` in `K` that minimizes the distance `‖u - v‖` to `u`. -/
33+
theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h₁ : IsComplete K)
34+
(h₂ : Convex ℝ K) : ∀ u : F, ∃ v ∈ K, ‖u - v‖ = ⨅ w : K, ‖u - w‖ := fun u => by
35+
let δ := ⨅ w : K, ‖u - w‖
36+
letI : Nonempty K := ne.to_subtype
37+
have zero_le_δ : 0 ≤ δ := le_ciInf fun _ => norm_nonneg _
38+
have δ_le : ∀ w : K, δ ≤ ‖u - w‖ := ciInf_le ⟨0, Set.forall_mem_range.2 fun _ => norm_nonneg _⟩
39+
have δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖ := fun w hw => δ_le ⟨w, hw⟩
40+
-- Step 1: since `δ` is the infimum, can find a sequence `w : ℕ → K` in `K`
41+
-- such that `‖u - w n‖ < δ + 1 / (n + 1)` (which implies `‖u - w n‖ --> δ`);
42+
-- maybe this should be a separate lemma
43+
have exists_seq : ∃ w : ℕ → K, ∀ n, ‖u - w n‖ < δ + 1 / (n + 1) := by
44+
have hδ : ∀ n : ℕ, δ < δ + 1 / (n + 1) := fun n =>
45+
lt_add_of_le_of_pos le_rfl Nat.one_div_pos_of_nat
46+
have h := fun n => exists_lt_of_ciInf_lt (hδ n)
47+
let w : ℕ → K := fun n => Classical.choose (h n)
48+
exact ⟨w, fun n => Classical.choose_spec (h n)⟩
49+
rcases exists_seq with ⟨w, hw⟩
50+
have norm_tendsto : Tendsto (fun n => ‖u - w n‖) atTop (𝓝 δ) := by
51+
have h : Tendsto (fun _ : ℕ => δ) atTop (𝓝 δ) := tendsto_const_nhds
52+
have h' : Tendsto (fun n : ℕ => δ + 1 / (n + 1)) atTop (𝓝 δ) := by
53+
convert h.add tendsto_one_div_add_atTop_nhds_zero_nat
54+
simp only [add_zero]
55+
exact tendsto_of_tendsto_of_tendsto_of_le_of_le h h' (fun x => δ_le _) fun x => le_of_lt (hw _)
56+
-- Step 2: Prove that the sequence `w : ℕ → K` is a Cauchy sequence
57+
have seq_is_cauchy : CauchySeq fun n => (w n : F) := by
58+
rw [cauchySeq_iff_le_tendsto_0]
59+
-- splits into three goals
60+
let b := fun n : ℕ => 8 * δ * (1 / (n + 1)) + 4 * (1 / (n + 1)) * (1 / (n + 1))
61+
use fun n => √(b n)
62+
constructor
63+
-- first goal : `∀ (n : ℕ), 0 ≤ √(b n)`
64+
· intro n
65+
exact sqrt_nonneg _
66+
constructor
67+
-- second goal : `∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ √(b N)`
68+
· intro p q N hp hq
69+
let wp := (w p : F)
70+
let wq := (w q : F)
71+
let a := u - wq
72+
let b := u - wp
73+
let half := 1 / (2 : ℝ)
74+
let div := 1 / ((N : ℝ) + 1)
75+
have :
76+
4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ =
77+
2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) :=
78+
calc
79+
4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ =
80+
2 * ‖u - half • (wq + wp)‖ * (2 * ‖u - half • (wq + wp)‖) + ‖wp - wq‖ * ‖wp - wq‖ :=
81+
by ring
82+
_ =
83+
absR 2 * ‖u - half • (wq + wp)‖ * (absR 2 * ‖u - half • (wq + wp)‖) +
84+
‖wp - wq‖ * ‖wp - wq‖ := by
85+
rw [abs_of_nonneg]
86+
exact zero_le_two
87+
_ =
88+
‖(2 : ℝ) • (u - half • (wq + wp))‖ * ‖(2 : ℝ) • (u - half • (wq + wp))‖ +
89+
‖wp - wq‖ * ‖wp - wq‖ := by simp [norm_smul]
90+
_ = ‖a + b‖ * ‖a + b‖ + ‖a - b‖ * ‖a - b‖ := by
91+
rw [smul_sub, smul_smul, mul_one_div_cancel (_root_.two_ne_zero : (2 : ℝ) ≠ 0), ←
92+
one_add_one_eq_two, add_smul]
93+
simp only [one_smul]
94+
have eq₁ : wp - wq = a - b := (sub_sub_sub_cancel_left _ _ _).symm
95+
have eq₂ : u + u - (wq + wp) = a + b := by
96+
change u + u - (wq + wp) = u - wq + (u - wp)
97+
abel
98+
rw [eq₁, eq₂]
99+
_ = 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) := parallelogram_law_with_norm ℝ _ _
100+
have eq : δ ≤ ‖u - half • (wq + wp)‖ := by
101+
rw [smul_add]
102+
apply δ_le'
103+
apply h₂
104+
repeat' exact Subtype.mem _
105+
repeat' exact le_of_lt one_half_pos
106+
exact add_halves 1
107+
have eq₁ : 4 * δ * δ ≤ 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ := by
108+
simp_rw [mul_assoc]
109+
gcongr
110+
have eq₂ : ‖a‖ ≤ δ + div :=
111+
le_trans (le_of_lt <| hw q) (add_le_add_left (Nat.one_div_le_one_div hq) _)
112+
have eq₂' : ‖b‖ ≤ δ + div :=
113+
le_trans (le_of_lt <| hw p) (add_le_add_left (Nat.one_div_le_one_div hp) _)
114+
rw [dist_eq_norm]
115+
apply nonneg_le_nonneg_of_sq_le_sq
116+
· exact sqrt_nonneg _
117+
rw [mul_self_sqrt]
118+
· calc
119+
‖wp - wq‖ * ‖wp - wq‖ =
120+
2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) - 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ := by
121+
simp [← this]
122+
_ ≤ 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) - 4 * δ * δ := by gcongr
123+
_ ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ := by gcongr
124+
_ = 8 * δ * div + 4 * div * div := by ring
125+
positivity
126+
-- third goal : `Tendsto (fun (n : ℕ) => √(b n)) atTop (𝓝 0)`
127+
suffices Tendsto (fun x ↦ √(8 * δ * x + 4 * x * x) : ℝ → ℝ) (𝓝 0) (𝓝 0)
128+
from this.comp tendsto_one_div_add_atTop_nhds_zero_nat
129+
exact Continuous.tendsto' (by fun_prop) _ _ (by simp)
130+
-- Step 3: By completeness of `K`, let `w : ℕ → K` converge to some `v : K`.
131+
-- Prove that it satisfies all requirements.
132+
rcases cauchySeq_tendsto_of_isComplete h₁ (fun n => Subtype.mem _) seq_is_cauchy with
133+
⟨v, hv, w_tendsto⟩
134+
use v
135+
use hv
136+
have h_cont : Continuous fun v => ‖u - v‖ :=
137+
Continuous.comp continuous_norm (Continuous.sub continuous_const continuous_id)
138+
have : Tendsto (fun n => ‖u - w n‖) atTop (𝓝 ‖u - v‖) := by
139+
convert Tendsto.comp h_cont.continuousAt w_tendsto
140+
exact tendsto_nhds_unique this norm_tendsto
141+
142+
/-- Characterization of minimizers for the projection on a convex set in a real inner product
143+
space. -/
144+
theorem norm_eq_iInf_iff_real_inner_le_zero {K : Set F} (h : Convex ℝ K) {u : F} {v : F}
145+
(hv : v ∈ K) : (‖u - v‖ = ⨅ w : K, ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 := by
146+
letI : Nonempty K := ⟨⟨v, hv⟩⟩
147+
constructor
148+
· intro eq w hw
149+
let δ := ⨅ w : K, ‖u - w‖
150+
let p := ⟪u - v, w - v⟫_ℝ
151+
let q := ‖w - v‖ ^ 2
152+
have δ_le (w : K) : δ ≤ ‖u - w‖ := ciInf_le ⟨0, fun _ ⟨_, h⟩ => h ▸ norm_nonneg _⟩ _
153+
have δ_le' (w) (hw : w ∈ K) : δ ≤ ‖u - w‖ := δ_le ⟨w, hw⟩
154+
have (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1) : 2 * p ≤ θ * q := by
155+
have : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 :=
156+
calc ‖u - v‖ ^ 2
157+
_ ≤ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 := by
158+
simp only [sq]; apply mul_self_le_mul_self (norm_nonneg _)
159+
rw [eq]; apply δ_le'
160+
apply h hw hv
161+
exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel _ _]
162+
_ = ‖u - v - θ • (w - v)‖ ^ 2 := by
163+
have : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v) := by
164+
rw [smul_sub, sub_smul, one_smul]
165+
simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev]
166+
rw [this]
167+
_ = ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 := by
168+
rw [@norm_sub_sq ℝ, inner_smul_right, norm_smul]
169+
simp only [sq]
170+
change
171+
‖u - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) +
172+
absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
173+
‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)
174+
rw [abs_of_pos hθ₁]; ring
175+
have eq₁ :
176+
‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 =
177+
‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ) := by
178+
abel
179+
rw [eq₁, le_add_iff_nonneg_right] at this
180+
have eq₂ :
181+
θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
182+
θ * (θ * ‖w - v‖ ^ 2 - 2 * ⟪u - v, w - v⟫_ℝ) := by ring
183+
rw [eq₂] at this
184+
exact le_of_sub_nonneg (nonneg_of_mul_nonneg_right this hθ₁)
185+
by_cases hq : q = 0
186+
· rw [hq] at this
187+
have : p ≤ 0 := by
188+
have := this (1 : ℝ) (by simp) (by simp)
189+
linarith
190+
exact this
191+
· have q_pos : 0 < q := lt_of_le_of_ne (sq_nonneg _) fun h ↦ hq h.symm
192+
by_contra hp
193+
rw [not_le] at hp
194+
let θ := min (1 : ℝ) (p / q)
195+
have eq₁ : θ * q ≤ p :=
196+
calc
197+
θ * q ≤ p / q * q := mul_le_mul_of_nonneg_right (min_le_right _ _) (sq_nonneg _)
198+
_ = p := div_mul_cancel₀ _ hq
199+
have : 2 * p ≤ p :=
200+
calc
201+
2 * p ≤ θ * q := by
202+
exact this θ (lt_min (by simp) (div_pos hp q_pos)) (by simp [θ])
203+
_ ≤ p := eq₁
204+
linarith
205+
· intro h
206+
apply le_antisymm
207+
· apply le_ciInf
208+
intro w
209+
apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _)
210+
have := h w w.2
211+
calc
212+
‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, w - v⟫_ℝ := by linarith
213+
_ ≤ ‖u - v‖ ^ 2 - 2 * ⟪u - v, w - v⟫_ℝ + ‖w - v‖ ^ 2 := by
214+
rw [sq]
215+
refine le_add_of_nonneg_right ?_
216+
exact sq_nonneg _
217+
_ = ‖u - v - (w - v)‖ ^ 2 := (@norm_sub_sq ℝ _ _ _ _ _ _).symm
218+
_ = ‖u - w‖ * ‖u - w‖ := by
219+
have : u - v - (w - v) = u - w := by abel
220+
rw [this, sq]
221+
· change ⨅ w : K, ‖u - w‖ ≤ (fun w : K => ‖u - w‖) ⟨v, hv⟩
222+
apply ciInf_le
223+
use 0
224+
rintro y ⟨z, rfl⟩
225+
exact norm_nonneg _
226+
227+
namespace Submodule
228+
229+
variable (K : Submodule 𝕜 E)
230+
231+
/-- Existence of projections on complete subspaces.
232+
Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace.
233+
Then there exists a (unique) `v` in `K` that minimizes the distance `‖u - v‖` to `u`.
234+
This point `v` is usually called the orthogonal projection of `u` onto `K`.
235+
-/
236+
theorem exists_norm_eq_iInf_of_complete_subspace (h : IsComplete (↑K : Set E)) :
237+
∀ u : E, ∃ v ∈ K, ‖u - v‖ = ⨅ w : (K : Set E), ‖u - w‖ := by
238+
letI : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
239+
letI : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
240+
let K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
241+
exact exists_norm_eq_iInf_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex
242+
243+
/-- Characterization of minimizers in the projection on a subspace, in the real case.
244+
Let `u` be a point in a real inner product space, and let `K` be a nonempty subspace.
245+
Then point `v` minimizes the distance `‖u - v‖` over points in `K` if and only if
246+
for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`).
247+
This is superseded by `norm_eq_iInf_iff_inner_eq_zero` that gives the same conclusion over
248+
any `RCLike` field.
249+
-/
250+
theorem norm_eq_iInf_iff_real_inner_eq_zero (K : Submodule ℝ F) {u : F} {v : F} (hv : v ∈ K) :
251+
(‖u - v‖ = ⨅ w : (↑K : Set F), ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0 :=
252+
Iff.intro
253+
(by
254+
intro h
255+
have h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 := by
256+
rwa [norm_eq_iInf_iff_real_inner_le_zero] at h
257+
exacts [K.convex, hv]
258+
intro w hw
259+
have le : ⟪u - v, w⟫_ℝ ≤ 0 := by
260+
let w' := w + v
261+
have : w' ∈ K := Submodule.add_mem _ hw hv
262+
have h₁ := h w' this
263+
have h₂ : w' - v = w := by
264+
simp only [w', add_neg_cancel_right, sub_eq_add_neg]
265+
rw [h₂] at h₁
266+
exact h₁
267+
have ge : ⟪u - v, w⟫_ℝ ≥ 0 := by
268+
let w'' := -w + v
269+
have : w'' ∈ K := Submodule.add_mem _ (Submodule.neg_mem _ hw) hv
270+
have h₁ := h w'' this
271+
have h₂ : w'' - v = -w := by
272+
simp only [w'', add_neg_cancel_right, sub_eq_add_neg]
273+
rw [h₂, inner_neg_right] at h₁
274+
linarith
275+
exact le_antisymm le ge)
276+
(by
277+
intro h
278+
have : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 := by
279+
intro w hw
280+
let w' := w - v
281+
have : w' ∈ K := Submodule.sub_mem _ hw hv
282+
have h₁ := h w' this
283+
exact le_of_eq h₁
284+
rwa [norm_eq_iInf_iff_real_inner_le_zero]
285+
exacts [Submodule.convex _, hv])
286+
287+
/-- Characterization of minimizers in the projection on a subspace.
288+
Let `u` be a point in an inner product space, and let `K` be a nonempty subspace.
289+
Then point `v` minimizes the distance `‖u - v‖` over points in `K` if and only if
290+
for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`)
291+
-/
292+
theorem norm_eq_iInf_iff_inner_eq_zero {u : E} {v : E} (hv : v ∈ K) :
293+
(‖u - v‖ = ⨅ w : K, ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w⟫ = 0 := by
294+
letI : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
295+
letI : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
296+
let K' : Submodule ℝ E := K.restrictScalars ℝ
297+
constructor
298+
· intro H
299+
have A : ∀ w ∈ K, re ⟪u - v, w⟫ = 0 := (K'.norm_eq_iInf_iff_real_inner_eq_zero hv).1 H
300+
intro w hw
301+
apply RCLike.ext
302+
· simp [A w hw]
303+
· symm
304+
calc
305+
im (0 : 𝕜) = 0 := im.map_zero
306+
_ = re ⟪u - v, (-I : 𝕜) • w⟫ := (A _ (K.smul_mem (-I) hw)).symm
307+
_ = re (-I * ⟪u - v, w⟫) := by rw [inner_smul_right]
308+
_ = im ⟪u - v, w⟫ := by simp
309+
· intro H
310+
have : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0 := by
311+
intro w hw
312+
rw [real_inner_eq_re_inner, H w hw]
313+
exact zero_re
314+
exact (K'.norm_eq_iInf_iff_real_inner_eq_zero hv).2 this
315+
316+
end Submodule

0 commit comments

Comments
 (0)