feat(Analysis/NormedSpace/Multilinear.Basic): operator norm on `Conti…

…nuousMultilinearMap` 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.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

@@ -153,7 +153,7 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
       ‖iteratedFDeriv ℝ i ((M⁻¹ * δ n) • g n) x‖ = ‖(M⁻¹ * δ n) • iteratedFDeriv ℝ i (g n) x‖ := by
         rw [iteratedFDeriv_const_smul_apply]; exact (g_smooth n).of_le le_top
       _ = M⁻¹ * δ n * ‖iteratedFDeriv ℝ i (g n) x‖ := by
-        rw [norm_smul, Real.norm_of_nonneg]; positivity
+        rw [norm_smul _ (iteratedFDeriv ℝ i (g n) x), Real.norm_of_nonneg]; positivity
       _ ≤ M⁻¹ * δ n * M := (mul_le_mul_of_nonneg_left ((hR i x).trans (IR i hi)) (by positivity))
       _ = δ n := by field_simp
   choose r rpos hr using this

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -210,7 +210,8 @@ variable [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
 theorem decay_smul_aux (k n : ℕ) (f : 𝓢(E, F)) (c : 𝕜) (x : E) :
     ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • (f : E → F)) x‖ =
       ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ := by
-  rw [mul_comm ‖c‖, mul_assoc, iteratedFDeriv_const_smul_apply (f.smooth _), norm_smul]
+  rw [mul_comm ‖c‖, mul_assoc, iteratedFDeriv_const_smul_apply (f.smooth _),
+    norm_smul c (iteratedFDeriv ℝ n (⇑f) x)]
 #align schwartz_map.decay_smul_aux SchwartzMap.decay_smul_aux
 
 end Aux