English
Let E be a Hilbert space over 𝕜 and let v: ι → E be an orthonormal family. If the orthogonal complement of the span of {v_i} is {0}, then the Hilbert basis constructed from this orthogonal set coincides with the original family; i.e., the basis vectors are exactly v.
Русский
Пусть E — гильбертово пространство над 𝕜 и пусть v: ι → E образует ортонормированную систему. Если ортогональное дополнение подпространства порожденного набором {v_i} состоит лишь из нуля, то база Хилберта, построенная из этого ортогонального набора, совпадает с исходной семействой; то есть базисные векторы равны v.
LaTeX
$$$ (\\mathrm{HilbertBasis.mkOfOrthogonalEqBot}\\ hv\\ hsp) = v $$$
Lean4
@[simp]
protected theorem coe_mkOfOrthogonalEqBot (hsp : (span 𝕜 (Set.range v))ᗮ = ⊥) :
⇑(HilbertBasis.mkOfOrthogonalEqBot hv hsp) = v :=
HilbertBasis.coe_mk hv
_
-- Note : this should be `b.repr` composed with an identification of `lp (fun i : ι => 𝕜) p` with
-- `PiLp p (fun i : ι => 𝕜)` (in this case with `p = 2`), but we don't have this yet (July 2022).
