English
If an orthogonal family has a complete decomposition, the ambient space decomposes as a direct sum of the subspaces via their orthogonal projections.
Русский
Если ортогональная совокупность даёт полное разложение, пространство распадается на прямую сумму подплощад через их ортогональные проекции.
LaTeX
$$$\\text{decomposition } V$$$
Lean4
/-- Characterization of minimizers in the projection on a subspace, in the real case.
Let `u` be a point in a real inner product space, and let `K` be a nonempty subspace.
Then point `v` minimizes the distance `‖u - v‖` over points in `K` if and only if
for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`).
This is superseded by `norm_eq_iInf_iff_inner_eq_zero` that gives the same conclusion over
any `RCLike` field.
-/
theorem norm_eq_iInf_iff_real_inner_eq_zero (K : Submodule ℝ F) {u : F} {v : F} (hv : v ∈ K) :
(‖u - v‖ = ⨅ w : (↑K : Set F), ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0 :=
Iff.intro
(by
intro h
have h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 :=
by
rwa [norm_eq_iInf_iff_real_inner_le_zero] at h
exacts [K.convex, hv]
intro w hw
have le : ⟪u - v, w⟫_ℝ ≤ 0 := by
let w' := w + v
have : w' ∈ K := Submodule.add_mem _ hw hv
have h₁ := h w' this
have h₂ : w' - v = w := by simp only [w', add_neg_cancel_right, sub_eq_add_neg]
rw [h₂] at h₁
exact h₁
have ge : ⟪u - v, w⟫_ℝ ≥ 0 := by
let w'' := -w + v
have : w'' ∈ K := Submodule.add_mem _ (Submodule.neg_mem _ hw) hv
have h₁ := h w'' this
have h₂ : w'' - v = -w := by simp only [w'', add_neg_cancel_right, sub_eq_add_neg]
rw [h₂, inner_neg_right] at h₁
linarith
exact le_antisymm le ge)
(by
intro h
have : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 := by
intro w hw
let w' := w - v
have : w' ∈ K := Submodule.sub_mem _ hw hv
have h₁ := h w' this
exact le_of_eq h₁
rwa [norm_eq_iInf_iff_real_inner_le_zero]
exacts [Submodule.convex _, hv])
