Commit 2022-01-15 07:39 df2d70d6

refactor(analysis/inner_product_space/basic): generalize orthogonal_family from submodules to maps (#11254) The old definition of orthogonal_family was a predicate on V : ι → submodule 𝕜 E, a family of submodules of an inner product space E; the new definition is a predicate on

{G : ι → Type*} [Π i, inner_product_space 𝕜 (G i)] (V : Π i, G i →ₗᵢ[𝕜] E)

a family of inner product spaces and (injective, generally not surjective) isometries of these inner product spaces into E. The new definition subsumes the old definition, but also applies more cleanly to orthonormal sets of vectors. An orthonormal set {v : ι → E} of vectors in E induces an orthogonal_family of the new style with G i chosen to be 𝕜, for each i, and V i : G i →ₗᵢ[𝕜] E the map from 𝕜 to the span of v i in E. In #11255 we write down the induced isometry from the l2 space lp G 2 into E induced by "summing" all the isometries in an orthogonal family. This works for either the old definition or the new definition. But with the old definition, an orthonormal set of vectors induces an isometry from the weird l2 space lp (λ i, span 𝕜 (v i)) 2 into E, whereas with the new definition it induces an isometry from the standard l2 space lp (λ i, 𝕜) 2 into E. This is much more elegant!