Documentation

Mathlib.Analysis.NormedSpace.Multilinear.Basic

Operator norm on the space of continuous multilinear maps #

When f is a continuous multilinear map in finitely many variables, we define its norm ‖f‖ as the smallest number such that ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖ for all m.

We show that it is indeed a norm, and prove its basic properties.

Main results #

Let f be a multilinear map in finitely many variables.

Let f be a continuous multilinear map in finitely many variables.

Implementation notes #

We mostly follow the API (and the proofs) of OperatorNorm.lean, with the additional complexity that we should deal with multilinear maps in several variables. The currying/uncurrying constructions are based on those in Multilinear.lean.

From the mathematical point of view, all the results follow from the results on operator norm in one variable, by applying them to one variable after the other through currying. However, this is only well defined when there is an order on the variables (for instance on Fin n) although the final result is independent of the order. While everything could be done following this approach, it turns out that direct proofs are easier and more efficient.

Type variables #

We use the following type variables in this file:

Continuity properties of multilinear maps #

We relate continuity of multilinear maps to the inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖, in both directions. Along the way, we prove useful bounds on the difference ‖f m₁ - f m₂‖.

theorem MultilinearMap.norm_map_coord_zero {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) (hf : Continuous f) {m : (i : ι) → E i} {i : ι} (hi : m i = 0) :
f m = 0

If f is a continuous multilinear map in finitely many variables on E and m is an element of ∀ i, E i such that one of the m i has norm 0, then f m has norm 0.

Note that we cannot drop the continuity assumption because f (m : Unit → E) = f (m ()), where the domain has zero norm and the codomain has a nonzero norm does not satisfy this condition.

theorem MultilinearMap.bound_of_shell_of_norm_map_coord_zero {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) (hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, m i = 0f m = 0) {ε : ι} {C : } (hε : ∀ (i : ι), 0 < ε i) {c : ι𝕜} (hc : ∀ (i : ι), 1 < c i) (hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / c i m i)(∀ (i : ι), m i < ε i)f m C * Finset.prod Finset.univ fun (i : ι) => m i) (m : (i : ι) → E i) :
f m C * Finset.prod Finset.univ fun (i : ι) => m i
theorem MultilinearMap.bound_of_shell_of_continuous {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) (hfc : Continuous f) {ε : ι} {C : } (hε : ∀ (i : ι), 0 < ε i) {c : ι𝕜} (hc : ∀ (i : ι), 1 < c i) (hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / c i m i)(∀ (i : ι), m i < ε i)f m C * Finset.prod Finset.univ fun (i : ι) => m i) (m : (i : ι) → E i) :
f m C * Finset.prod Finset.univ fun (i : ι) => m i

If a continuous multilinear map in finitely many variables on normed spaces satisfies the inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖ on a shell ε i / ‖c i‖ < ‖m i‖ < ε i for some positive numbers ε i and elements c i : 𝕜, 1 < ‖c i‖, then it satisfies this inequality for all m.

theorem MultilinearMap.exists_bound_of_continuous {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) (hf : Continuous f) :
∃ (C : ), 0 < C ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i

If a multilinear map in finitely many variables on normed spaces is continuous, then it satisfies the inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖, for some C which can be chosen to be positive.

theorem MultilinearMap.norm_image_sub_le_of_bound' {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) [DecidableEq ι] {C : } (hC : 0 C) (H : ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i) (m₁ : (i : ι) → E i) (m₂ : (i : ι) → E i) :
f m₁ - f m₂ C * Finset.sum Finset.univ fun (i : ι) => Finset.prod Finset.univ fun (j : ι) => if j = i then m₁ i - m₂ i else max m₁ j m₂ j

If f satisfies a boundedness property around 0, one can deduce a bound on f m₁ - f m₂ using the multilinearity. Here, we give a precise but hard to use version. See norm_image_sub_le_of_bound for a less precise but more usable version. The bound reads ‖f m - f m'‖ ≤ C * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ..., where the other terms in the sum are the same products where 1 is replaced by any i.

theorem MultilinearMap.norm_image_sub_le_of_bound {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {C : } (hC : 0 C) (H : ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i) (m₁ : (i : ι) → E i) (m₂ : (i : ι) → E i) :
f m₁ - f m₂ C * (Fintype.card ι) * max m₁ m₂ ^ (Fintype.card ι - 1) * m₁ - m₂

If f satisfies a boundedness property around 0, one can deduce a bound on f m₁ - f m₂ using the multilinearity. Here, we give a usable but not very precise version. See norm_image_sub_le_of_bound' for a more precise but less usable version. The bound is ‖f m - f m'‖ ≤ C * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1).

theorem MultilinearMap.continuous_of_bound {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) (C : ) (H : ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i) :

If a multilinear map satisfies an inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖, then it is continuous.

noncomputable def MultilinearMap.mkContinuous {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) (C : ) (H : ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i) :

Constructing a continuous multilinear map from a multilinear map satisfying a boundedness condition.

