Commit 2024-01-20 11:07 9d89f498

feat(Analysis/NormedSpace/Multilinear.Basic): operator norm on ContinuousMultilinearMap for seminormed spaces (#9700) Slightly generalize the definition of the operator norm on ContinuousMultilinearMap so that it works when the spaces have seminorms (and not just norms). There are two new lemmas MultilinearMap.zero_of_continuous_of_one_entry_norm_zero and MultilinearMap.bound_of_shell_of_continuous that do the work of the old lemma MultilinearMap.bound_of_shell; I kept that last lemma (with the same hypotheses as before) in case it is useful somewhere else. Also, ContinuousMultilinearMap only gets a SeminormedAddCommGroup instance in general, which is upgraded to a NormedAddCommGroup instance if the target space is normed. Other lemmas and their proofs are unchanged, they are just rearranged to separate the ones that work for general seminormed spaces and the ones that only work for normed spaces.