English
For a decidable index set, and finite-dimensional ambient space, DirectSum.IsInternal V is equivalent to a canonical orthogonality condition.
Русский
Для декидируемого множества индексов и конечном пространства, DirectSum.IsInternal V эквивалентно каноническому условию ортогональности.
LaTeX
$$$\\text{DirectSum.IsInternal } V \\iff (iSup V)^{\\perp} = 0$$$
Lean4
/-- Characterization of minimizers in the projection on a subspace.
Let `u` be a point in an 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`)
-/
theorem norm_eq_iInf_iff_inner_eq_zero {u : E} {v : E} (hv : v ∈ K) :
(‖u - v‖ = ⨅ w : K, ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w⟫ = 0 :=
by
letI : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
letI : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
let K' : Submodule ℝ E := K.restrictScalars ℝ
constructor
· intro H
have A : ∀ w ∈ K, re ⟪u - v, w⟫ = 0 := (K'.norm_eq_iInf_iff_real_inner_eq_zero hv).1 H
intro w hw
apply RCLike.ext
· simp [A w hw]
· symm
calc
im (0 : 𝕜) = 0 := im.map_zero
_ = re ⟪u - v, (-I : 𝕜) • w⟫ := (A _ (K.smul_mem (-I) hw)).symm
_ = re (-I * ⟪u - v, w⟫) := by rw [inner_smul_right]
_ = im ⟪u - v, w⟫ := by simp
· intro H
have : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0 := by
intro w hw
rw [real_inner_eq_re_inner, H w hw]
exact zero_re
exact (K'.norm_eq_iInf_iff_real_inner_eq_zero hv).2 this
