English
If x lies in the orthogonal sum of subspaces V_i, then the sum of their orthogonal projections equals x.
Русский
Если элемент x принадлежит ортогональной сумме подпространств V_i, то сумма ортогональных проекций по V_i равна x.
LaTeX
$$$\\sum_i (V_i)^{\\ast}\\!\\mathrm{starProjection}(x) = x$$$
Lean4
/-- If `x` lies within an orthogonal family `v`, it can be expressed as a sum of projections. -/
theorem sum_projection_of_mem_iSup [Fintype ι] {V : ι → Submodule 𝕜 E} [∀ i, CompleteSpace (V i)]
(hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (x : E) (hx : x ∈ iSup V) :
(∑ i, (V i).starProjection x) = x := by
induction hx using iSup_induction' with
| mem i x
hx =>
refine
(Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hij => ?_).trans (starProjection_eq_self_iff.mpr hx)
rw [starProjection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.coe_zero]
exact hV.isOrtho hij.symm hx
| zero => simp_rw [map_zero, Finset.sum_const_zero]
| add x y _ _ hx hy =>
simp_rw [map_add, Finset.sum_add_distrib]
exact congr_arg₂ (· + ·) hx hy