Equations
Instances For
    @[simp]
    theorem MultilinearMap.coe_mkContinuous {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) (C : ) (H : ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i) :
    theorem MultilinearMap.restr_norm_le {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k : } {n : } (f : MultilinearMap 𝕜 (fun (x : Fin n) => G) G') (s : Finset (Fin n)) (hk : s.card = k) (z : G) {C : } (H : ∀ (m : Fin nG), f m C * Finset.prod Finset.univ fun (i : Fin n) => m i) (v : Fin kG) :
    (MultilinearMap.restr f s hk z) v C * z ^ (n - k) * Finset.prod Finset.univ fun (i : Fin k) => v i

    Given a multilinear map in n variables, if one restricts it to k variables putting z on the other coordinates, then the resulting restricted function satisfies an inequality ‖f.restr v‖ ≤ C * ‖z‖^(n-k) * Π ‖v i‖ if the original function satisfies ‖f v‖ ≤ C * Π ‖v i‖.

    Continuous multilinear maps #

    We define the norm ‖f‖ of a continuous multilinear map f in finitely many variables as the smallest number such that ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖ for all m. We show that this defines a normed space structure on ContinuousMultilinearMap 𝕜 E G.

    theorem ContinuousMultilinearMap.bound {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
    ∃ (C : ), 0 < C ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i
    noncomputable def ContinuousMultilinearMap.opNorm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :

    The operator norm of a continuous multilinear map is the inf of all its bounds.

    Equations
    Instances For
      noncomputable instance ContinuousMultilinearMap.hasOpNorm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] :
      Equations
      • ContinuousMultilinearMap.hasOpNorm = { norm := ContinuousMultilinearMap.opNorm }
      noncomputable instance ContinuousMultilinearMap.hasOpNorm' {𝕜 : Type u} {ι : Type v} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] :
      Norm (ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) G')

      An alias of ContinuousMultilinearMap.hasOpNorm with non-dependent types to help typeclass search.

      Equations
      • ContinuousMultilinearMap.hasOpNorm' = ContinuousMultilinearMap.hasOpNorm
      theorem ContinuousMultilinearMap.norm_def {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
      f = sInf {c : | 0 c ∀ (m : (i : ι) → E i), f m c * Finset.prod Finset.univ fun (i : ι) => m i}
      theorem ContinuousMultilinearMap.bounds_nonempty {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ContinuousMultilinearMap 𝕜 E G} :
      ∃ (c : ), c {c : | 0 c ∀ (m : (i : ι) → E i), f m c * Finset.prod Finset.univ fun (i : ι) => m i}
      theorem ContinuousMultilinearMap.bounds_bddBelow {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ContinuousMultilinearMap 𝕜 E G} :
      BddBelow {c : | 0 c ∀ (m : (i : ι) → E i), f m c * Finset.prod Finset.univ fun (i : ι) => m i}
      theorem ContinuousMultilinearMap.isLeast_opNorm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
      IsLeast {c : | 0 c ∀ (m : (i : ι) → E i), f m c * Finset.prod Finset.univ fun (i : ι) => m i} f
      @[deprecated ContinuousMultilinearMap.isLeast_opNorm]
      theorem ContinuousMultilinearMap.isLeast_op_norm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
      IsLeast {c : | 0 c ∀ (m : (i : ι) → E i), f m c * Finset.prod Finset.univ fun (i : ι) => m i} f

      Alias of ContinuousMultilinearMap.isLeast_opNorm.

      theorem ContinuousMultilinearMap.opNorm_nonneg {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
      @[deprecated ContinuousMultilinearMap.opNorm_nonneg]
      theorem ContinuousMultilinearMap.op_norm_nonneg {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :

      Alias of ContinuousMultilinearMap.opNorm_nonneg.

      theorem ContinuousMultilinearMap.le_opNorm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) :
      f m f * Finset.prod Finset.univ fun (i : ι) => m i

      The fundamental property of the operator norm of a continuous multilinear map: ‖f m‖ is bounded by ‖f‖ times the product of the ‖m i‖.

      @[deprecated ContinuousMultilinearMap.le_opNorm]
      theorem ContinuousMultilinearMap.le_op_norm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) :
      f m f * Finset.prod Finset.univ fun (i : ι) => m i

      Alias of ContinuousMultilinearMap.le_opNorm.


      The fundamental property of the operator norm of a continuous multilinear map: ‖f m‖ is bounded by ‖f‖ times the product of the ‖m i‖.

      theorem ContinuousMultilinearMap.le_mul_prod_of_le_opNorm_of_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ContinuousMultilinearMap 𝕜 E G} {m : (i : ι) → E i} {C : } {b : ι} (hC : f C) (hm : ∀ (i : ι), m i b i) :
      f m C * Finset.prod Finset.univ fun (i : ι) => b i
      @[deprecated ContinuousMultilinearMap.le_mul_prod_of_le_opNorm_of_le]
      theorem ContinuousMultilinearMap.le_mul_prod_of_le_op_norm_of_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ContinuousMultilinearMap 𝕜 E G} {m : (i : ι) → E i} {C : } {b : ι} (hC : f C) (hm : ∀ (i : ι), m i b i) :
      f m C * Finset.prod Finset.univ fun (i : ι) => b i

      Alias of ContinuousMultilinearMap.le_mul_prod_of_le_opNorm_of_le.

      theorem ContinuousMultilinearMap.le_opNorm_mul_prod_of_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {m : (i : ι) → E i} {b : ι} (hm : ∀ (i : ι), m i b i) :
      f m f * Finset.prod Finset.univ fun (i : ι) => b i
      @[deprecated ContinuousMultilinearMap.le_opNorm_mul_prod_of_le]
      theorem ContinuousMultilinearMap.le_op_norm_mul_prod_of_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {m : (i : ι) → E i} {b : ι} (hm : ∀ (i : ι), m i b i) :
      f m f * Finset.prod Finset.univ fun (i : ι) => b i

      Alias of ContinuousMultilinearMap.le_opNorm_mul_prod_of_le.

      theorem ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {m : (i : ι) → E i} {b : } (hm : m b) :
      @[deprecated ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le]
      theorem ContinuousMultilinearMap.le_op_norm_mul_pow_card_of_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {m : (i : ι) → E i} {b : } (hm : m b) :

      Alias of ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le.

      theorem ContinuousMultilinearMap.le_opNorm_mul_pow_of_le {𝕜 : Type u} {n : } {G : Type wG} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {Ei : Fin nType u_1} [(i : Fin n) → NormedAddCommGroup (Ei i)] [(i : Fin n) → NormedSpace 𝕜 (Ei i)] (f : ContinuousMultilinearMap 𝕜 Ei G) {m : (i : Fin n) → Ei i} {b : } (hm : m b) :
      f m f * b ^ n
      @[deprecated ContinuousMultilinearMap.le_opNorm_mul_pow_of_le]
      theorem ContinuousMultilinearMap.le_op_norm_mul_pow_of_le {𝕜 : Type u} {n : } {G : Type wG} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {Ei : Fin nType u_1} [(i : Fin n) → NormedAddCommGroup (Ei i)] [(i : Fin n) → NormedSpace 𝕜 (Ei i)] (f : ContinuousMultilinearMap 𝕜 Ei G) {m : (i : Fin n) → Ei i} {b : } (hm : m b) :
      f m f * b ^ n

      Alias of ContinuousMultilinearMap.le_opNorm_mul_pow_of_le.

      theorem ContinuousMultilinearMap.le_of_opNorm_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ContinuousMultilinearMap 𝕜 E G} (m : (i : ι) → E i) {C : } (h : f C) :
      f m C * Finset.prod Finset.univ fun (i : ι) => m i
      @[deprecated ContinuousMultilinearMap.le_of_opNorm_le]
      theorem ContinuousMultilinearMap.le_of_op_norm_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {f : ContinuousMultilinearMap 𝕜 E G} (m : (i : ι) → E i) {C : } (h : f C) :
      f m C * Finset.prod Finset.univ fun (i : ι) => m i

      Alias of ContinuousMultilinearMap.le_of_opNorm_le.

      theorem ContinuousMultilinearMap.ratio_le_opNorm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) :
      (f m / Finset.prod Finset.univ fun (i : ι) => m i) f
      @[deprecated ContinuousMultilinearMap.ratio_le_opNorm]
      theorem ContinuousMultilinearMap.ratio_le_op_norm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) :
      (f m / Finset.prod Finset.univ fun (i : ι) => m i) f

      Alias of ContinuousMultilinearMap.ratio_le_opNorm.

      theorem ContinuousMultilinearMap.unit_le_opNorm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) (h : m 1) :

      The image of the unit ball under a continuous multilinear map is bounded.

      @[deprecated ContinuousMultilinearMap.unit_le_opNorm]
      theorem ContinuousMultilinearMap.unit_le_op_norm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) (h : m 1) :

      Alias of ContinuousMultilinearMap.unit_le_opNorm.


      The image of the unit ball under a continuous multilinear map is bounded.

      theorem ContinuousMultilinearMap.opNorm_le_bound {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {M : } (hMp : 0 M) (hM : ∀ (m : (i : ι) → E i), f m M * Finset.prod Finset.univ fun (i : ι) => m i) :

      If one controls the norm of every f x, then one controls the norm of f.

      @[deprecated ContinuousMultilinearMap.opNorm_le_bound]
      theorem ContinuousMultilinearMap.op_norm_le_bound {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {M : } (hMp : 0 M) (hM : ∀ (m : (i : ι) → E i), f m M * Finset.prod Finset.univ fun (i : ι) => m i) :

      Alias of ContinuousMultilinearMap.opNorm_le_bound.


      If one controls the norm of every f x, then one controls the norm of f.

      theorem ContinuousMultilinearMap.opNorm_le_iff {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {C : } (hC : 0 C) :
      f C ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i
      @[deprecated ContinuousMultilinearMap.opNorm_le_iff]
      theorem ContinuousMultilinearMap.op_norm_le_iff {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {C : } (hC : 0 C) :
      f C ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i

      Alias of ContinuousMultilinearMap.opNorm_le_iff.

      theorem ContinuousMultilinearMap.opNorm_add_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G) :

      The operator norm satisfies the triangle inequality.

      @[deprecated ContinuousMultilinearMap.opNorm_add_le]
      theorem ContinuousMultilinearMap.op_norm_add_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G) :

      Alias of ContinuousMultilinearMap.opNorm_add_le.


      The operator norm satisfies the triangle inequality.

      theorem ContinuousMultilinearMap.opNorm_zero {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] :
      @[deprecated ContinuousMultilinearMap.opNorm_zero]
      theorem ContinuousMultilinearMap.op_norm_zero {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] :

      Alias of ContinuousMultilinearMap.opNorm_zero.

      theorem ContinuousMultilinearMap.opNorm_smul_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {𝕜' : Type u_1} [NormedField 𝕜'] [NormedSpace 𝕜' G] [SMulCommClass 𝕜 𝕜' G] (c : 𝕜') :
      @[deprecated ContinuousMultilinearMap.opNorm_smul_le]
      theorem ContinuousMultilinearMap.op_norm_smul_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {𝕜' : Type u_1} [NormedField 𝕜'] [NormedSpace 𝕜' G] [SMulCommClass 𝕜 𝕜' G] (c : 𝕜') :

      Alias of ContinuousMultilinearMap.opNorm_smul_le.

      theorem ContinuousMultilinearMap.opNorm_neg {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
      @[deprecated ContinuousMultilinearMap.opNorm_neg]
      theorem ContinuousMultilinearMap.op_norm_neg {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :

      Alias of ContinuousMultilinearMap.opNorm_neg.

      noncomputable instance ContinuousMultilinearMap.seminormedAddCommGroup {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] :

      Continuous multilinear maps themselves form a seminormed space with respect to the operator norm.

      Equations
      noncomputable instance ContinuousMultilinearMap.seminormedAddCommGroup' {𝕜 : Type u} {ι : Type v} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] :
      SeminormedAddCommGroup (ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) G')

      An alias of ContinuousMultilinearMap.seminormedAddCommGroup with non-dependent types to help typeclass search.

      Equations
      • ContinuousMultilinearMap.seminormedAddCommGroup' = ContinuousMultilinearMap.seminormedAddCommGroup
      noncomputable instance ContinuousMultilinearMap.normedSpace {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {𝕜' : Type u_1} [NormedField 𝕜'] [NormedSpace 𝕜' G] [SMulCommClass 𝕜 𝕜' G] :
      Equations
      noncomputable instance ContinuousMultilinearMap.normedSpace' {𝕜 : Type u} {ι : Type v} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] {𝕜' : Type u_1} [NormedField 𝕜'] [NormedSpace 𝕜' G] [SMulCommClass 𝕜 𝕜' G] :
      NormedSpace 𝕜' (ContinuousMultilinearMap 𝕜 (fun (x : ι) => G') G)

      An alias of ContinuousMultilinearMap.normedSpace with non-dependent types to help typeclass search.

      Equations
      • ContinuousMultilinearMap.normedSpace' = ContinuousMultilinearMap.normedSpace
      theorem ContinuousMultilinearMap.le_opNNNorm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) :
      f m‖₊ f‖₊ * Finset.prod Finset.univ fun (i : ι) => m i‖₊

      The fundamental property of the operator norm of a continuous multilinear map: ‖f m‖ is bounded by ‖f‖ times the product of the ‖m i‖, nnnorm version.

      @[deprecated ContinuousMultilinearMap.le_opNNNorm]
      theorem ContinuousMultilinearMap.le_op_nnnorm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) :
      f m‖₊ f‖₊ * Finset.prod Finset.univ fun (i : ι) => m i‖₊

      Alias of ContinuousMultilinearMap.le_opNNNorm.


      The fundamental property of the operator norm of a continuous multilinear map: ‖f m‖ is bounded by ‖f‖ times the product of the ‖m i‖, nnnorm version.

      theorem ContinuousMultilinearMap.le_of_opNNNorm_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) {C : NNReal} (h : f‖₊ C) :
      f m‖₊ C * Finset.prod Finset.univ fun (i : ι) => m i‖₊
      @[deprecated ContinuousMultilinearMap.le_of_opNNNorm_le]
      theorem ContinuousMultilinearMap.le_of_op_nnnorm_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) {C : NNReal} (h : f‖₊ C) :
      f m‖₊ C * Finset.prod Finset.univ fun (i : ι) => m i‖₊

      Alias of ContinuousMultilinearMap.le_of_opNNNorm_le.

      theorem ContinuousMultilinearMap.opNNNorm_le_iff {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {C : NNReal} :
      f‖₊ C ∀ (m : (i : ι) → E i), f m‖₊ C * Finset.prod Finset.univ fun (i : ι) => m i‖₊
      @[deprecated ContinuousMultilinearMap.opNNNorm_le_iff]
      theorem ContinuousMultilinearMap.op_nnnorm_le_iff {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {C : NNReal} :
      f‖₊ C ∀ (m : (i : ι) → E i), f m‖₊ C * Finset.prod Finset.univ fun (i : ι) => m i‖₊

      Alias of ContinuousMultilinearMap.opNNNorm_le_iff.

      theorem ContinuousMultilinearMap.isLeast_opNNNorm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
      IsLeast {C : NNReal | ∀ (m : (i : ι) → E i), f m‖₊ C * Finset.prod Finset.univ fun (i : ι) => m i‖₊} f‖₊
      @[deprecated ContinuousMultilinearMap.isLeast_opNNNorm]
      theorem ContinuousMultilinearMap.isLeast_op_nnnorm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
      IsLeast {C : NNReal | ∀ (m : (i : ι) → E i), f m‖₊ C * Finset.prod Finset.univ fun (i : ι) => m i‖₊} f‖₊

      Alias of ContinuousMultilinearMap.isLeast_opNNNorm.

      theorem ContinuousMultilinearMap.opNNNorm_prod {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :
      @[deprecated ContinuousMultilinearMap.opNNNorm_prod]
      theorem ContinuousMultilinearMap.op_nnnorm_prod {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :

      Alias of ContinuousMultilinearMap.opNNNorm_prod.

      theorem ContinuousMultilinearMap.opNorm_prod {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :
      @[deprecated ContinuousMultilinearMap.opNorm_prod]
      theorem ContinuousMultilinearMap.op_norm_prod {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :

      Alias of ContinuousMultilinearMap.opNorm_prod.

      theorem ContinuousMultilinearMap.opNNNorm_pi {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ιType wE} {E' : ι'Type wE'} [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i' : ι') → SeminormedAddCommGroup (E' i')] [(i' : ι') → NormedSpace 𝕜 (E' i')] (f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')) :
      theorem ContinuousMultilinearMap.opNorm_pi {𝕜 : Type u} {ι : Type v} {E : ιType wE} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {ι' : Type v'} [Fintype ι'] {E' : ι'Type wE'} [(i' : ι') → SeminormedAddCommGroup (E' i')] [(i' : ι') → NormedSpace 𝕜 (E' i')] (f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')) :
      @[deprecated ContinuousMultilinearMap.opNorm_pi]
      theorem ContinuousMultilinearMap.op_norm_pi {𝕜 : Type u} {ι : Type v} {E : ιType wE} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {ι' : Type v'} [Fintype ι'] {E' : ι'Type wE'} [(i' : ι') → SeminormedAddCommGroup (E' i')] [(i' : ι') → NormedSpace 𝕜 (E' i')] (f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')) :

      Alias of ContinuousMultilinearMap.opNorm_pi.

      @[simp]
      noncomputable def ContinuousMultilinearMap.ofSubsingletonₗᵢ (𝕜 : Type u) {ι : Type v} (G : Type wG) {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Subsingleton ι] (i : ι) :
      (G →L[𝕜] G') ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) G'

      Linear isometry between continuous linear maps from G to G' and continuous 1-multilinear maps from G to G'.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem ContinuousMultilinearMap.norm_constOfIsEmpty (𝕜 : Type u) {ι : Type v} (E : ιType wE) {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [IsEmpty ι] (x : G) :
        @[simp]
        theorem ContinuousMultilinearMap.nnnorm_constOfIsEmpty (𝕜 : Type u) {ι : Type v} (E : ιType wE) {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [IsEmpty ι] (x : G) :
        noncomputable def ContinuousMultilinearMap.prodL (𝕜 : Type u) {ι : Type v} (E : ιType wE) (G : Type wG) (G' : Type wG') [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] :

        ContinuousMultilinearMap.prod as a LinearIsometryEquiv.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable def ContinuousMultilinearMap.piₗᵢ (𝕜 : Type u) {ι : Type v} (E : ιType wE) [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {ι' : Type v'} [Fintype ι'] {E' : ι'Type wE'} [(i' : ι') → NormedAddCommGroup (E' i')] [(i' : ι') → NormedSpace 𝕜 (E' i')] :
          ((i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')) ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 E ((i : ι') → E' i)

          ContinuousMultilinearMap.pi as a LinearIsometryEquiv.

          Equations
          Instances For
            @[simp]
            theorem ContinuousMultilinearMap.norm_restrictScalars {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' G] [IsScalarTower 𝕜' 𝕜 G] [(i : ι) → NormedSpace 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] :
            noncomputable def ContinuousMultilinearMap.restrictScalarsₗᵢ {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (𝕜' : Type u_1) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' G] [IsScalarTower 𝕜' 𝕜 G] [(i : ι) → NormedSpace 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] :

            ContinuousMultilinearMap.restrictScalars as a LinearIsometry.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def ContinuousMultilinearMap.restrictScalarsLinear {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (𝕜' : Type u_1) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' G] [IsScalarTower 𝕜' 𝕜 G] [(i : ι) → NormedSpace 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] :

              ContinuousMultilinearMap.restrictScalars as a ContinuousLinearMap.

              Equations
              Instances For
                theorem ContinuousMultilinearMap.continuous_restrictScalars {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' G] [IsScalarTower 𝕜' 𝕜 G] [(i : ι) → NormedSpace 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] :
                theorem ContinuousMultilinearMap.norm_image_sub_le' {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) [DecidableEq ι] (m₁ : (i : ι) → E i) (m₂ : (i : ι) → E i) :
                f m₁ - f m₂ f * Finset.sum Finset.univ fun (i : ι) => Finset.prod Finset.univ fun (j : ι) => if j = i then m₁ i - m₂ i else max m₁ j m₂ j

                The difference f m₁ - f m₂ is controlled in terms of ‖f‖ and ‖m₁ - m₂‖, precise version. For a less precise but more usable version, see norm_image_sub_le. The bound reads ‖f m - f m'‖ ≤ ‖f‖ * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ..., where the other terms in the sum are the same products where 1 is replaced by any i.

                theorem ContinuousMultilinearMap.norm_image_sub_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (m₁ : (i : ι) → E i) (m₂ : (i : ι) → E i) :
                f m₁ - f m₂ f * (Fintype.card ι) * max m₁ m₂ ^ (Fintype.card ι - 1) * m₁ - m₂

                The difference f m₁ - f m₂ is controlled in terms of ‖f‖ and ‖m₁ - m₂‖, less precise version. For a more precise but less usable version, see norm_image_sub_le'. The bound is ‖f m - f m'‖ ≤ ‖f‖ * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1).

                theorem ContinuousMultilinearMap.continuous_eval {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] :
                Continuous fun (p : ContinuousMultilinearMap 𝕜 E G × ((i : ι) → E i)) => p.1 p.2

                Applying a multilinear map to a vector is continuous in both coordinates.

                theorem ContinuousMultilinearMap.continuous_eval_left {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (m : (i : ι) → E i) :
                Continuous fun (p : ContinuousMultilinearMap 𝕜 E G) => p m
                theorem ContinuousMultilinearMap.hasSum_eval {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {α : Type u_1} {p : αContinuousMultilinearMap 𝕜 E G} {q : ContinuousMultilinearMap 𝕜 E G} (h : HasSum p q) (m : (i : ι) → E i) :
                HasSum (fun (a : α) => (p a) m) (q m)
                noncomputable def ContinuousMultilinearMap.apply (𝕜 : Type u) {ι : Type v} (E : ιType wE) (G : Type wG) [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (m : (i : ι) → E i) :

                The application of a multilinear map as a ContinuousLinearMap.

                Equations
                Instances For
                  @[simp]
                  theorem ContinuousMultilinearMap.apply_apply {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {m : (i : ι) → E i} {c : ContinuousMultilinearMap 𝕜 E G} :
                  theorem MultilinearMap.mkContinuous_norm_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {C : } (hC : 0 C) (H : ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i) :

                  If a continuous multilinear map is constructed from a multilinear map via the constructor mkContinuous, then its norm is bounded by the bound given to the constructor if it is nonnegative.

                  theorem MultilinearMap.mkContinuous_norm_le' {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {C : } (H : ∀ (m : (i : ι) → E i), f m C * Finset.prod Finset.univ fun (i : ι) => m i) :

                  If a continuous multilinear map is constructed from a multilinear map via the constructor mkContinuous, then its norm is bounded by the bound given to the constructor if it is nonnegative.

                  noncomputable def ContinuousMultilinearMap.restr {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k : } {n : } (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => G) G') (s : Finset (Fin n)) (hk : s.card = k) (z : G) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin k) => G) G'

                  Given a continuous multilinear map f on n variables (parameterized by Fin n) and a subset s of k of these variables, one gets a new continuous multilinear map on Fin k by varying these variables, and fixing the other ones equal to a given value z. It is denoted by f.restr s hk z, where hk is a proof that the cardinality of s is k. The implicit identification between Fin k and s that we use is the canonical (increasing) bijection.

                  Equations
                  Instances For
                    theorem ContinuousMultilinearMap.norm_restr {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k : } {n : } (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => G) G') (s : Finset (Fin n)) (hk : s.card = k) (z : G) :
                    theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos {𝕜 : Type u} {n : } {Ei : Fin (Nat.succ n)Type wEi} [NontriviallyNormedField 𝕜] [(i : Fin (Nat.succ n)) → SeminormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)] {A : Type u_1} [NormedRing A] [NormedAlgebra 𝕜 A] (hn : 0 < n) :
                    @[simp]
                    theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin {𝕜 : Type u} {n : } {Ei : Fin (Nat.succ n)Type wEi} [NontriviallyNormedField 𝕜] [(i : Fin (Nat.succ n)) → SeminormedAddCommGroup (Ei i)] [(i : Fin (Nat.succ n)) → NormedSpace 𝕜 (Ei i)] {A : Type u_1} [NormedRing A] [NormedAlgebra 𝕜 A] [NormOneClass A] :
                    @[simp]
                    theorem ContinuousMultilinearMap.nnnorm_smulRight {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
                    @[simp]
                    theorem ContinuousMultilinearMap.norm_smulRight {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
                    noncomputable def ContinuousMultilinearMap.piFieldEquiv (𝕜 : Type u) (ι : Type v) (G : Type wG) [Fintype ι] [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] :
                    G ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) => 𝕜) G

                    Continuous multilinear maps on 𝕜^n with values in G are in bijection with G, as such a continuous multilinear map is completely determined by its value on the constant vector made of ones. We register this bijection as a linear isometry in ContinuousMultilinearMap.piFieldEquiv.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem ContinuousLinearMap.norm_compContinuousMultilinearMap_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (g : G →L[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) :
                      noncomputable def ContinuousLinearMap.compContinuousMultilinearMapL (𝕜 : Type u) {ι : Type v} (E : ιType wE) (G : Type wG) (G' : Type wG') [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] :

                      ContinuousLinearMap.compContinuousMultilinearMap as a bundled continuous bilinear map.

                      Equations
                      Instances For
                        noncomputable def ContinuousLinearEquiv.compContinuousMultilinearMapL {𝕜 : Type u} {ι : Type v} (E : ιType wE) {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (g : G ≃L[𝕜] G') :

                        ContinuousLinearMap.compContinuousMultilinearMap as a bundled continuous linear equiv.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          noncomputable def ContinuousLinearMap.flipMultilinear {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') :

                          Flip arguments in f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G' to get ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem ContinuousLinearMap.flipMultilinear_apply_apply {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') (m : (i : ι) → E i) (x : G) :
                            noncomputable def MultilinearMap.mkContinuousLinear {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ) (H : ∀ (x : G) (m : (i : ι) → E i), (f x) m C * x * Finset.prod Finset.univ fun (i : ι) => m i) :

                            Given a map f : G →ₗ[𝕜] MultilinearMap 𝕜 E G' and an estimate H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖, construct a continuous linear map from G to ContinuousMultilinearMap 𝕜 E G'.

                            In order to lift, e.g., a map f : (MultilinearMap 𝕜 E G) →ₗ[𝕜] MultilinearMap 𝕜 E' G' to a map (ContinuousMultilinearMap 𝕜 E G) →L[𝕜] ContinuousMultilinearMap 𝕜 E' G', one can apply this construction to f.comp ContinuousMultilinearMap.toMultilinearMapLinear which is a linear map from ContinuousMultilinearMap 𝕜 E G to MultilinearMap 𝕜 E' G'.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem MultilinearMap.mkContinuousLinear_norm_le' {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ) (H : ∀ (x : G) (m : (i : ι) → E i), (f x) m C * x * Finset.prod Finset.univ fun (i : ι) => m i) :
                              theorem MultilinearMap.mkContinuousLinear_norm_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') {C : } (hC : 0 C) (H : ∀ (x : G) (m : (i : ι) → E i), (f x) m C * x * Finset.prod Finset.univ fun (i : ι) => m i) :
                              noncomputable def MultilinearMap.mkContinuousMultilinear {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ιType wE} {E' : ι'Type wE'} {G : Type wG} [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι') → SeminormedAddCommGroup (E' i)] [(i : ι') → NormedSpace 𝕜 (E' i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ) (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), (f m₁) m₂ (C * Finset.prod Finset.univ fun (i : ι) => m₁ i) * Finset.prod Finset.univ fun (i : ι') => m₂ i) :

                              Given a map f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G) and an estimate H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖, upgrade all MultilinearMaps in the type to ContinuousMultilinearMaps.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem MultilinearMap.mkContinuousMultilinear_apply {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ιType wE} {E' : ι'Type wE'} {G : Type wG} [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι') → SeminormedAddCommGroup (E' i)] [(i : ι') → NormedSpace 𝕜 (E' i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : } (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), (f m₁) m₂ (C * Finset.prod Finset.univ fun (i : ι) => m₁ i) * Finset.prod Finset.univ fun (i : ι') => m₂ i) (m : (i : ι) → E i) :
                                theorem MultilinearMap.mkContinuousMultilinear_norm_le' {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ιType wE} {E' : ι'Type wE'} {G : Type wG} [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι') → SeminormedAddCommGroup (E' i)] [(i : ι') → NormedSpace 𝕜 (E' i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ) (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), (f m₁) m₂ (C * Finset.prod Finset.univ fun (i : ι) => m₁ i) * Finset.prod Finset.univ fun (i : ι') => m₂ i) :
                                theorem MultilinearMap.mkContinuousMultilinear_norm_le {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ιType wE} {E' : ι'Type wE'} {G : Type wG} [Fintype ι] [Fintype ι'] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι') → SeminormedAddCommGroup (E' i)] [(i : ι') → NormedSpace 𝕜 (E' i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : } (hC : 0 C) (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), (f m₁) m₂ (C * Finset.prod Finset.univ fun (i : ι) => m₁ i) * Finset.prod Finset.univ fun (i : ι') => m₂ i) :
                                theorem ContinuousMultilinearMap.norm_compContinuousLinearMap_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {E₁ : ιType wE₁} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i →L[𝕜] E₁ i) :
                                theorem ContinuousMultilinearMap.norm_compContinuous_linearIsometry_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {E₁ : ιType wE₁} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i) :
                                theorem ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv {𝕜 : Type u} {ι : Type v} {E : ιType wE} {E₁ : ιType wE₁} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i) :
                                ContinuousMultilinearMap.compContinuousLinearMap g fun (i : ι) => { toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := , continuous_invFun := } = g
                                noncomputable def ContinuousMultilinearMap.compContinuousLinearMapL {𝕜 : Type u} {ι : Type v} {E : ιType wE} {E₁ : ιType wE₁} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : (i : ι) → E i →L[𝕜] E₁ i) :

                                ContinuousMultilinearMap.compContinuousLinearMap as a bundled continuous linear map. This implementation fixes f : Π i, E i →L[𝕜] E₁ i.

                                Actually, the map is multilinear in f, see ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem ContinuousMultilinearMap.compContinuousLinearMapL_apply {𝕜 : Type u} {ι : Type v} {E : ιType wE} {E₁ : ιType wE₁} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i →L[𝕜] E₁ i) :
                                  theorem ContinuousMultilinearMap.norm_compContinuousLinearMapL_le {𝕜 : Type u} {ι : Type v} {E : ιType wE} {E₁ : ιType wE₁} (G : Type wG) [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : (i : ι) → E i →L[𝕜] E₁ i) :
                                  noncomputable def ContinuousMultilinearMap.compContinuousLinearMapMultilinear (𝕜 : Type u) {ι : Type v} (E : ιType wE) (E₁ : ιType wE₁) (G : Type wG) [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] :
                                  MultilinearMap 𝕜 (fun (i : ι) => E i →L[𝕜] E₁ i) (ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)

                                  If f is a collection of continuous linear maps, then the construction ContinuousMultilinearMap.compContinuousLinearMap sending a continuous multilinear map g to g (f₁ ·, ..., fₙ ·) is continuous-linear in g and multilinear in f₁, ..., fₙ.

                                  Equations
                                  Instances For
                                    noncomputable def ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear (𝕜 : Type u) {ι : Type v} (E : ιType wE) (E₁ : ιType wE₁) (G : Type wG) [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] :
                                    ContinuousMultilinearMap 𝕜 (fun (i : ι) => E i →L[𝕜] E₁ i) (ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)

                                    If f is a collection of continuous linear maps, then the construction ContinuousMultilinearMap.compContinuousLinearMap sending a continuous multilinear map g to g (f₁ ·, ..., fₙ ·) is continuous-linear in g and continuous-multilinear in f₁, ..., fₙ.

                                    Equations
                                    Instances For
                                      noncomputable def ContinuousMultilinearMap.compContinuousLinearMapEquivL {𝕜 : Type u} {ι : Type v} {E : ιType wE} {E₁ : ιType wE₁} (G : Type wG) [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : (i : ι) → E i ≃L[𝕜] E₁ i) :

                                      ContinuousMultilinearMap.compContinuousLinearMap as a bundled continuous linear equiv, given f : Π i, E i ≃L[𝕜] E₁ i.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem ContinuousMultilinearMap.compContinuousLinearMapEquivL_symm {𝕜 : Type u} {ι : Type v} {E : ιType wE} {E₁ : ιType wE₁} (G : Type wG) [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : (i : ι) → E i ≃L[𝕜] E₁ i) :
                                        @[simp]
                                        theorem ContinuousMultilinearMap.compContinuousLinearMapEquivL_apply {𝕜 : Type u} {ι : Type v} {E : ιType wE} {E₁ : ιType wE₁} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i ≃L[𝕜] E₁ i) :
                                        noncomputable instance continuousConstSMul {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {R : Type u_1} [Semiring R] [Module R G] [SMulCommClass 𝕜 R G] [ContinuousConstSMul R G] :
                                        Equations
                                        • =

                                        Results that are only true if the target space is a NormedAddCommGroup (and not just a SeminormedAddCommGroup).

                                        theorem ContinuousMultilinearMap.opNorm_zero_iff {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
                                        f = 0 f = 0

                                        A continuous linear map is zero iff its norm vanishes.

                                        @[deprecated ContinuousMultilinearMap.opNorm_zero_iff]
                                        theorem ContinuousMultilinearMap.op_norm_zero_iff {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
                                        f = 0 f = 0

                                        Alias of ContinuousMultilinearMap.opNorm_zero_iff.


                                        A continuous linear map is zero iff its norm vanishes.

                                        noncomputable instance ContinuousMultilinearMap.normedAddCommGroup {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] :

                                        Continuous multilinear maps themselves form a normed group with respect to the operator norm.

                                        Equations
                                        noncomputable instance ContinuousMultilinearMap.normedAddCommGroup' {𝕜 : Type u} {ι : Type v} {G : Type wG} {G' : Type wG'} [Fintype ι] [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] :
                                        NormedAddCommGroup (ContinuousMultilinearMap 𝕜 (fun (x : ι) => G') G)

                                        An alias of ContinuousMultilinearMap.normedAddCommGroup with non-dependent types to help typeclass search.

                                        Equations
                                        • ContinuousMultilinearMap.normedAddCommGroup' = ContinuousMultilinearMap.normedAddCommGroup
                                        theorem ContinuousMultilinearMap.tsum_eval {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {α : Type u_1} {p : αContinuousMultilinearMap 𝕜 E G} (hp : Summable p) (m : (i : ι) → E i) :
                                        (∑' (a : α), p a) m = ∑' (a : α), (p a) m
                                        noncomputable instance ContinuousMultilinearMap.completeSpace {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G] :

                                        If the target space is complete, the space of continuous multilinear maps with its norm is also complete. The proof is essentially the same as for the space of continuous linear maps (modulo the addition of Finset.prod where needed. The duplication could be avoided by deducing the linear case from the multilinear case via a currying isomorphism. However, this would mess up imports, and it is more satisfactory to have the simplest case as a standalone proof.

                                        Equations
                                        • =

                                        Results that are only true if the source is a NormedAddCommGroup (and not just a SeminormedAddCommGroup).

                                        theorem MultilinearMap.bound_of_shell {𝕜 : Type u} {ι : Type v} {E : ιType wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {ε : ι} {C : } (hε : ∀ (i : ι), 0 < ε i) {c : ι𝕜} (hc : ∀ (i : ι), 1 < c i) (hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / c i m i)(∀ (i : ι), m i < ε i)f m C * Finset.prod Finset.univ fun (i : ι) => m i) (m : (i : ι) → E i) :
                                        f m C * Finset.prod Finset.univ fun (i : ι) => m i

                                        If a multilinear map in finitely many variables on normed spaces satisfies the inequality ‖f m‖ ≤ C * ∏ i, ‖m i‖ on a shell ε i / ‖c i‖ < ‖m i‖ < ε i for some positive numbers ε i and elements c i : 𝕜, 1 < ‖c i‖, then it satisfies this inequality for all m.