mathlib

df2d70d6 - refactor(analysis/inner_product_space/basic): generalize `orthogonal_family` from submodules to maps (#11254)

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 ```lean {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!