Commit 2024-07-27 16:22 946985da

feat: add NormedSpace.Core structure to easily define normed vector spaces (#13424) This PR introduces a NormedSpace.Core structure loosely based on InnerProductSpace.Core, which encapsulates the minimal axioms needed to show that a type forms a normed vector space, as found in textbooks. We then provide functions that take a NormedSpace.Core and produce instances of NormedAddCommGroup and NormedSpace. Note that as it stands, defining a normed vector space from scratch (i.e. on a type without a preexisting notion of distance) is surprisingly painful, we have to keep converting between norm and distance, and there are many redundant proofs to provide. Update (2024-07-25): This PR has now been significantly expanded to include tools to add a norm structure to a type that already has a uniformity or bornology. This involves "replacing" the uniformity/bornology induced by the norm by the preexisting one, while ensuring that the uniformity/bornology induced by the norm is a equal to the old one. (This is fairly common for e.g. matrices, where all reasonable norms induce the product uniformity.)