mathlib

0e0a8b42 - feat(analysis/inner_product_space/l2_space): define `is_hilbert_sum` predicate (#15772)

feat(analysis/inner_product_space/l2_space): define `is_hilbert_sum` predicate (#15772) This introduces a predicate on a space `E` and a family of linear isometries `V : Π i, G i →ₗᵢ[𝕜] E` expressing that the associated map `lp G 2 →ₗᵢ[𝕜] E` is surjective. As explained in the docstring, this is *somewhat* analogous to `direct_sum.is_internal`, but **not completely**, since it is a predicate on embeddings rather than subspaces (so in a sense it is more category-theoretic, even though we don't implement it as a universal property). I am aware that introducing this inconsistency is not ideal, but I believe this is the cleanest thing to do here, because it follows the design of `orthogonal_family`. I also have a more practical motivation : in a following PR, I will introduce a way to concatenate Hilbert bases from mutually orthogonal "subspaces" with dense span to form a Hilbert basis for the whole space. Without this, the natural way would be to state this with hypotheses `orthogonal_family 𝕜 V` and `⊤ ≤ (⨆ (i : ι), (V i).to_linear_map.range).topological_closure`. First, this is quite verbose for such a common set of hypotheses, but the real problem comes with the fact that for actual subspaces you want to replace this second hypothesis by `⊤ ≤ (⨆ (i : ι), F i).topological_closure`, so you essentially have to duplicate the API. With this constructions, these two variants just correspond to two different ways of proving `is_hilbert_sum`. I think we should consider doing a similar thing for direct sums, stating the fact that the map `direct_sum.to_module` is bijective, but it will be harder since linear maps are not injective in general like linear isometries are.