Mathlib.Analysis.NormedSpace.Multilinear.Basic

ContinuousLinearMap.continuous_uncurry_of_multilinear theorem

(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) : Continuous (fun (p : G × (Π i, E i)) ↦ f p.1 p.2)

Full source

lemma continuous_uncurry_of_multilinear (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) :
    Continuous (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) := by
  fun_prop

Continuity of Uncurried Multilinear Map Associated to a Continuous Linear Map

Informal description

Let $G$ and $E_i$ for $i \in \iota$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $F$ be another normed vector space over $\mathbb{K}$. Given a continuous linear map $f \colon G \to \mathcal{L}_{\text{cont}}(\prod_{i \in \iota} E_i, F)$ from $G$ to the space of continuous multilinear maps from $\prod_{i \in \iota} E_i$ to $F$, the uncurried function $(g, \mathbf{x}) \mapsto f(g)(\mathbf{x})$ is continuous on $G \times \prod_{i \in \iota} E_i$.

ContinuousLinearMap.continuousOn_uncurry_of_multilinear theorem

(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {s} : ContinuousOn (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) s

Full source

lemma continuousOn_uncurry_of_multilinear (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {s} :
    ContinuousOn (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) s :=
  f.continuous_uncurry_of_multilinear.continuousOn

Continuity on Subsets for Uncurried Multilinear Map Associated to a Continuous Linear Map

Informal description

Let $G$ and $E_i$ for $i \in \iota$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $F$ be another normed vector space over $\mathbb{K}$. Given a continuous linear map $f \colon G \to \mathcal{L}_{\text{cont}}(\prod_{i \in \iota} E_i, F)$ from $G$ to the space of continuous multilinear maps from $\prod_{i \in \iota} E_i$ to $F$, the uncurried function $(g, \mathbf{x}) \mapsto f(g)(\mathbf{x})$ is continuous on any subset $s \subseteq G \times \prod_{i \in \iota} E_i$.

ContinuousLinearMap.continuousAt_uncurry_of_multilinear theorem

(f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {x} : ContinuousAt (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) x

Full source

lemma continuousAt_uncurry_of_multilinear (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {x} :
    ContinuousAt (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) x :=
  f.continuous_uncurry_of_multilinear.continuousAt

Pointwise Continuity of Uncurried Multilinear Map Associated to a Continuous Linear Map

Informal description

Let $G$ and $E_i$ for $i \in \iota$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $F$ be another normed vector space over $\mathbb{K}$. Given a continuous linear map $f \colon G \to \mathcal{L}_{\text{cont}}(\prod_{i \in \iota} E_i, F)$, the uncurried function $(g, \mathbf{x}) \mapsto f(g)(\mathbf{x})$ is continuous at every point $x \in G \times \prod_{i \in \iota} E_i$.

ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear theorem

 (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {s x} : ContinuousWithinAt (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) s x

Full source

lemma continuousWithinAt_uncurry_of_multilinear (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {s x} :
    ContinuousWithinAt (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) s x :=
  f.continuous_uncurry_of_multilinear.continuousWithinAt

Continuity Within Subset for Uncurried Multilinear Map Associated to a Continuous Linear Map

Informal description

Let $G$ and $E_i$ for $i \in \iota$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $F$ be another normed vector space over $\mathbb{K}$. Given a continuous linear map $f \colon G \to \mathcal{L}_{\text{cont}}(\prod_{i \in \iota} E_i, F)$ from $G$ to the space of continuous multilinear maps from $\prod_{i \in \iota} E_i$ to $F$, the uncurried function $(g, \mathbf{x}) \mapsto f(g)(\mathbf{x})$ is continuous within any subset $s \subseteq G \times \prod_{i \in \iota} E_i$ at any point $x \in s$.

MultilinearMap.norm_map_coord_zero theorem

(f : MultilinearMap 𝕜 E G) (hf : Continuous f) {m : ∀ i, E i} {i : ι} (hi : ‖m i‖ = 0) : ‖f m‖ = 0

Full source

/-- If `f` is a continuous multilinear map 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. -/
lemma norm_map_coord_zero (f : MultilinearMap 𝕜 E G) (hf : Continuous f)
    {m : ∀ i, E i} {i : ι} (hi : ‖m i‖ = 0) : ‖f m‖ = 0 := by
  classical
  rw [← inseparable_zero_iff_norm] at hi ⊢
  have : Inseparable (update m i 0) m := inseparable_pi.2 <|
    (forall_update_iff m fun i a ↦ Inseparable a (m i)).2 ⟨hi.symm, fun _ _ ↦ rfl⟩
  simpa only [map_update_zero] using this.symm.map hf

Vanishing of Continuous Multilinear Map at Zero-Norm Component

Informal description

Let $f$ be a continuous multilinear map on a family of normed vector spaces $(E_i)_{i \in \iota}$ over a nontrivially normed field $\mathbb{K}$, and let $m \in \prod_{i \in \iota} E_i$ be such that $\|m_i\| = 0$ for some $i \in \iota$. Then $\|f(m)\| = 0$.

MultilinearMap.bound_of_shell_of_norm_map_coord_zero theorem

 (f : MultilinearMap 𝕜 E G) (hf₀ : ∀ {m i}, ‖m i‖ = 0 → ‖f 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 * ∏ i, ‖m i‖)
  (m : ∀ i, E i) : ‖f m‖ ≤ C * ∏ i, ‖m i‖

Full source

/-- If a multilinear map in finitely many variables on seminormed spaces
sends vectors with a component of norm zero to vectors of norm zero
and 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`.

The first assumption is automatically satisfied on normed spaces, see `bound_of_shell` below.
For seminormed spaces, it follows from continuity of `f`, see next lemma,
see `bound_of_shell_of_continuous` below. -/
theorem bound_of_shell_of_norm_map_coord_zero (f : MultilinearMap 𝕜 E G)
    (hf₀ : ∀ {m i}, ‖m i‖ = 0 → ‖f 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 * ∏ i, ‖m i‖)
    (m : ∀ i, E i) : ‖f m‖ ≤ C * ∏ i, ‖m i‖ := by
  rcases em (∃ i, ‖m i‖ = 0) with (⟨i, hi⟩ | hm)
  · rw [hf₀ hi, prod_eq_zero (mem_univ i) hi, mul_zero]
  push_neg at hm
  choose δ hδ0 hδm_lt hle_δm _ using fun i => rescale_to_shell_semi_normed (hc i) (hε i) (hm i)
  have hδ0 : 0 < ∏ i, ‖δ i‖ := prod_pos fun i _ => norm_pos_iff.2 (hδ0 i)
  simpa [map_smul_univ, norm_smul, prod_mul_distrib, mul_left_comm C, mul_le_mul_left hδ0] using
    hf (fun i => δ i • m i) hle_δm hδm_lt

Shell Condition Implies Global Bound for Vanishing Multilinear Maps

Informal description

Let $f$ be a multilinear map on a family of seminormed vector spaces $(E_i)_{i \in \iota}$ over a nontrivially normed field $\mathbb{K}$. Suppose that: 1. $f$ vanishes on vectors with a zero-norm component, i.e., $\|m_i\| = 0$ implies $\|f(m)\| = 0$ for any $m \in \prod_{i \in \iota} E_i$ and $i \in \iota$; 2. There exist positive numbers $\varepsilon_i > 0$ and elements $c_i \in \mathbb{K}$ with $\|c_i\| > 1$ for each $i \in \iota$; 3. For all $m$ satisfying $\varepsilon_i / \|c_i\| \leq \|m_i\| < \varepsilon_i$ for each $i$, the inequality $\|f(m)\| \leq C \prod_{i} \|m_i\|$ holds. Then for all $m \in \prod_{i \in \iota} E_i$, the inequality $\|f(m)\| \leq C \prod_{i} \|m_i\|$ holds.

MultilinearMap.bound_of_shell_of_continuous theorem

 (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 * ∏ i, ‖m i‖)
  (m : ∀ i, E i) : ‖f m‖ ≤ C * ∏ i, ‖m i‖

Full source

/-- 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 bound_of_shell_of_continuous (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 * ∏ i, ‖m i‖)
    (m : ∀ i, E i) : ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
  bound_of_shell_of_norm_map_coord_zero f (norm_map_coord_zero f hfc) hε hc hf m

Shell Condition Implies Global Bound for Continuous Multilinear Maps

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. Suppose there exist positive numbers $\varepsilon_i > 0$ and elements $c_i \in \mathbb{K}$ with $\|c_i\| > 1$ for each $i \in \iota$, such that for all $m \in \prod_{i \in \iota} E_i$ satisfying $\varepsilon_i / \|c_i\| \leq \|m_i\| < \varepsilon_i$ for each $i$, the inequality $\|f(m)\| \leq C \prod_{i} \|m_i\|$ holds. Then for all $m \in \prod_{i \in \iota} E_i$, the inequality $\|f(m)\| \leq C \prod_{i} \|m_i\|$ holds.

MultilinearMap.exists_bound_of_continuous theorem

(f : MultilinearMap 𝕜 E G) (hf : Continuous f) : ∃ C : ℝ, 0 < C ∧ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖

Full source

/-- 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 exists_bound_of_continuous (f : MultilinearMap 𝕜 E G) (hf : Continuous f) :
    ∃ C : ℝ, 0 < C ∧ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖ := by
  cases isEmpty_or_nonempty ι
  · refine ⟨‖f 0‖ + 1, add_pos_of_nonneg_of_pos (norm_nonneg _) zero_lt_one, fun m => ?_⟩
    obtain rfl : m = 0 := funext (IsEmpty.elim ‹_›)
    simp [univ_eq_empty, zero_le_one]
  obtain ⟨ε : ℝ, ε0 : 0 < ε, hε : ∀ m : ∀ i, E i, ‖m - 0‖ < ε → ‖f m - f 0‖ < 1⟩ :=
    NormedAddCommGroup.tendsto_nhds_nhds.1 (hf.tendsto 0) 1 zero_lt_one
  simp only [sub_zero, f.map_zero] at hε
  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
  have : 0 < (‖c‖ / ε) ^ Fintype.card ι := pow_pos (div_pos (zero_lt_one.trans hc) ε0) _
  refine ⟨_, this, ?_⟩
  refine f.bound_of_shell_of_continuous hf (fun _ => ε0) (fun _ => hc) fun m hcm hm => ?_
  refine (hε m ((pi_norm_lt_iff ε0).2 hm)).le.trans ?_
  rw [← div_le_iff₀' this, one_div, ← inv_pow, inv_div, Fintype.card, ← prod_const]
  exact prod_le_prod (fun _ _ => div_nonneg ε0.le (norm_nonneg _)) fun i _ => hcm i

Existence of Bound for Continuous Multilinear Maps

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. Then there exists a positive constant $C > 0$ such that for all $m \in \prod_{i \in \iota} E_i$, the inequality $\|f(m)\| \leq C \prod_{i \in \iota} \|m_i\|$ holds.

MultilinearMap.norm_image_sub_le_of_bound' theorem

 [DecidableEq ι] (f : MultilinearMap 𝕜 E G) {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m₁ m₂ : ∀ i, E i) :
  ‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Full source

/-- If a multilinear map `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 norm_image_sub_le_of_bound' [DecidableEq ι] (f : MultilinearMap 𝕜 E G) {C : ℝ} (hC : 0 ≤ C)
    (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m₁ m₂ : ∀ i, E i) :
    ‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
  have A :
    ∀ s : Finset ι,
      ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤
        C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
    intro s
    induction' s using Finset.induction with i s his Hrec
    · simp
    have I :
      ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
        C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
      have A : (insert i s).piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₂ i) :=
        s.piecewise_insert _ _ _
      have B : s.piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₁ i) := by
        simp [eq_update_iff, his]
      rw [B, A, ← f.map_update_sub]
      apply le_trans (H _)
      gcongr with j
      by_cases h : j = i
      · rw [h]
        simp
      · by_cases h' : j ∈ s <;> simp [h', h, le_refl]
    calc
      ‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
          ‖f m₁ - f (s.piecewise m₂ m₁)‖ +
            ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ := by
        rw [← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm]
        exact dist_triangle _ _ _
      _ ≤ (C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
            C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
        (add_le_add Hrec I)
      _ = C * ∑ i ∈ insert i s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
        simp [his, add_comm, left_distrib]
  convert A univ
  simp

Precise Bound on Multilinear Map Difference: $\|f(m_1) - f(m_2)\|$ under Boundedness Condition

Informal description

Let $f$ be a multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, where $\iota$ is a finite index type with decidable equality. Suppose there exists a nonnegative constant $C \geq 0$ such that for all $m = (m_i)_{i \in \iota}$, the norm $\|f(m)\| \leq C \prod_{i \in \iota} \|m_i\|$. Then for any two vectors $m_1, m_2 \in \prod_{i \in \iota} E_i$, the difference satisfies the inequality: \[ \|f(m_1) - f(m_2)\| \leq C \sum_{i \in \iota} \left( \|m_1(i) - m_2(i)\| \cdot \prod_{j \neq i} \max(\|m_1(j)\|, \|m_2(j)\|) \right). \]

MultilinearMap.norm_image_sub_le_of_bound theorem

 (f : MultilinearMap 𝕜 E G) {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m₁ m₂ : ∀ i, E i) :
  ‖f m₁ - f m₂‖ ≤ C * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Full source

/-- 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 norm_image_sub_le_of_bound (f : MultilinearMap 𝕜 E G)
    {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m₁ m₂ : ∀ i, E i) :
    ‖f m₁ - f m₂‖ ≤ C * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖ := by
  classical
  have A :
    ∀ i : ι,
      ∏ j, (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
        ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by
    intro i
    calc
      ∏ j, (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
          ∏ j : ι, Function.update (fun _ => max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j := by
        apply Finset.prod_le_prod
        · intro j _
          by_cases h : j = i <;> simp [h, norm_nonneg]
        · intro j _
          by_cases h : j = i
          · rw [h]
            simp only [ite_true, Function.update_self]
            exact norm_le_pi_norm (m₁ - m₂) i
          · simp [h, - le_sup_iff, - sup_le_iff, sup_le_sup, norm_le_pi_norm]
      _ = ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by
        rw [prod_update_of_mem (Finset.mem_univ _)]
        simp [card_univ_diff]
  calc
    ‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
      f.norm_image_sub_le_of_bound' hC H m₁ m₂
    _ ≤ C * ∑ _i, ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by gcongr; apply A
    _ = C * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖ := by
      rw [sum_const, card_univ, nsmul_eq_mul]
      ring

Bound on Multilinear Map Difference: $\|f(m_1) - f(m_2)\|$ under Boundedness Condition

Informal description

Let $f$ be a multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, where $\iota$ is a finite index type. Suppose there exists a nonnegative constant $C \geq 0$ such that for all $m = (m_i)_{i \in \iota}$, the norm $\|f(m)\| \leq C \prod_{i \in \iota} \|m_i\|$. Then for any two vectors $m_1, m_2 \in \prod_{i \in \iota} E_i$, the difference satisfies the inequality: \[ \|f(m_1) - f(m_2)\| \leq C \cdot |\iota| \cdot \max(\|m_1\|, \|m_2\|)^{|\iota| - 1} \cdot \|m_1 - m_2\|, \] where $|\iota|$ denotes the cardinality of the index set $\iota$.

MultilinearMap.continuous_of_bound theorem

(f : MultilinearMap 𝕜 E G) (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : Continuous f

Full source

/-- If a multilinear map satisfies an inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`, then it is
continuous. -/
theorem continuous_of_bound (f : MultilinearMap 𝕜 E G) (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :
    Continuous f := by
  let D := max C 1
  have D_pos : 0 ≤ D := le_trans zero_le_one (le_max_right _ _)
  replace H (m) : ‖f m‖ ≤ D * ∏ i, ‖m i‖ :=
    (H m).trans (mul_le_mul_of_nonneg_right (le_max_left _ _) <| by positivity)
  refine continuous_iff_continuousAt.2 fun m => ?_
  refine
    continuousAt_of_locally_lipschitz zero_lt_one
      (D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1)) fun m' h' => ?_
  rw [dist_eq_norm, dist_eq_norm]
  have : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1 := by
    simp [zero_le_one, norm_le_of_mem_closedBall (le_of_lt h')]
  calc
    ‖f m' - f m‖ ≤ D * Fintype.card ι * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ :=
      f.norm_image_sub_le_of_bound D_pos H m' m
    _ ≤ D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖ := by gcongr

Continuity of Bounded Multilinear Maps

Informal description

Let $f$ be a multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, where $\iota$ is a finite index type. If there exists a constant $C \in \mathbb{R}$ such that for all $m = (m_i)_{i \in \iota} \in \prod_{i \in \iota} E_i$, the norm satisfies $\|f(m)\| \leq C \prod_{i \in \iota} \|m_i\|$, then $f$ is continuous.

MultilinearMap.coe_mkContinuous theorem

(f : MultilinearMap 𝕜 E G) (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : ⇑(f.mkContinuous C H) = f

Full source

@[simp]
theorem coe_mkContinuous (f : MultilinearMap 𝕜 E G) (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :
    ⇑(f.mkContinuous C H) = f :=
  rfl

Equality of Underlying Functions in Continuous Multilinear Map Construction

Informal description

Let $f$ be a multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, where $\iota$ is a finite index type. If there exists a constant $C \in \mathbb{R}$ such that for all $m \in \prod_{i \in \iota} E_i$, the norm satisfies $\|f(m)\| \leq C \prod_{i \in \iota} \|m_i\|$, then the underlying function of the continuous multilinear map constructed from $f$ via `mkContinuous` coincides with $f$ itself. In other words, the map $\text{mkContinuous}(f, C, H)$ and $f$ have the same underlying function.

MultilinearMap.restr_norm_le theorem

 {k n : ℕ} (f : MultilinearMap 𝕜 (fun _ : Fin n => G) G') (s : Finset (Fin n)) (hk : #s = k) (z : G) {C : ℝ}
  (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (v : Fin k → G) : ‖f.restr s hk z v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i, ‖v i‖

Full source

/-- 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‖`. -/
theorem restr_norm_le {k n : ℕ} (f : MultilinearMap 𝕜 (fun _ : Fin n => G) G')
    (s : Finset (Fin n)) (hk : #s = k) (z : G) {C : ℝ} (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖)
    (v : Fin k → G) : ‖f.restr s hk z v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i, ‖v i‖ := by
  rw [mul_right_comm, mul_assoc]
  convert H _ using 2
  simp only [apply_dite norm, Fintype.prod_dite, prod_const ‖z‖, Finset.card_univ,
    Fintype.card_of_subtype sᶜ fun _ => mem_compl, card_compl, Fintype.card_fin, hk, mk_coe, ←
    (s.orderIsoOfFin hk).symm.bijective.prod_comp fun x => ‖v x‖]
  convert rfl

Norm Bound for Restricted Multilinear Map: $\|f_{\text{restr}}(v)\| \leq C \|z\|^{n-k} \prod \|v_i\|$

Informal description

Let $f$ be a multilinear map from $G^n$ to $G'$ (where $G$ and $G'$ are normed vector spaces over a nontrivially normed field $\mathbb{K}$), and suppose there exists a constant $C > 0$ such that for all $m \in G^n$, $\|f(m)\| \leq C \prod_{i=1}^n \|m_i\|$. Given a subset $s$ of $\{1,\dots,n\}$ with cardinality $k$, and a fixed vector $z \in G$, the restricted map $f_{\text{restr}}$ (obtained by setting the coordinates not in $s$ to $z$) satisfies the inequality: \[ \|f_{\text{restr}}(v)\| \leq C \|z\|^{n-k} \prod_{i=1}^k \|v_i\| \] for all $v \in G^k$.

ContinuousMultilinearMap.bound theorem

(f : ContinuousMultilinearMap 𝕜 E G) : ∃ C : ℝ, 0 < C ∧ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖

Full source

theorem bound (f : ContinuousMultilinearMap 𝕜 E G) :
    ∃ C : ℝ, 0 < C ∧ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
  f.toMultilinearMap.exists_bound_of_continuous f.2

Existence of Bound for Continuous Multilinear Maps

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. Then there exists a positive constant $C > 0$ such that for all $m \in \prod_{i \in \iota} E_i$, the inequality $\|f(m)\| \leq C \prod_{i \in \iota} \|m_i\|$ holds.

ContinuousMultilinearMap.norm_def theorem

 (f : ContinuousMultilinearMap 𝕜 E G) : ‖f‖ = sInf {c | 0 ≤ (c : ℝ) ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖}

Full source

theorem norm_def (f : ContinuousMultilinearMap 𝕜 E G) :
    ‖f‖ = sInf { c | 0 ≤ (c : ℝ) ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖ } :=
  rfl

Definition of Operator Norm for Continuous Multilinear Maps

Informal description

For a continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, the operator norm $\|f\|$ is defined as the infimum of all nonnegative real numbers $c$ satisfying the inequality $\|f(m)\| \leq c \cdot \prod_{i \in \iota} \|m_i\|$ for all $m \in \prod_{i \in \iota} E_i$.

ContinuousMultilinearMap.bounds_nonempty theorem

{f : ContinuousMultilinearMap 𝕜 E G} : ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖}

Full source

theorem bounds_nonempty {f : ContinuousMultilinearMap 𝕜 E G} :
    ∃ c, c ∈ { c | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖ } :=
  let ⟨M, hMp, hMb⟩ := f.bound
  ⟨M, le_of_lt hMp, hMb⟩

Existence of Bounding Constant for Continuous Multilinear Maps

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, there exists a nonnegative real number $c$ such that $\|f(m)\| \leq c \cdot \prod_{i \in \iota} \|m_i\|$ holds for all $m \in \prod_{i \in \iota} E_i$.

ContinuousMultilinearMap.bounds_bddBelow theorem

{f : ContinuousMultilinearMap 𝕜 E G} : BddBelow {c | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖}

Full source

theorem bounds_bddBelow {f : ContinuousMultilinearMap 𝕜 E G} :
    BddBelow { c | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖ } :=
  ⟨0, fun _ ⟨hn, _⟩ => hn⟩

Lower Bound Exists for Multilinear Operator Norm Coefficients

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, the set of nonnegative real numbers $c$ satisfying $\|f(m)\| \leq c \cdot \prod_{i} \|m_i\|$ for all $m$ is bounded below.

ContinuousMultilinearMap.isLeast_opNorm theorem

 (f : ContinuousMultilinearMap 𝕜 E G) : IsLeast {c : ℝ | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖} ‖f‖

Full source

theorem isLeast_opNorm (f : ContinuousMultilinearMap 𝕜 E G) :
    IsLeast {c : ℝ | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖} ‖f‖ := by
  refine IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow
  simp only [Set.setOf_and, Set.setOf_forall]
  exact isClosed_Ici.inter (isClosed_iInter fun m ↦
    isClosed_le continuous_const (continuous_id.mul continuous_const))

Operator Norm is Minimal Bounding Constant for Continuous Multilinear Maps

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, the operator norm $\|f\|$ is the least element of the set of nonnegative real numbers $c$ satisfying $\|f(m)\| \leq c \cdot \prod_{i \in \iota} \|m_i\|$ for all $m \in \prod_{i \in \iota} E_i$. In other words: 1. $\|f\| \geq 0$ and $\|f(m)\| \leq \|f\| \cdot \prod_{i} \|m_i\|$ for all $m$; 2. $\|f\| \leq c$ for any $c \geq 0$ satisfying $\|f(m)\| \leq c \cdot \prod_{i} \|m_i\|$ for all $m$.

ContinuousMultilinearMap.opNorm_nonneg theorem

(f : ContinuousMultilinearMap 𝕜 E G) : 0 ≤ ‖f‖

Full source

theorem opNorm_nonneg (f : ContinuousMultilinearMap 𝕜 E G) : 0 ≤ ‖f‖ :=
  Real.sInf_nonneg fun _ ⟨hx, _⟩ => hx

Nonnegativity of the Operator Norm for Continuous Multilinear Maps

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, the operator norm $\|f\|$ is nonnegative, i.e., $\|f\| \geq 0$.

ContinuousMultilinearMap.le_opNorm theorem

(f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) : ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖

Full source

/-- 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 le_opNorm (f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) :
    ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖ :=
  f.isLeast_opNorm.1.2 m

Fundamental Inequality for Operator Norm of Continuous Multilinear Maps

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, and for any $m \in \prod_{i \in \iota} E_i$, the following inequality holds: \[ \|f(m)\| \leq \|f\| \cdot \prod_{i \in \iota} \|m_i\|. \]

ContinuousMultilinearMap.le_mul_prod_of_opNorm_le_of_le theorem

 {f : ContinuousMultilinearMap 𝕜 E G} {m : ∀ i, E i} {C : ℝ} {b : ι → ℝ} (hC : ‖f‖ ≤ C) (hm : ∀ i, ‖m i‖ ≤ b i) :
  ‖f m‖ ≤ C * ∏ i, b i

Full source

theorem le_mul_prod_of_opNorm_le_of_le {f : ContinuousMultilinearMap 𝕜 E G}
    {m : ∀ i, E i} {C : ℝ} {b : ι → ℝ} (hC : ‖f‖ ≤ C) (hm : ∀ i, ‖m i‖ ≤ b i) :
    ‖f m‖ ≤ C * ∏ i, b i :=
  (f.le_opNorm m).trans <| by gcongr; exacts [f.opNorm_nonneg.trans hC, hm _]

Norm Bound for Continuous Multilinear Maps with Componentwise Bounds

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. Suppose $\|f\| \leq C$ for some $C \geq 0$, and let $m \in \prod_{i \in \iota} E_i$ satisfy $\|m_i\| \leq b_i$ for some $b_i \geq 0$ for each $i \in \iota$. Then: \[ \|f(m)\| \leq C \cdot \prod_{i \in \iota} b_i. \]

ContinuousMultilinearMap.le_opNorm_mul_prod_of_le theorem

 (f : ContinuousMultilinearMap 𝕜 E G) {m : ∀ i, E i} {b : ι → ℝ} (hm : ∀ i, ‖m i‖ ≤ b i) : ‖f m‖ ≤ ‖f‖ * ∏ i, b i

Full source

theorem le_opNorm_mul_prod_of_le (f : ContinuousMultilinearMap 𝕜 E G)
    {m : ∀ i, E i} {b : ι → ℝ} (hm : ∀ i, ‖m i‖ ≤ b i) : ‖f m‖ ≤ ‖f‖ * ∏ i, b i :=
  le_mul_prod_of_opNorm_le_of_le le_rfl hm

Operator Norm Bound for Continuous Multilinear Maps with Componentwise Norm Constraints

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. For any $m \in \prod_{i \in \iota} E_i$ and any family of nonnegative real numbers $(b_i)_{i \in \iota}$ such that $\|m_i\| \leq b_i$ for each $i$, the following inequality holds: \[ \|f(m)\| \leq \|f\| \cdot \prod_{i \in \iota} b_i. \]

ContinuousMultilinearMap.le_opNorm_mul_pow_of_le theorem

 {n : ℕ} {Ei : Fin n → Type*} [∀ i, SeminormedAddCommGroup (Ei i)] [∀ i, NormedSpace 𝕜 (Ei i)]
  (f : ContinuousMultilinearMap 𝕜 Ei G) {m : ∀ i, Ei i} {b : ℝ} (hm : ‖m‖ ≤ b) : ‖f m‖ ≤ ‖f‖ * b ^ n

Full source

theorem le_opNorm_mul_pow_of_le {n : ℕ} {Ei : Fin n → Type*} [∀ i, SeminormedAddCommGroup (Ei i)]
    [∀ i, NormedSpace 𝕜 (Ei i)] (f : ContinuousMultilinearMap 𝕜 Ei G) {m : ∀ i, Ei i} {b : ℝ}
    (hm : ‖m‖ ≤ b) : ‖f m‖ ≤ ‖f‖ * b ^ n := by
  simpa only [Fintype.card_fin] using f.le_opNorm_mul_pow_card_of_le hm

Operator Norm Bound for Continuous Multilinear Maps: $\|f(m)\| \leq \|f\| \cdot b^n$

Informal description

Let $n$ be a natural number, $(E_i)_{i \in \text{Fin } n}$ be a family of seminormed additive commutative groups equipped with a normed space structure over a nontrivially normed field $\mathbb{K}$, and $G$ be a normed vector space over $\mathbb{K}$. For any continuous multilinear map $f \colon \prod_{i \in \text{Fin } n} E_i \to G$, and any $m \in \prod_{i \in \text{Fin } n} E_i$ and $b \in \mathbb{R}$ such that $\|m\| \leq b$, the following inequality holds: \[ \|f(m)\| \leq \|f\| \cdot b^n. \]

ContinuousMultilinearMap.le_of_opNorm_le theorem

 {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ} (h : ‖f‖ ≤ C) (m : ∀ i, E i) : ‖f m‖ ≤ C * ∏ i, ‖m i‖

Full source

theorem le_of_opNorm_le {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ} (h : ‖f‖ ≤ C) (m : ∀ i, E i) :
    ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
  le_mul_prod_of_opNorm_le_of_le h fun _ ↦ le_rfl

Operator Norm Bound for Continuous Multilinear Maps: $\|f(m)\| \leq C \cdot \prod \|m_i\|$

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. If the operator norm of $f$ satisfies $\|f\| \leq C$ for some constant $C \geq 0$, then for any $m \in \prod_{i \in \iota} E_i$, the following inequality holds: \[ \|f(m)\| \leq C \cdot \prod_{i \in \iota} \|m_i\|. \]

ContinuousMultilinearMap.ratio_le_opNorm theorem

(f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) : (‖f m‖ / ∏ i, ‖m i‖) ≤ ‖f‖

Full source

theorem ratio_le_opNorm (f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) :
    (‖f m‖ / ∏ i, ‖m i‖) ≤ ‖f‖ :=
  div_le_of_le_mul₀ (by positivity) (opNorm_nonneg _) (f.le_opNorm m)

Ratio Bound for Continuous Multilinear Maps: $\frac{\|f(m)\|}{\prod \|m_i\|} \leq \|f\|$

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, and for any $m \in \prod_{i \in \iota} E_i$, the ratio of the norm of $f(m)$ to the product of the norms of the $m_i$ is bounded by the operator norm of $f$: \[ \frac{\|f(m)\|}{\prod_{i \in \iota} \|m_i\|} \leq \|f\|. \]

ContinuousMultilinearMap.unit_le_opNorm theorem

(f : ContinuousMultilinearMap 𝕜 E G) {m : ∀ i, E i} (h : ‖m‖ ≤ 1) : ‖f m‖ ≤ ‖f‖

Full source

/-- The image of the unit ball under a continuous multilinear map is bounded. -/
theorem unit_le_opNorm (f : ContinuousMultilinearMap 𝕜 E G) {m : ∀ i, E i} (h : ‖m‖ ≤ 1) :
    ‖f m‖ ≤ ‖f‖ :=
  (le_opNorm_mul_pow_card_of_le f h).trans <| by simp

Norm Bound on Unit Ball for Continuous Multilinear Maps: $\|f(m)\| \leq \|f\|$ when $\|m\| \leq 1$

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. For any $m \in \prod_{i \in \iota} E_i$ with $\|m\| \leq 1$, the norm of $f(m)$ is bounded by the operator norm of $f$: \[ \|f(m)\| \leq \|f\|. \]

ContinuousMultilinearMap.opNorm_le_bound theorem

 {f : ContinuousMultilinearMap 𝕜 E G} {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ m, ‖f m‖ ≤ M * ∏ i, ‖m i‖) : ‖f‖ ≤ M

Full source

/-- If one controls the norm of every `f x`, then one controls the norm of `f`. -/
theorem opNorm_le_bound {f : ContinuousMultilinearMap 𝕜 E G}
    {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ m, ‖f m‖ ≤ M * ∏ i, ‖m i‖) : ‖f‖ ≤ M :=
  csInf_le bounds_bddBelow ⟨hMp, hM⟩

Operator Norm Bound for Continuous Multilinear Maps

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. If there exists a nonnegative real number $M$ such that for all $m \in \prod_i E_i$, the inequality $\|f(m)\| \leq M \cdot \prod_i \|m_i\|$ holds, then the operator norm of $f$ satisfies $\|f\| \leq M$.

ContinuousMultilinearMap.opNorm_le_iff theorem

 {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ} (hC : 0 ≤ C) : ‖f‖ ≤ C ↔ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖

Full source

theorem opNorm_le_iff {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ} (hC : 0 ≤ C) :
    ‖f‖‖f‖ ≤ C ↔ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
  ⟨fun h _ ↦ le_of_opNorm_le h _, opNorm_le_bound hC⟩

Characterization of Operator Norm for Continuous Multilinear Maps: $\|f\| \leq C \leftrightarrow \forall m, \|f(m)\| \leq C \prod \|m_i\|$

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. For any nonnegative real number $C \geq 0$, the operator norm of $f$ satisfies $\|f\| \leq C$ if and only if for all $m \in \prod_{i \in \iota} E_i$, the following inequality holds: \[ \|f(m)\| \leq C \cdot \prod_{i \in \iota} \|m_i\|. \]

ContinuousMultilinearMap.opNorm_add_le theorem

(f g : ContinuousMultilinearMap 𝕜 E G) : ‖f + g‖ ≤ ‖f‖ + ‖g‖

Full source

/-- The operator norm satisfies the triangle inequality. -/
theorem opNorm_add_le (f g : ContinuousMultilinearMap 𝕜 E G) : ‖f + g‖ ≤ ‖f‖ + ‖g‖ :=
  opNorm_le_bound (add_nonneg (opNorm_nonneg f) (opNorm_nonneg g)) fun x => by
    rw [add_mul]
    exact norm_add_le_of_le (le_opNorm _ _) (le_opNorm _ _)

Triangle Inequality for Operator Norm of Continuous Multilinear Maps

Informal description

For any two continuous multilinear maps $f$ and $g$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, the operator norm of their sum satisfies the triangle inequality: \[ \|f + g\| \leq \|f\| + \|g\|. \]

ContinuousMultilinearMap.opNorm_zero theorem

: ‖(0 : ContinuousMultilinearMap 𝕜 E G)‖ = 0

Full source

theorem opNorm_zero : ‖(0 : ContinuousMultilinearMap 𝕜 E G)‖ = 0 :=
  (opNorm_nonneg _).antisymm' <| opNorm_le_bound le_rfl fun m => by simp

Operator Norm of Zero Continuous Multilinear Map is Zero

Informal description

The operator norm of the zero continuous multilinear map is zero, i.e., $\|0\| = 0$.

ContinuousMultilinearMap.opNorm_smul_le theorem

(c : 𝕜') (f : ContinuousMultilinearMap 𝕜 E G) : ‖c • f‖ ≤ ‖c‖ * ‖f‖

Full source

theorem opNorm_smul_le (c : 𝕜') (f : ContinuousMultilinearMap 𝕜 E G) : ‖c • f‖ ≤ ‖c‖ * ‖f‖ :=
  (c • f).opNorm_le_bound (mul_nonneg (norm_nonneg _) (opNorm_nonneg _)) fun m ↦ by
    rw [smul_apply, norm_smul, mul_assoc]
    exact mul_le_mul_of_nonneg_left (le_opNorm _ _) (norm_nonneg _)

Operator Norm Inequality for Scalar Multiplication of Continuous Multilinear Maps

Informal description

For any scalar $c$ in a normed field $\mathbb{K}'$ and any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, the operator norm of the scalar multiple $c \cdot f$ satisfies the inequality: \[ \|c \cdot f\| \leq \|c\| \cdot \|f\|. \]

ContinuousMultilinearMap.opNorm_neg theorem

(f : ContinuousMultilinearMap 𝕜 E G) : ‖-f‖ = ‖f‖

Full source

@[deprecated norm_neg (since := "2024-11-24")]
theorem opNorm_neg (f : ContinuousMultilinearMap 𝕜 E G) : ‖-f‖ = ‖f‖ := norm_neg f

Operator Norm of Negated Continuous Multilinear Map Equals Original Norm

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, the operator norm of the negation $-f$ satisfies $\|-f\| = \|f\|$.

ContinuousMultilinearMap.le_opNNNorm theorem

(f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) : ‖f m‖₊ ≤ ‖f‖₊ * ∏ i, ‖m i‖₊

Full source

/-- 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 le_opNNNorm (f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) :
    ‖f m‖₊ ≤ ‖f‖₊ * ∏ i, ‖m i‖₊ :=
  NNReal.coe_le_coe.1 <| by
    push_cast
    exact f.le_opNorm m

Fundamental Inequality for Non-Negative Operator Norm of Continuous Multilinear Maps

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, and for any $m \in \prod_{i \in \iota} E_i$, the following inequality holds for the non-negative operator norm: \[ \|f(m)\|_{\mathbb{R}_{\geq 0}} \leq \|f\|_{\mathbb{R}_{\geq 0}} \cdot \prod_{i \in \iota} \|m_i\|_{\mathbb{R}_{\geq 0}}. \]

ContinuousMultilinearMap.le_of_opNNNorm_le theorem

 (f : ContinuousMultilinearMap 𝕜 E G) {C : ℝ≥0} (h : ‖f‖₊ ≤ C) (m : ∀ i, E i) : ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊

Full source

theorem le_of_opNNNorm_le (f : ContinuousMultilinearMap 𝕜 E G)
    {C : ℝ≥0} (h : ‖f‖₊ ≤ C) (m : ∀ i, E i) : ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊ :=
  (f.le_opNNNorm m).trans <| mul_le_mul' h le_rfl

Operator Norm Bound Implies Pointwise Bound for Continuous Multilinear Maps

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, if the operator seminorm $\|f\|_{\mathbb{R}_{\geq 0}}$ is bounded above by a constant $C \geq 0$, then for any $m \in \prod_{i \in \iota} E_i$, the following inequality holds: \[ \|f(m)\|_{\mathbb{R}_{\geq 0}} \leq C \cdot \prod_{i \in \iota} \|m_i\|_{\mathbb{R}_{\geq 0}}. \]

ContinuousMultilinearMap.opNNNorm_le_iff theorem

 {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ≥0} : ‖f‖₊ ≤ C ↔ ∀ m, ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊

Full source

theorem opNNNorm_le_iff {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ≥0} :
    ‖f‖₊‖f‖₊ ≤ C ↔ ∀ m, ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊ := by
  simp only [← NNReal.coe_le_coe]; simp [opNorm_le_iff C.coe_nonneg, NNReal.coe_prod]

Characterization of Operator Seminorm for Continuous Multilinear Maps: $\|f\|_{\text{op}} \leq C \leftrightarrow \forall m, \|f(m)\| \leq C \prod \|m_i\|$

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. For any nonnegative real number $C \geq 0$ (represented as an element of $\mathbb{R}_{\geq 0}$), the operator seminorm of $f$ satisfies $\|f\|_{\text{op}} \leq C$ if and only if for all $m \in \prod_{i \in \iota} E_i$, the following inequality holds: \[ \|f(m)\| \leq C \cdot \prod_{i \in \iota} \|m_i\|. \]

ContinuousMultilinearMap.isLeast_opNNNorm theorem

 (f : ContinuousMultilinearMap 𝕜 E G) : IsLeast {C : ℝ≥0 | ∀ m, ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊} ‖f‖₊

Full source

theorem isLeast_opNNNorm (f : ContinuousMultilinearMap 𝕜 E G) :
    IsLeast {C : ℝ≥0 | ∀ m, ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊} ‖f‖₊ := by
  simpa only [← opNNNorm_le_iff] using isLeast_Ici

Minimality of Operator Seminorm for Continuous Multilinear Maps

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, the operator seminorm $\|f\|_*$ is the least element of the set of nonnegative real numbers $C$ such that for all $m \in \prod_{i \in \iota} E_i$, the inequality $\|f(m)\| \leq C \prod_{i \in \iota} \|m_i\|$ holds.

ContinuousMultilinearMap.opNNNorm_prod theorem

 (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') : ‖f.prod g‖₊ = max ‖f‖₊ ‖g‖₊

Full source

theorem opNNNorm_prod (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :
    ‖f.prod g‖₊ = max ‖f‖₊ ‖g‖₊ :=
  eq_of_forall_ge_iff fun _ ↦ by
    simp only [opNNNorm_le_iff, prod_apply, Prod.nnnorm_def, max_le_iff, forall_and]

Operator Seminorm of Product of Continuous Multilinear Maps is Maximum of Seminorms

Informal description

Let $f$ and $g$ be continuous multilinear maps from a family of normed vector spaces $E$ over a nontrivially normed field $\mathbb{K}$ to normed vector spaces $G$ and $G'$ respectively. The operator seminorm of the product map $f \times g$ is equal to the maximum of the operator seminorms of $f$ and $g$, i.e., \[ \|f \times g\|_{\text{op}} = \max(\|f\|_{\text{op}}, \|g\|_{\text{op}}). \]

ContinuousMultilinearMap.opNorm_prod theorem

(f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') : ‖f.prod g‖ = max ‖f‖ ‖g‖

Full source

theorem opNorm_prod (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :
    ‖f.prod g‖ = max ‖f‖ ‖g‖ :=
  congr_arg NNReal.toReal (opNNNorm_prod f g)

Operator Norm of Product of Continuous Multilinear Maps is Maximum of Norms

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ a family of normed vector spaces over $\mathbb{K}$, and $G$, $G'$ normed vector spaces over $\mathbb{K}$. For any continuous multilinear maps $f \colon \prod_{i} E_i \to G$ and $g \colon \prod_{i} E_i \to G'$, the operator norm of their product map $f \times g \colon \prod_{i} E_i \to G \times G'$ satisfies \[ \|f \times g\| = \max(\|f\|, \|g\|). \]

ContinuousMultilinearMap.opNNNorm_pi theorem

 [∀ i', SeminormedAddCommGroup (E' i')] [∀ i', NormedSpace 𝕜 (E' i')] (f : ∀ i', ContinuousMultilinearMap 𝕜 E (E' i')) :
  ‖pi f‖₊ = ‖f‖₊

Full source

theorem opNNNorm_pi
    [∀ i', SeminormedAddCommGroup (E' i')] [∀ i', NormedSpace 𝕜 (E' i')]
    (f : ∀ i', ContinuousMultilinearMap 𝕜 E (E' i')) : ‖pi f‖₊ = ‖f‖₊ :=
  eq_of_forall_ge_iff fun _ ↦ by simpa [opNNNorm_le_iff, pi_nnnorm_le_iff] using forall_swap

Operator Seminorm of Product of Continuous Multilinear Maps Equals Supremum of Component Seminorms

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\iota'$ a finite index type, and for each $i' \in \iota'$, let $E'_{i'}$ be a seminormed additive commutative group and a normed space over $\mathbb{K}$. Given a family of continuous multilinear maps $f = (f_{i'} : \text{ContinuousMultilinearMap}_{\mathbb{K}} E (E'_{i'}))_{i' \in \iota'}$, the operator seminorm of the product map $\pi f$ (which combines all $f_{i'}$ into a single multilinear map) is equal to the supremum of the operator seminorms of the individual maps $f_{i'}$, i.e., $$\|\pi f\|_{\text{op}} = \sup_{i'} \|f_{i'}\|_{\text{op}}.$$

ContinuousMultilinearMap.opNorm_pi theorem

 {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'} [∀ i', SeminormedAddCommGroup (E' i')] [∀ i', NormedSpace 𝕜 (E' i')]
  (f : ∀ i', ContinuousMultilinearMap 𝕜 E (E' i')) : ‖pi f‖ = ‖f‖

Full source

theorem opNorm_pi {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'}
    [∀ i', SeminormedAddCommGroup (E' i')] [∀ i', NormedSpace 𝕜 (E' i')]
    (f : ∀ i', ContinuousMultilinearMap 𝕜 E (E' i')) :
    ‖pi f‖ = ‖f‖ :=
  congr_arg NNReal.toReal (opNNNorm_pi f)

Operator Norm of Product of Continuous Multilinear Maps Equals Supremum of Component Norms

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $\iota'$ a finite index type, and for each $i' \in \iota'$, let $E'_{i'}$ be a seminormed additive commutative group and a normed space over $\mathbb{K}$. Given a family of continuous multilinear maps $f = (f_{i'} : \text{ContinuousMultilinearMap}_{\mathbb{K}} E (E'_{i'}))_{i' \in \iota'}$, the operator norm of the product map $\pi f$ (which combines all $f_{i'}$ into a single multilinear map) is equal to the supremum of the operator norms of the individual maps $f_{i'}$, i.e., $$\|\pi f\| = \sup_{i'} \|f_{i'}\|.$$

ContinuousMultilinearMap.norm_ofSubsingleton theorem

[Subsingleton ι] (i : ι) (f : G →L[𝕜] G') : ‖ofSubsingleton 𝕜 G G' i f‖ = ‖f‖

Full source

@[simp]
theorem norm_ofSubsingleton [Subsingleton ι] (i : ι) (f : G →L[𝕜] G') :
    ‖ofSubsingleton 𝕜 G G' i f‖ = ‖f‖ := by
  letI : Unique ι := uniqueOfSubsingleton i
  simp [norm_def, ContinuousLinearMap.norm_def, (Equiv.funUnique _ _).symm.surjective.forall]

Operator Norm Preservation under Subsingleton Construction of Multilinear Maps

Informal description

Let $\iota$ be a finite index type with decidable equality that is a subsingleton (i.e., all elements are equal), and let $G$, $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$. For any $i \in \iota$ and any continuous linear map $f : G \to G'$, the operator norm of the continuous multilinear map constructed from $f$ via `ofSubsingleton` equals the operator norm of $f$, i.e., $$\|\text{ofSubsingleton}_{\mathbb{K},G,G'}(i, f)\| = \|f\|.$$

ContinuousMultilinearMap.norm_ofSubsingleton_id_le theorem

[Subsingleton ι] (i : ι) : ‖ofSubsingleton 𝕜 G G i (.id _ _)‖ ≤ 1

Full source

theorem norm_ofSubsingleton_id_le [Subsingleton ι] (i : ι) :
    ‖ofSubsingleton 𝕜 G G i (.id _ _)‖ ≤ 1 := by
  rw [norm_ofSubsingleton]
  apply ContinuousLinearMap.norm_id_le

Operator Norm Bound for Identity Map in Subsingleton Multilinear Construction

Informal description

Let $\iota$ be a finite index type with decidable equality that is a subsingleton (i.e., all elements are equal), and let $G$ be a normed vector space over a nontrivially normed field $\mathbb{K}$. For any $i \in \iota$, the operator norm of the continuous multilinear map constructed from the identity map $\text{id} \colon G \to G$ via `ofSubsingleton` satisfies $$\|\text{ofSubsingleton}_{\mathbb{K},G,G}(i, \text{id})\| \leq 1.$$

ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le theorem

[Subsingleton ι] (i : ι) : ‖ofSubsingleton 𝕜 G G i (.id _ _)‖₊ ≤ 1

Full source

theorem nnnorm_ofSubsingleton_id_le [Subsingleton ι] (i : ι) :
    ‖ofSubsingleton 𝕜 G G i (.id _ _)‖₊ ≤ 1 :=
  norm_ofSubsingleton_id_le _ _ _

Non-negative operator norm bound for identity map in subsingleton multilinear construction

Informal description

Let $\iota$ be a finite index type with decidable equality that is a subsingleton (i.e., all elements are equal), and let $G$ be a normed vector space over a nontrivially normed field $\mathbb{K}$. For any $i \in \iota$, the non-negative operator norm of the continuous multilinear map constructed from the identity map $\text{id} \colon G \to G$ via `ofSubsingleton` satisfies $$\|\text{ofSubsingleton}_{\mathbb{K},G,G}(i, \text{id})\|_{\mathbb{R}_+} \leq 1.$$

ContinuousMultilinearMap.norm_constOfIsEmpty theorem

[IsEmpty ι] (x : G) : ‖constOfIsEmpty 𝕜 E x‖ = ‖x‖

Full source

@[simp]
theorem norm_constOfIsEmpty [IsEmpty ι] (x : G) : ‖constOfIsEmpty 𝕜 E x‖ = ‖x‖ := by
  apply le_antisymm
  · refine opNorm_le_bound (norm_nonneg _) fun x => ?_
    rw [Fintype.prod_empty, mul_one, constOfIsEmpty_apply]
  · simpa using (constOfIsEmpty 𝕜 E x).le_opNorm 0

Operator Norm of Constant Multilinear Map on Empty Index Type

Informal description

For any normed vector space $G$ over a nontrivially normed field $\mathbb{K}$ and any empty index type $\iota$, the operator norm of the constant multilinear map `constOfIsEmpty 𝕜 E x` is equal to the norm of $x \in G$, i.e., $\|\text{constOfIsEmpty}_{\mathbb{K},E}(x)\| = \|x\|$.

ContinuousMultilinearMap.nnnorm_constOfIsEmpty theorem

[IsEmpty ι] (x : G) : ‖constOfIsEmpty 𝕜 E x‖₊ = ‖x‖₊

Full source

@[simp]
theorem nnnorm_constOfIsEmpty [IsEmpty ι] (x : G) : ‖constOfIsEmpty 𝕜 E x‖₊ = ‖x‖₊ :=
  NNReal.eq <| norm_constOfIsEmpty _ _ _

Non-negative operator norm equality for constant multilinear maps on empty index type

Informal description

For any normed vector space $G$ over a nontrivially normed field $\mathbb{K}$ and any empty index type $\iota$, the operator norm (with non-negative real values) of the constant multilinear map $\text{constOfIsEmpty}_{\mathbb{K},E}(x)$ is equal to the norm of $x \in G$, i.e., $\|\text{constOfIsEmpty}_{\mathbb{K},E}(x)\|_{\mathbb{R}_+} = \|x\|_{\mathbb{R}_+}$.

ContinuousMultilinearMap.norm_restrictScalars theorem

(f : ContinuousMultilinearMap 𝕜 E G) : ‖f.restrictScalars 𝕜'‖ = ‖f‖

Full source

@[simp]
theorem norm_restrictScalars (f : ContinuousMultilinearMap 𝕜 E G) :
    ‖f.restrictScalars 𝕜'‖ = ‖f‖ :=
  rfl

Invariance of Operator Norm under Scalar Restriction for Continuous Multilinear Maps

Informal description

Let $f$ be a continuous multilinear map from $E$ to $G$ over a nontrivially normed field $\mathbb{K}$. Then the operator norm of $f$ remains unchanged when restricting the scalar field to a subfield $\mathbb{K}'$ of $\mathbb{K}$, i.e., $\|f\|_{\mathbb{K}'} = \|f\|_{\mathbb{K}}$.

ContinuousMultilinearMap.norm_image_sub_le' theorem

 [DecidableEq ι] (f : ContinuousMultilinearMap 𝕜 E G) (m₁ m₂ : ∀ i, E i) :
  ‖f m₁ - f m₂‖ ≤ ‖f‖ * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Full source

/-- 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 norm_image_sub_le' [DecidableEq ι] (f : ContinuousMultilinearMap 𝕜 E G) (m₁ m₂ : ∀ i, E i) :
    ‖f m₁ - f m₂‖ ≤ ‖f‖ * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
  f.toMultilinearMap.norm_image_sub_le_of_bound' (norm_nonneg _) f.le_opNorm _ _

Precise Bound on Continuous Multilinear Map Difference: $\|f(m_1) - f(m_2)\|$ in Terms of Operator Norm and Input Differences

Informal description

Let $f$ be a continuous multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, where $\iota$ is a finite index type with decidable equality. For any two vectors $m_1, m_2 \in \prod_{i \in \iota} E_i$, the difference satisfies the inequality: \[ \|f(m_1) - f(m_2)\| \leq \|f\| \sum_{i \in \iota} \left( \|m_1(i) - m_2(i)\| \cdot \prod_{j \neq i} \max(\|m_1(j)\|, \|m_2(j)\|) \right). \]

ContinuousMultilinearMap.norm_image_sub_le theorem

 (f : ContinuousMultilinearMap 𝕜 E G) (m₁ m₂ : ∀ i, E i) :
  ‖f m₁ - f m₂‖ ≤ ‖f‖ * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Full source

/-- 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 norm_image_sub_le (f : ContinuousMultilinearMap 𝕜 E G) (m₁ m₂ : ∀ i, E i) :
    ‖f m₁ - f m₂‖ ≤ ‖f‖ * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖ :=
  f.toMultilinearMap.norm_image_sub_le_of_bound (norm_nonneg _) f.le_opNorm _ _

Lipschitz-like bound for continuous multilinear maps: $\|f(m_1) - f(m_2)\| \leq \|f\| \cdot |\iota| \cdot \max(\|m_1\|, \|m_2\|)^{|\iota| - 1} \cdot \|m_1 - m_2\|$

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, and for any $m_1, m_2 \in \prod_{i \in \iota} E_i$, the difference satisfies the inequality: \[ \|f(m_1) - f(m_2)\| \leq \|f\| \cdot |\iota| \cdot \max(\|m_1\|, \|m_2\|)^{|\iota| - 1} \cdot \|m_1 - m_2\|, \] where $|\iota|$ denotes the cardinality of the index set $\iota$.

MultilinearMap.mkContinuous_norm_le theorem

 (f : MultilinearMap 𝕜 E G) {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : ‖f.mkContinuous C H‖ ≤ C

Full source

/-- 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 (f : MultilinearMap 𝕜 E G) {C : ℝ} (hC : 0 ≤ C)
    (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : ‖f.mkContinuous C H‖ ≤ C :=
  ContinuousMultilinearMap.opNorm_le_bound hC fun m => H m

Operator Norm Bound for $\mathrm{mkContinuous}$ Construction: $\|\mathrm{mkContinuous}(f, C, H)\| \leq C$ when $C \geq 0$

Informal description

Let $f$ be a multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. If there exists a nonnegative real number $C$ such that for all $m \in \prod_i E_i$, the inequality $\|f(m)\| \leq C \cdot \prod_i \|m_i\|$ holds, then the operator norm of the continuous multilinear map $\mathrm{mkContinuous}(f, C, H)$ satisfies $\|\mathrm{mkContinuous}(f, C, H)\| \leq C$.

MultilinearMap.mkContinuous_norm_le' theorem

 (f : MultilinearMap 𝕜 E G) {C : ℝ} (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : ‖f.mkContinuous C H‖ ≤ max C 0

Full source

/-- 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' (f : MultilinearMap 𝕜 E G) {C : ℝ}
    (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : ‖f.mkContinuous C H‖ ≤ max C 0 :=
  ContinuousMultilinearMap.opNorm_le_bound (le_max_right _ _) fun m ↦ (H m).trans <|
    mul_le_mul_of_nonneg_right (le_max_left _ _) <| by positivity

Operator Norm Bound for $\mathrm{mkContinuous}$ Construction: $\|\mathrm{mkContinuous}(f, C, H)\| \leq \max(C, 0)$

Informal description

Let $f$ be a multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$. If there exists a real number $C$ such that for all $m \in \prod_i E_i$, the inequality $\|f(m)\| \leq C \cdot \prod_i \|m_i\|$ holds, then the operator norm of the continuous multilinear map $\mathrm{mkContinuous}(f, C, H)$ satisfies $\|\mathrm{mkContinuous}(f, C, H)\| \leq \max(C, 0)$.

ContinuousMultilinearMap.norm_restr theorem

 {k n : ℕ} (f : G [×n]→L[𝕜] G') (s : Finset (Fin n)) (hk : #s = k) (z : G) : ‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)

Full source

theorem norm_restr {k n : ℕ} (f : G [×n]→L[𝕜] G') (s : Finset (Fin n)) (hk : #s = k) (z : G) :
    ‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k) := by
  apply MultilinearMap.mkContinuous_norm_le
  exact mul_nonneg (norm_nonneg _) (pow_nonneg (norm_nonneg _) _)

Norm Bound for Restricted Continuous Multilinear Map: $\|f.\mathrm{restr}\,s\,hk\,z\| \leq \|f\| \cdot \|z\|^{n-k}$

Informal description

Let $f$ be a continuous multilinear map from $G^n$ to $G'$ over a nontrivially normed field $\mathbb{K}$. For any subset $s$ of $\mathrm{Fin}\,n$ with cardinality $k$, and any vector $z \in G$, the norm of the restricted map $f.\mathrm{restr}\,s\,hk\,z$ satisfies the inequality \[ \|f.\mathrm{restr}\,s\,hk\,z\| \leq \|f\| \cdot \|z\|^{n-k}. \]

ContinuousMultilinearMap.norm_mkPiAlgebra_le theorem

[Nonempty ι] : ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ 1

Full source

@[simp]
theorem norm_mkPiAlgebra_le [Nonempty ι] : ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ 1 := by
  refine opNorm_le_bound zero_le_one fun m => ?_
  simp only [ContinuousMultilinearMap.mkPiAlgebra_apply, one_mul]
  exact norm_prod_le' _ univ_nonempty _

Operator Norm Bound for $\mathrm{mkPiAlgebra}$ on Nonempty Index Type

Informal description

For a nonempty finite index type $\iota$ and a normed algebra $A$ over a nontrivially normed field $\mathbb{K}$, the operator norm of the continuous multilinear map $\mathrm{mkPiAlgebra}$ from $\mathbb{K}$ to $A$ indexed by $\iota$ satisfies $\|\mathrm{mkPiAlgebra}\| \leq 1$.

ContinuousMultilinearMap.norm_mkPiAlgebra_of_empty theorem

[IsEmpty ι] : ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = ‖(1 : A)‖

Full source

theorem norm_mkPiAlgebra_of_empty [IsEmpty ι] :
    ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = ‖(1 : A)‖ := by
  apply le_antisymm
  · apply opNorm_le_bound <;> simp
  · convert ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1
    simp [eq_empty_of_isEmpty univ]

Operator Norm of $\mathrm{mkPiAlgebra}$ on Empty Index Type Equals Norm of Identity

Informal description

For an empty index type $\iota$, the operator norm of the continuous multilinear map $\mathrm{mkPiAlgebra}_{\mathbb{K}}(\iota, A)$ is equal to the norm of the multiplicative identity $1$ in the normed algebra $A$ over the nontrivially normed field $\mathbb{K}$: \[ \|\mathrm{mkPiAlgebra}_{\mathbb{K}}(\iota, A)\| = \|1\|. \]

ContinuousMultilinearMap.norm_mkPiAlgebra theorem

[NormOneClass A] : ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1

Full source

@[simp]
theorem norm_mkPiAlgebra [NormOneClass A] : ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1 := by
  cases isEmpty_or_nonempty ι
  · simp [norm_mkPiAlgebra_of_empty]
  · refine le_antisymm norm_mkPiAlgebra_le ?_
    convert ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1
    simp

Operator Norm Identity for $\mathrm{mkPiAlgebra}$ in Norm-One Algebras

Informal description

For a normed algebra $A$ over a nontrivially normed field $\mathbb{K}$ with $\|1_A\| = 1$, and for any finite index type $\iota$, the operator norm of the continuous multilinear map $\mathrm{mkPiAlgebra}_{\mathbb{K}}(\iota, A)$ is equal to 1: \[ \|\mathrm{mkPiAlgebra}_{\mathbb{K}}(\iota, A)\| = 1. \]

ContinuousMultilinearMap.norm_mkPiAlgebraFin_succ_le theorem

: ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1

Full source

theorem norm_mkPiAlgebraFin_succ_le : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1 := by
  refine opNorm_le_bound zero_le_one fun m => ?_
  simp only [ContinuousMultilinearMap.mkPiAlgebraFin_apply, one_mul, List.ofFn_eq_map,
    Fin.prod_univ_def, Multiset.map_coe, Multiset.prod_coe]
  refine (List.norm_prod_le' ?_).trans_eq ?_
  · rw [Ne, List.map_eq_nil_iff, List.finRange_eq_nil]
    exact Nat.succ_ne_zero _
  rw [List.map_map, Function.comp_def]

Operator Norm Bound for $(n+1)$-ary Algebra Multiplication Map

Informal description

For any nontrivially normed field $\mathbb{K}$ and any normed algebra $A$ over $\mathbb{K}$ with $\|1\| = 1$, the operator norm of the continuous multilinear map $\text{mkPiAlgebraFin}_{\mathbb{K}}(n+1, A)$ is bounded by 1, i.e., $\|\text{mkPiAlgebraFin}_{\mathbb{K}}(n+1, A)\| \leq 1$.

ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos theorem

(hn : 0 < n) : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1

Full source

theorem norm_mkPiAlgebraFin_le_of_pos (hn : 0 < n) :
    ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1 := by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'
  exact norm_mkPiAlgebraFin_succ_le

Operator Norm Bound for Positive $n$-ary Algebra Multiplication Map

Informal description

For any nontrivially normed field $\mathbb{K}$ and any normed algebra $A$ over $\mathbb{K}$ with $\|1\| = 1$, if $n$ is a positive natural number, then the operator norm of the continuous multilinear map $\text{mkPiAlgebraFin}_{\mathbb{K}}(n, A)$ is bounded by 1, i.e., $\|\text{mkPiAlgebraFin}_{\mathbb{K}}(n, A)\| \leq 1$.

ContinuousMultilinearMap.norm_mkPiAlgebraFin_zero theorem

: ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖(1 : A)‖

Full source

theorem norm_mkPiAlgebraFin_zero : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖(1 : A)‖ := by
  refine le_antisymm ?_ ?_
  · refine opNorm_le_bound (norm_nonneg (1 : A)) ?_
    simp
  · convert ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun _ => (1 : A)
    simp

Operator Norm of Zero-Variable Algebra Multiplication Map: $\|\text{mkPiAlgebraFin}_{\mathbb{K}}(0, A)\| = \|1\|$

Informal description

For any nontrivially normed field $\mathbb{K}$ and any normed algebra $A$ over $\mathbb{K}$, the operator norm of the zero-variable continuous multilinear map $\text{mkPiAlgebraFin}_{\mathbb{K}}(0, A)$ is equal to the norm of the multiplicative identity $1$ in $A$, i.e., \[ \|\text{mkPiAlgebraFin}_{\mathbb{K}}(0, A)\| = \|1\|. \]

ContinuousMultilinearMap.norm_mkPiAlgebraFin_le theorem

: ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ max 1 ‖(1 : A)‖

Full source

theorem norm_mkPiAlgebraFin_le :
    ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ max 1 ‖(1 : A)‖ := by
  cases n
  · exact norm_mkPiAlgebraFin_zero.le.trans (le_max_right _ _)
  · exact (norm_mkPiAlgebraFin_le_of_pos (Nat.zero_lt_succ _)).trans (le_max_left _ _)

Operator Norm Bound for $n$-ary Algebra Multiplication Map: $\|\text{mkPiAlgebraFin}_{\mathbb{K}}(n, A)\| \leq \max(1, \|1\|)$

Informal description

For any nontrivially normed field $\mathbb{K}$ and any normed algebra $A$ over $\mathbb{K}$, the operator norm of the continuous multilinear map $\text{mkPiAlgebraFin}_{\mathbb{K}}(n, A)$ is bounded by the maximum of 1 and the norm of the multiplicative identity in $A$, i.e., \[ \|\text{mkPiAlgebraFin}_{\mathbb{K}}(n, A)\| \leq \max(1, \|1_A\|). \]

ContinuousMultilinearMap.norm_mkPiAlgebraFin theorem

[NormOneClass A] : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ = 1

Full source

@[simp]
theorem norm_mkPiAlgebraFin [NormOneClass A] :
    ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ = 1 := by
  cases n
  · rw [norm_mkPiAlgebraFin_zero]
    simp
  · refine le_antisymm norm_mkPiAlgebraFin_succ_le ?_
    refine le_of_eq_of_le ?_ <|
      ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (Nat.succ _) A) fun _ => 1
    simp

Operator Norm Identity for n-ary Algebra Multiplication Map: $\|\text{mkPiAlgebraFin}_{\mathbb{K}}(n, A)\| = 1$

Informal description

For any nontrivially normed field $\mathbb{K}$ and any normed algebra $A$ over $\mathbb{K}$ with $\|1\| = 1$, the operator norm of the continuous multilinear map $\text{mkPiAlgebraFin}_{\mathbb{K}}(n, A)$ is equal to 1, i.e., \[ \|\text{mkPiAlgebraFin}_{\mathbb{K}}(n, A)\| = 1. \]

ContinuousMultilinearMap.nnnorm_smulRight theorem

(f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) : ‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊

Full source

@[simp]
theorem nnnorm_smulRight (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
    ‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊ := by
  refine le_antisymm ?_ ?_
  · refine opNNNorm_le_iff.2 fun m => (nnnorm_smul_le _ _).trans ?_
    rw [mul_right_comm]
    gcongr
    exact le_opNNNorm _ _
  · obtain hz | hz := eq_zero_or_pos ‖z‖₊
    · simp [hz]
    rw [← le_div_iff₀ hz, opNNNorm_le_iff]
    intro m
    rw [div_mul_eq_mul_div, le_div_iff₀ hz]
    refine le_trans ?_ ((f.smulRight z).le_opNNNorm m)
    rw [smulRight_apply, nnnorm_smul]

Non-negative operator norm identity for scalar multiplication of multilinear maps: $\|f.smulRight\, z\| = \|f\| \cdot \|z\|$

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to the base field $\mathbb{K}$, and any element $z$ in a normed vector space $G$ over $\mathbb{K}$, the non-negative operator norm of the map $f.smulRight\, z$ (which sends $m$ to $f(m) \cdot z$) satisfies: \[ \|f.smulRight\, z\|_{\mathbb{R}_{\geq 0}} = \|f\|_{\mathbb{R}_{\geq 0}} \cdot \|z\|_{\mathbb{R}_{\geq 0}}. \]

ContinuousMultilinearMap.norm_smulRight theorem

(f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) : ‖f.smulRight z‖ = ‖f‖ * ‖z‖

Full source

@[simp]
theorem norm_smulRight (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
    ‖f.smulRight z‖ = ‖f‖ * ‖z‖ :=
  congr_arg NNReal.toReal (nnnorm_smulRight f z)

Operator Norm Identity for Scalar Multiplication of Multilinear Maps: $\|f \cdot z\| = \|f\| \cdot \|z\|$

Informal description

For any continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to the base field $\mathbb{K}$, and any element $z$ in a normed vector space $G$ over $\mathbb{K}$, the operator norm of the map $f \cdot z$ (which sends $m$ to $f(m) \cdot z$) satisfies: \[ \|f \cdot z\| = \|f\| \cdot \|z\|. \]

ContinuousMultilinearMap.norm_mkPiRing theorem

(z : G) : ‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖

Full source

@[simp]
theorem norm_mkPiRing (z : G) : ‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖ := by
  rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_mul]

Operator Norm Identity for $\mathrm{mkPiRing}$: $\|\mathrm{mkPiRing}_{\mathbb{K}}(\iota, z)\| = \|z\|$

Informal description

For any element $z$ in a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, and for any finite index type $\iota$, the operator norm of the continuous multilinear map $\mathrm{mkPiRing}_{\mathbb{K}}(\iota, z)$ is equal to the norm of $z$: \[ \|\mathrm{mkPiRing}_{\mathbb{K}}(\iota, z)\| = \|z\|. \]

ContinuousMultilinearMap.smulRightL_apply theorem

(f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) : smulRightL 𝕜 E G f z = f.smulRight z

Full source

@[simp] lemma smulRightL_apply (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
  smulRightL 𝕜 E G f z = f.smulRight z := rfl

Application of Scalar Multiplication Linear Map Equals Right Scalar Multiplication

Informal description

For any continuous multilinear map $f \colon \prod_{i \in \iota} E_i \to \mathbb{K}$ and any element $z \in G$, the application of the linear map $\text{smulRightL}_{\mathbb{K},E,G}$ to $f$ and $z$ equals the scalar multiplication of $f$ by $z$ on the right, i.e., \[ \text{smulRightL}_{\mathbb{K},E,G}(f)(z) = f.\text{smulRight}(z). \]

ContinuousMultilinearMap.norm_smulRightL_le theorem

: ‖smulRightL 𝕜 E G‖ ≤ 1

Full source

lemma norm_smulRightL_le : ‖smulRightL 𝕜 E G‖ ≤ 1 :=
  LinearMap.mkContinuous₂_norm_le _ zero_le_one _

Operator Norm Bound for Scalar Multiplication Linear Map: $\|\text{smulRightL}_{\mathbb{K}, E, G}\| \leq 1$

Informal description

The operator norm of the continuous linear map `smulRightL 𝕜 E G`, which sends a continuous multilinear map `f : ContinuousMultilinearMap 𝕜 E 𝕜` and an element `z : G` to the multilinear map `f.smulRight z`, is bounded above by 1. In other words, \[ \|\text{smulRightL}_{\mathbb{K}, E, G}\| \leq 1. \]

ContinuousLinearMap.norm_compContinuousMultilinearMap_le theorem

 (g : G →L[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) : ‖g.compContinuousMultilinearMap f‖ ≤ ‖g‖ * ‖f‖

Full source

theorem norm_compContinuousMultilinearMap_le (g : G →L[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) :
    ‖g.compContinuousMultilinearMap f‖ ≤ ‖g‖ * ‖f‖ :=
  ContinuousMultilinearMap.opNorm_le_bound (by positivity) fun m ↦
    calc
      ‖g (f m)‖ ≤ ‖g‖ * (‖f‖ * ∏ i, ‖m i‖) := g.le_opNorm_of_le <| f.le_opNorm _
      _ = _ := (mul_assoc _ _ _).symm

Operator Norm Inequality for Composition of Continuous Linear and Multilinear Maps

Informal description

Let $G$ and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $E$ be a family of normed vector spaces over $\mathbb{K}$. For any continuous linear map $g \colon G \to G'$ and any continuous multilinear map $f \colon \prod_{i \in \iota} E_i \to G$, the operator norm of the composition $g \circ f$ satisfies the inequality: \[ \|g \circ f\| \leq \|g\| \cdot \|f\|. \]

ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm theorem

(g : G ≃L[𝕜] G') : (g.continuousMultilinearMapCongrRight E).symm = g.symm.continuousMultilinearMapCongrRight E

Full source

@[simp]
theorem _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm (g : G ≃L[𝕜] G') :
    (g.continuousMultilinearMapCongrRight E).symm = g.symm.continuousMultilinearMapCongrRight E :=
  rfl

Inverse of Induced Isomorphism on Continuous Multilinear Maps

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $G$ and $G'$ be normed vector spaces over $\mathbb{K}$, and $E$ be a family of normed vector spaces over $\mathbb{K}$. For any continuous linear equivalence $g : G \to G'$, the inverse of the induced isomorphism $g.\text{continuousMultilinearMapCongrRight}(E)$ on the space of continuous multilinear maps is equal to the isomorphism induced by the inverse $g^{-1}$, i.e., \[ (g.\text{continuousMultilinearMapCongrRight}(E))^{-1} = g^{-1}.\text{continuousMultilinearMapCongrRight}(E). \]

ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply theorem

 (g : G ≃L[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) :
  g.continuousMultilinearMapCongrRight E f = (g : G →L[𝕜] G').compContinuousMultilinearMap f

Full source

@[simp]
theorem _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply (g : G ≃L[𝕜] G')
    (f : ContinuousMultilinearMap 𝕜 E G) :
    g.continuousMultilinearMapCongrRight E f = (g : G →L[𝕜] G').compContinuousMultilinearMap f :=
  rfl

Conjugation of Continuous Multilinear Map by Continuous Linear Equivalence

Informal description

Let $G$ and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $E$ be a family of normed vector spaces over $\mathbb{K}$. For any continuous linear equivalence $g \colon G \to G'$ and any continuous multilinear map $f \colon \prod_{i \in \iota} E_i \to G$, the continuous multilinear map obtained by conjugating $f$ with $g$ is equal to the composition of $f$ with the underlying continuous linear map of $g$, i.e., \[ g.\text{continuousMultilinearMapCongrRight}(E)(f) = (g \colon G \to_{\mathbb{K}} G') \circ f. \]

LinearIsometry.norm_compContinuousMultilinearMap theorem

 (g : G →ₗᵢ[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) : ‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖

Full source

theorem LinearIsometry.norm_compContinuousMultilinearMap (g : G →ₗᵢ[𝕜] G')
    (f : ContinuousMultilinearMap 𝕜 E G) :
    ‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖ := by
  simp only [ContinuousLinearMap.compContinuousMultilinearMap_coe,
    LinearIsometry.coe_toContinuousLinearMap, LinearIsometry.norm_map,
    ContinuousMultilinearMap.norm_def, Function.comp_apply]

Norm Preservation Under Composition with Linear Isometry

Informal description

Let $G$ and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $g : G \to G'$ be a linear isometry. For any continuous multilinear map $f$ from a family of normed vector spaces $E$ to $G$, the operator norm of the composition $g \circ f$ is equal to the operator norm of $f$, i.e., $\|g \circ f\| = \|f\|$.

MultilinearMap.mkContinuousLinear_norm_le' theorem

 (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ) (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) :
  ‖mkContinuousLinear f C H‖ ≤ max C 0

Full source

theorem mkContinuousLinear_norm_le' (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ)
    (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ max C 0 := by
  dsimp only [mkContinuousLinear]
  exact LinearMap.mkContinuous_norm_le _ (le_max_right _ _) _

Operator Norm Bound for Continuous Linear Extension of Multilinear Map

Informal description

Let $G$ and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f \colon G \to \text{MultilinearMap}(\mathbb{K}, E, G')$ be a linear map. Given a real constant $C \in \mathbb{R}$ such that for all $x \in G$ and all $m \in \prod_i E_i$, the inequality $\|f(x)(m)\| \leq C \cdot \|x\| \cdot \prod_i \|m_i\|$ holds, then the operator norm of the continuous multilinear map constructed via `mkContinuousLinear` satisfies $\|\text{mkContinuousLinear}(f, C, H)\| \leq \max(C, 0)$.

MultilinearMap.mkContinuousLinear_norm_le theorem

 (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') {C : ℝ} (hC : 0 ≤ C) (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) :
  ‖mkContinuousLinear f C H‖ ≤ C

Full source

theorem mkContinuousLinear_norm_le (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') {C : ℝ} (hC : 0 ≤ C)
    (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ C :=
  (mkContinuousLinear_norm_le' f C H).trans_eq (max_eq_left hC)

Operator Norm Bound for Nonnegative Constant: $\|\text{mkContinuousLinear}(f, C, H)\| \leq C$

Informal description

Let $G$ and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f \colon G \to \text{MultilinearMap}(\mathbb{K}, E, G')$ be a linear map. Given a nonnegative real constant $C \geq 0$ such that for all $x \in G$ and all $m \in \prod_i E_i$, the inequality $\|f(x)(m)\| \leq C \cdot \|x\| \cdot \prod_i \|m_i\|$ holds, then the operator norm of the continuous multilinear map constructed via `mkContinuousLinear` satisfies $\|\text{mkContinuousLinear}(f, C, H)\| \leq C$.

MultilinearMap.mkContinuousMultilinear_apply theorem

 (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ} (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖)
  (m : ∀ i, E i) : ⇑(mkContinuousMultilinear f C H m) = f m

Full source

@[simp]
theorem mkContinuousMultilinear_apply (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ}
    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) (m : ∀ i, E i) :
    ⇑(mkContinuousMultilinear f C H m) = f m :=
  rfl

Equality of Constructed Continuous Multilinear Map with Original Multilinear Map

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $E'$ be families of normed vector spaces over $\mathbb{K}$ indexed by finite types $\iota$ and $\iota'$ respectively, and $G$ be a normed vector space over $\mathbb{K}$. Given a multilinear map $f \colon \prod_{i} E_i \to \text{MultilinearMap}(\mathbb{K}, E', G)$, a constant $C \in \mathbb{R}$, and a hypothesis $H$ stating that for all $m_1 \in \prod_{i} E_i$ and $m_2 \in \prod_{i} E'_i$, the inequality $\|f(m_1)(m_2)\| \leq (C \prod_i \|m_{1,i}\|) \prod_i \|m_{2,i}\|$ holds, then for any $m \in \prod_i E_i$, the continuous multilinear map $\text{mkContinuousMultilinear}(f, C, H)(m)$ coincides with $f(m)$.

MultilinearMap.mkContinuousMultilinear_norm_le' theorem

 (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ) (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) :
  ‖mkContinuousMultilinear f C H‖ ≤ max C 0

Full source

theorem mkContinuousMultilinear_norm_le' (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ)
    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) :
    ‖mkContinuousMultilinear f C H‖ ≤ max C 0 := by
  dsimp only [mkContinuousMultilinear]
  exact mkContinuous_norm_le _ (le_max_right _ _) _

Operator Norm Bound for $\mathrm{mkContinuousMultilinear}$: $\|\mathrm{mkContinuousMultilinear}(f, C, H)\| \leq \max(C, 0)$

Informal description

Let $f$ be a multilinear map from a family of normed vector spaces $(E_i)_{i \in \iota}$ to the space of multilinear maps from another family $(E'_i)_{i \in \iota'}$ to a normed vector space $G$, all over a nontrivially normed field $\mathbb{K}$. Given a real number $C$ such that for all $m_1 \in \prod_i E_i$ and $m_2 \in \prod_i E'_i$, the inequality \[ \|f(m_1)(m_2)\| \leq \left(C \prod_i \|m_{1,i}\|\right) \prod_i \|m_{2,i}\| \] holds, then the operator norm of the continuous multilinear map $\mathrm{mkContinuousMultilinear}(f, C, H)$ satisfies \[ \|\mathrm{mkContinuousMultilinear}(f, C, H)\| \leq \max(C, 0). \]

MultilinearMap.mkContinuousMultilinear_norm_le theorem

 (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ} (hC : 0 ≤ C)
  (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) : ‖mkContinuousMultilinear f C H‖ ≤ C

Full source

theorem mkContinuousMultilinear_norm_le (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ}
    (hC : 0 ≤ C) (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) :
    ‖mkContinuousMultilinear f C H‖ ≤ C :=
  (mkContinuousMultilinear_norm_le' f C H).trans_eq (max_eq_left hC)

Operator Norm Bound for $\text{mkContinuousMultilinear}$: $\|\text{mkContinuousMultilinear}(f, C, H)\| \leq C$ when $C \geq 0$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E$ and $E'$ be families of normed vector spaces over $\mathbb{K}$ indexed by finite types $\iota$ and $\iota'$ respectively, and $G$ be a normed vector space over $\mathbb{K}$. Given a multilinear map $f \colon \prod_{i} E_i \to \text{MultilinearMap}(\mathbb{K}, E', G)$, a nonnegative constant $C \geq 0$, and a hypothesis $H$ stating that for all $m_1 \in \prod_{i} E_i$ and $m_2 \in \prod_{i} E'_i$, the inequality $\|f(m_1)(m_2)\| \leq (C \prod_i \|m_{1,i}\|) \prod_i \|m_{2,i}\|$ holds, then the operator norm of the continuous multilinear map $\text{mkContinuousMultilinear}(f, C, H)$ satisfies $\|\text{mkContinuousMultilinear}(f, C, H)\| \leq C$.

ContinuousMultilinearMap.norm_compContinuousLinearMap_le theorem

 (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : ∀ i, E i →L[𝕜] E₁ i) : ‖g.compContinuousLinearMap f‖ ≤ ‖g‖ * ∏ i, ‖f i‖

Full source

theorem norm_compContinuousLinearMap_le (g : ContinuousMultilinearMap 𝕜 E₁ G)
    (f : ∀ i, E i →L[𝕜] E₁ i) : ‖g.compContinuousLinearMap f‖ ≤ ‖g‖ * ∏ i, ‖f i‖ :=
  opNorm_le_bound (by positivity) fun m =>
    calc
      ‖g fun i => f i (m i)‖ ≤ ‖g‖ * ∏ i, ‖f i (m i)‖ := g.le_opNorm _
      _ ≤ ‖g‖ * ∏ i, ‖f i‖ * ‖m i‖ :=
        (mul_le_mul_of_nonneg_left
          (prod_le_prod (fun _ _ => norm_nonneg _) fun i _ => (f i).le_opNorm (m i))
          (norm_nonneg g))
      _ = (‖g‖ * ∏ i, ‖f i‖) * ∏ i, ‖m i‖ := by rw [prod_mul_distrib, mul_assoc]

Operator Norm Inequality for Composition of Continuous Multilinear and Linear Maps: $\|g \circ (f_i)\| \leq \|g\| \cdot \prod_i \|f_i\|$

Informal description

Let $g$ be a continuous multilinear map from a family of normed vector spaces $(E_{1,i})_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, and let $f_i \colon E_i \to E_{1,i}$ be a family of continuous linear maps. Then the operator norm of the composition $g \circ (f_i)_{i \in \iota}$ satisfies the inequality: \[ \|g \circ (f_i)_{i \in \iota}\| \leq \|g\| \cdot \prod_{i \in \iota} \|f_i\|. \]

ContinuousMultilinearMap.norm_compContinuous_linearIsometry_le theorem

 (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : ∀ i, E i →ₗᵢ[𝕜] E₁ i) :
  ‖g.compContinuousLinearMap fun i => (f i).toContinuousLinearMap‖ ≤ ‖g‖

Full source

theorem norm_compContinuous_linearIsometry_le (g : ContinuousMultilinearMap 𝕜 E₁ G)
    (f : ∀ i, E i →ₗᵢ[𝕜] E₁ i) :
    ‖g.compContinuousLinearMap fun i => (f i).toContinuousLinearMap‖ ≤ ‖g‖ := by
  refine opNorm_le_bound (norm_nonneg _) fun m => ?_
  apply (g.le_opNorm _).trans _
  simp only [ContinuousLinearMap.coe_coe, LinearIsometry.coe_toContinuousLinearMap,
    LinearIsometry.norm_map, le_rfl]

Operator Norm Bound for Composition with Linear Isometries

Informal description

Let $G$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $(E_i)_{i \in \iota}$ and $(E'_i)_{i \in \iota}$ be families of normed vector spaces over $\mathbb{K}$. For any continuous multilinear map $g \colon \prod_{i \in \iota} E'_i \to G$ and any family of linear isometries $f_i \colon E_i \to E'_i$, the operator norm of the composition $g \circ (f_i)_{i \in \iota}$ satisfies \[ \|g \circ (f_i)_{i \in \iota}\| \leq \|g\|. \]

ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv theorem

 (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : ∀ i, E i ≃ₗᵢ[𝕜] E₁ i) :
  ‖g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)‖ = ‖g‖

Full source

theorem norm_compContinuous_linearIsometryEquiv (g : ContinuousMultilinearMap 𝕜 E₁ G)
    (f : ∀ i, E i ≃ₗᵢ[𝕜] E₁ i) :
    ‖g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)‖ = ‖g‖ := by
  apply le_antisymm (g.norm_compContinuous_linearIsometry_le fun i => (f i).toLinearIsometry)
  have : g = (g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)).compContinuousLinearMap
      fun i => ((f i).symm : E₁ i →L[𝕜] E i) := by
    ext1 m
    simp only [compContinuousLinearMap_apply, LinearIsometryEquiv.coe_coe'',
      LinearIsometryEquiv.apply_symm_apply]
  conv_lhs => rw [this]
  apply (g.compContinuousLinearMap fun i =>
    (f i : E i →L[𝕜] E₁ i)).norm_compContinuous_linearIsometry_le
      fun i => (f i).symm.toLinearIsometry

Operator Norm Preservation under Composition with Linear Isometric Isomorphisms: $\|g \circ (f_i)\| = \|g\|$

Informal description

Let $G$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $(E_i)_{i \in \iota}$ and $(E'_i)_{i \in \iota}$ be families of normed vector spaces over $\mathbb{K}$. For any continuous multilinear map $g \colon \prod_{i \in \iota} E'_i \to G$ and any family of linear isometric isomorphisms $f_i \colon E_i \to E'_i$, the operator norm of the composition $g \circ (f_i)_{i \in \iota}$ satisfies \[ \|g \circ (f_i)_{i \in \iota}\| = \|g\|. \]

ContinuousMultilinearMap.compContinuousLinearMapL_apply theorem

 (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : ∀ i, E i →L[𝕜] E₁ i) :
  compContinuousLinearMapL f g = g.compContinuousLinearMap f

Full source

@[simp]
theorem compContinuousLinearMapL_apply (g : ContinuousMultilinearMap 𝕜 E₁ G)
    (f : ∀ i, E i →L[𝕜] E₁ i) : compContinuousLinearMapL f g = g.compContinuousLinearMap f :=
  rfl

Application of Continuous Linear Map Composition Operator

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $(E_i)_{i \in \iota}$ and $(E'_i)_{i \in \iota}$ be families of normed vector spaces over $\mathbb{K}$, and $G$ be a normed vector space over $\mathbb{K}$. For any continuous multilinear map $g \colon \prod_{i \in \iota} E'_i \to G$ and any family of continuous linear maps $f_i \colon E_i \to E'_i$, the application of the continuous linear map composition operator satisfies \[ \text{compContinuousLinearMapL}(f)(g) = g \circ (f_i)_{i \in \iota}. \]

ContinuousMultilinearMap.norm_compContinuousLinearMapL_le theorem

(f : ∀ i, E i →L[𝕜] E₁ i) : ‖compContinuousLinearMapL (G := G) f‖ ≤ ∏ i, ‖f i‖

Full source

theorem norm_compContinuousLinearMapL_le (f : ∀ i, E i →L[𝕜] E₁ i) :
    ‖compContinuousLinearMapL (G := G) f‖ ≤ ∏ i, ‖f i‖ :=
  LinearMap.mkContinuous_norm_le _ (by positivity) _

Operator Norm Bound for Composition with Continuous Linear Maps: $\|\text{compContinuousLinearMapL}(f)\| \leq \prod \|f_i\|$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $(E_i)_{i \in \iota}$ and $(E'_i)_{i \in \iota}$ be families of normed vector spaces over $\mathbb{K}$, and $G$ be a normed vector space over $\mathbb{K}$. For any family of continuous linear maps $f_i \colon E_i \to E'_i$, the operator norm of the composition operator $\text{compContinuousLinearMapL}(f)$ satisfies \[ \|\text{compContinuousLinearMapL}(f)\| \leq \prod_{i} \|f_i\|. \]

ContinuousMultilinearMap.compContinuousLinearMapLRight_apply theorem

 (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : ∀ i, E i →L[𝕜] E₁ i) :
  compContinuousLinearMapLRight g f = g.compContinuousLinearMap f

Full source

@[simp]
theorem compContinuousLinearMapLRight_apply (g : ContinuousMultilinearMap 𝕜 E₁ G)
    (f : ∀ i, E i →L[𝕜] E₁ i) : compContinuousLinearMapLRight g f = g.compContinuousLinearMap f :=
  rfl

Right Composition of Continuous Multilinear Map with Linear Maps: $\text{compContinuousLinearMapLRight}(g)(f) = g \circ (f_i)_i$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $(E_i)_{i \in \iota}$ and $(E'_i)_{i \in \iota}$ be families of normed vector spaces over $\mathbb{K}$, and $G$ be a normed vector space over $\mathbb{K}$. For any continuous multilinear map $g \colon \prod_{i \in \iota} E'_i \to G$ and any family of continuous linear maps $f_i \colon E_i \to E'_i$, the application of the right continuous linear map composition operator satisfies \[ \text{compContinuousLinearMapLRight}(g)(f) = g \circ (f_i)_{i \in \iota}. \]

ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le theorem

(g : ContinuousMultilinearMap 𝕜 E₁ G) : ‖compContinuousLinearMapLRight (E := E) g‖ ≤ ‖g‖

Full source

theorem norm_compContinuousLinearMapLRight_le (g : ContinuousMultilinearMap 𝕜 E₁ G) :
    ‖compContinuousLinearMapLRight (E := E) g‖ ≤ ‖g‖ :=
  MultilinearMap.mkContinuous_norm_le _ (norm_nonneg _) _

Operator Norm Bound for Right Composition with Continuous Linear Maps: $\|\text{compContinuousLinearMapLRight}(g)\| \leq \|g\|$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $(E_i)_{i \in \iota}$ and $(E'_i)_{i \in \iota}$ be families of normed vector spaces over $\mathbb{K}$, and $G$ be a normed vector space over $\mathbb{K}$. For any continuous multilinear map $g \colon \prod_i E'_i \to G$, the operator norm of the right composition operator $\text{compContinuousLinearMapLRight}(g)$ satisfies \[ \|\text{compContinuousLinearMapLRight}(g)\| \leq \|g\|. \]

ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm theorem

 (f : ∀ i, E i ≃L[𝕜] E₁ i) :
  (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft G f).symm =
    .continuousMultilinearMapCongrLeft G fun i : ι => (f i).symm

Full source

@[simp]
theorem _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm
    (f : ∀ i, E i ≃L[𝕜] E₁ i) :
    (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft G f).symm =
      .continuousMultilinearMapCongrLeft G fun i : ι => (f i).symm :=
  rfl

Inverse of Continuous Multilinear Map Congruence via Linear Equivalences

Informal description

Let $E$ and $E₁$ be families of normed vector spaces over a nontrivially normed field $\mathbb{K}$, indexed by a finite type $\iota$. For any family of continuous linear equivalences $f_i : E_i \simeq_{L[\mathbb{K}]} E₁_i$ (for each $i \in \iota$), the inverse of the induced continuous linear equivalence on the space of continuous multilinear maps $\text{ContinuousMultilinearMap}(\mathbb{K}, E₁, G) \simeq_{L[\mathbb{K}]} \text{ContinuousMultilinearMap}(\mathbb{K}, E, G)$ is equal to the continuous linear equivalence induced by the family of inverses $(f_i)^{-1} : E₁_i \simeq_{L[\mathbb{K}]} E_i$.

ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply theorem

 (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : ∀ i, E i ≃L[𝕜] E₁ i) :
  ContinuousLinearEquiv.continuousMultilinearMapCongrLeft G f g =
    g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)

Full source

@[simp]
theorem _root_.ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply
    (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : ∀ i, E i ≃L[𝕜] E₁ i) :
    ContinuousLinearEquiv.continuousMultilinearMapCongrLeft G f g =
      g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i) :=
  rfl

Action of Linear Isomorphisms on Continuous Multilinear Maps via Congruence

Informal description

Let $G$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, and let $E_i$ and $E'_i$ be families of normed vector spaces over $\mathbb{K}$ indexed by a finite set $I$. For any continuous multilinear map $g \colon \prod_{i \in I} E'_i \to G$ and any family of continuous linear isomorphisms $f_i \colon E_i \to E'_i$ for each $i \in I$, the map $\text{continuousMultilinearMapCongrLeft}_G(f)(g)$ is equal to the composition of $g$ with the family of continuous linear maps $(f_i)_{i \in I}$.

ContinuousMultilinearMap.iteratedFDerivComponent_apply theorem

 {α : Type*} [Fintype α] (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ s) [DecidablePred (· ∈ s)]
  (v : ∀ i : { a : ι // a ∉ s }, E₁ i) (w : α → (∀ i, E₁ i)) :
  f.iteratedFDerivComponent e v w = f (fun j ↦ if h : j ∈ s then w (e.symm ⟨j, h⟩) j else v ⟨j, h⟩)

Full source

@[simp] lemma iteratedFDerivComponent_apply {α : Type*} [Fintype α]
    (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ s) [DecidablePred (· ∈ s)]
    (v : ∀ i : {a : ι // a ∉ s}, E₁ i) (w : α → (∀ i, E₁ i)) :
    f.iteratedFDerivComponent e v w =
      f (fun j ↦ if h : j ∈ s then w (e.symm ⟨j, h⟩) j else v ⟨j, h⟩) := by
  simp [iteratedFDerivComponent, MultilinearMap.iteratedFDerivComponent,
    MultilinearMap.domDomRestrictₗ]

Expression for Iterated Fréchet Derivative Component of a Continuous Multilinear Map

Informal description

Let $E₁$ be a family of normed vector spaces over a nontrivially normed field $\mathbb{K}$, indexed by a finite set $\iota$, and let $G$ be another normed vector space over $\mathbb{K}$. Given a continuous multilinear map $f \colon \prod_{i \in \iota} E₁_i \to G$, a subset $s \subset \iota$, a bijection $e \colon \alpha \simeq s$ where $\alpha$ is a finite type, and vectors $v \colon \prod_{i \notin s} E₁_i$ and $w \colon \alpha \to \prod_{i \in \iota} E₁_i$, the iterated Fréchet derivative component of $f$ satisfies \[ f_{\text{iteratedFDerivComponent}}(e, v, w) = f\left(\lambda j \mapsto \begin{cases} w(e^{-1}(j))_j & \text{if } j \in s, \\ v_j & \text{if } j \notin s. \end{cases}\right). \]

ContinuousMultilinearMap.norm_iteratedFDerivComponent_le theorem

 {α : Type*} [Fintype α] (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ s) [DecidablePred (· ∈ s)]
  (x : (i : ι) → E₁ i) : ‖f.iteratedFDerivComponent e (x ·)‖ ≤ ‖f‖ * ‖x‖ ^ (Fintype.card ι - Fintype.card α)

Full source

lemma norm_iteratedFDerivComponent_le {α : Type*} [Fintype α]
    (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ s) [DecidablePred (· ∈ s)]
    (x : (i : ι) → E₁ i) :
    ‖f.iteratedFDerivComponent e (x ·)‖ ≤ ‖f‖ * ‖x‖ ^ (Fintype.card ι - Fintype.card α) := calc
  ‖f.iteratedFDerivComponent e (fun i ↦ x i)‖
    ≤ ‖f.iteratedFDerivComponent e‖ * ∏ i : {a : ι // a ∉ s}, ‖x i‖ :=
      ContinuousMultilinearMap.le_opNorm _ _
  _ ≤ ‖f‖ * ∏ _i : {a : ι // a ∉ s}, ‖x‖ := by
      gcongr
      · exact MultilinearMap.mkContinuousMultilinear_norm_le _ (norm_nonneg _) _
      · exact norm_le_pi_norm _ _
  _ = ‖f‖ * ‖x‖ ^ (Fintype.card {a : ι // a ∉ s}) := by rw [prod_const, card_univ]
  _ = ‖f‖ * ‖x‖ ^ (Fintype.card ι - Fintype.card α) := by simp [Fintype.card_congr e]

Norm Bound for Iterated Fréchet Derivative Component: $\|f_{\text{iteratedFDerivComponent}}(e, x)\| \leq \|f\| \cdot \|x\|^{|\iota| - |\alpha|}$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E₁$ a family of normed vector spaces over $\mathbb{K}$ indexed by a finite set $\iota$, and $G$ a normed vector space over $\mathbb{K}$. For any continuous multilinear map $f \colon \prod_{i \in \iota} E₁_i \to G$, finite type $\alpha$, subset $s \subset \iota$ with a bijection $e \colon \alpha \simeq s$, and vector $x \in \prod_{i \in \iota} E₁_i$, the norm of the iterated Fréchet derivative component satisfies \[ \|f_{\text{iteratedFDerivComponent}}(e, x)\| \leq \|f\| \cdot \|x\|^{|\iota| - |\alpha|}, \] where $|\iota|$ and $|\alpha|$ denote the cardinalities of $\iota$ and $\alpha$ respectively.

ContinuousMultilinearMap.norm_iteratedFDeriv_le' theorem

 (f : ContinuousMultilinearMap 𝕜 E₁ G) (k : ℕ) (x : (i : ι) → E₁ i) :
  ‖f.iteratedFDeriv k x‖ ≤ Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Full source

/-- Controlling the norm of `f.iteratedFDeriv` when `f` is continuous multilinear. For the same
bound on the iterated derivative of `f` in the calculus sense,
see `ContinuousMultilinearMap.norm_iteratedFDeriv_le`. -/
lemma norm_iteratedFDeriv_le' (f : ContinuousMultilinearMap 𝕜 E₁ G) (k : ℕ) (x : (i : ι) → E₁ i) :
    ‖f.iteratedFDeriv k x‖
      ≤ Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
  classical
  calc ‖f.iteratedFDeriv k x‖
  _ ≤ ∑ e : Fin k ↪ ι, ‖iteratedFDerivComponent f e.toEquivRange (fun i ↦ x i)‖ := norm_sum_le _ _
  _ ≤ ∑ _ : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
    gcongr with e _
    simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x
  _ = Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
    simp [card_univ, mul_assoc]

Norm Bound for Iterated Fréchet Derivative: $\|f^{(k)}(x)\| \leq \binom{|\iota|}{k} k! \cdot \|f\| \cdot \|x\|^{|\iota| - k}$

Informal description

Let $\mathbb{K}$ be a nontrivially normed field, $E₁$ a family of normed vector spaces over $\mathbb{K}$ indexed by a finite set $\iota$, and $G$ a normed vector space over $\mathbb{K}$. For any continuous multilinear map $f \colon \prod_{i \in \iota} E₁_i \to G$, natural number $k$, and vector $x \in \prod_{i \in \iota} E₁_i$, the norm of the $k$-th iterated Fréchet derivative of $f$ at $x$ satisfies \[ \|f^{(k)}(x)\| \leq \binom{|\iota|}{k} k! \cdot \|f\| \cdot \|x\|^{|\iota| - k}, \] where $|\iota|$ denotes the cardinality of $\iota$ and $\binom{|\iota|}{k} k!$ is the descending factorial of $|\iota|$ and $k$.

ContinuousMultilinearMap.opNorm_zero_iff theorem

{f : ContinuousMultilinearMap 𝕜 E G} : ‖f‖ = 0 ↔ f = 0

Full source

/-- A continuous linear map is zero iff its norm vanishes. -/
theorem opNorm_zero_iff {f : ContinuousMultilinearMap 𝕜 E G} : ‖f‖‖f‖ = 0 ↔ f = 0 := by
  simp [← (opNorm_nonneg f).le_iff_eq, opNorm_le_iff le_rfl, ContinuousMultilinearMap.ext_iff]

Vanishing Operator Norm Characterizes Zero Continuous Multilinear Maps

Informal description

For a continuous multilinear map $f$ from a family of normed vector spaces $(E_i)_{i \in \iota}$ to a normed vector space $G$ over a nontrivially normed field $\mathbb{K}$, the operator norm $\|f\|$ is zero if and only if $f$ is identically zero.

ContinuousMultilinearMap.norm_ofSubsingleton_id theorem

[Subsingleton ι] [Nontrivial G] (i : ι) : ‖ofSubsingleton 𝕜 G G i (.id _ _)‖ = 1

Full source

theorem norm_ofSubsingleton_id [Subsingleton ι] [Nontrivial G] (i : ι) :
    ‖ofSubsingleton 𝕜 G G i (.id _ _)‖ = 1 := by
  simp

Operator Norm of Identity via Subsingleton Construction is 1

Informal description

Let $\iota$ be a finite index type with decidable equality that is a subsingleton (i.e., all elements are equal), and let $G$ be a nontrivial normed vector space over a nontrivially normed field $\mathbb{K}$. For any $i \in \iota$, the operator norm of the continuous multilinear map constructed from the identity map $\text{id}_{\mathbb{K} G}$ via `ofSubsingleton` equals $1$, i.e., $$\|\text{ofSubsingleton}_{\mathbb{K},G,G}(i, \text{id}_{\mathbb{K} G})\| = 1.$$

ContinuousMultilinearMap.nnnorm_ofSubsingleton_id theorem

[Subsingleton ι] [Nontrivial G] (i : ι) : ‖ofSubsingleton 𝕜 G G i (.id _ _)‖₊ = 1

Full source

theorem nnnorm_ofSubsingleton_id [Subsingleton ι] [Nontrivial G] (i : ι) :
    ‖ofSubsingleton 𝕜 G G i (.id _ _)‖₊ = 1 :=
  NNReal.eq <| norm_ofSubsingleton_id ..

Operator Seminorm of Identity via Subsingleton Construction is 1

Informal description

Let $\iota$ be a finite index type with decidable equality that is a subsingleton (i.e., all elements are equal), and let $G$ be a nontrivial normed vector space over a nontrivially normed field $\mathbb{K}$. For any $i \in \iota$, the operator seminorm (nonnegative norm) of the continuous multilinear map constructed from the identity map $\text{id}_{\mathbb{K} G}$ via `ofSubsingleton` equals $1$, i.e., $$\|\text{ofSubsingleton}_{\mathbb{K},G,G}(i, \text{id}_{\mathbb{K} G})\|_+ = 1.$$

MultilinearMap.bound_of_shell theorem

 (f : MultilinearMap 𝕜 E G) {ε : ι → ℝ} {C : ℝ} {c : ι → 𝕜} (hε : ∀ i, 0 < ε i) (hc : ∀ i, 1 < ‖c i‖)
  (hf : ∀ m : ∀ i, E i, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m : ∀ i, E i) :
  ‖f m‖ ≤ C * ∏ i, ‖m i‖

Full source

/-- 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`. -/
theorem bound_of_shell (f : MultilinearMap 𝕜 E G) {ε : ι → ℝ} {C : ℝ} {c : ι → 𝕜}
    (hε : ∀ i, 0 < ε i) (hc : ∀ i, 1 < ‖c i‖)
    (hf : ∀ m : ∀ i, E i, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖)
    (m : ∀ i, E i) : ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
  bound_of_shell_of_norm_map_coord_zero f
    (fun h ↦ by rw [map_coord_zero f _ (norm_eq_zero.1 h), norm_zero]) hε hc hf m

Shell Condition Implies Global Bound for Multilinear Maps

Informal description

Let $f$ be a multilinear map on a family of normed vector spaces $(E_i)_{i \in \iota}$ over a nontrivially normed field $\mathbb{K}$. Suppose there exist positive numbers $\varepsilon_i > 0$ and elements $c_i \in \mathbb{K}$ with $\|c_i\| > 1$ for each $i \in \iota$, such that for all $m \in \prod_{i \in \iota} E_i$ satisfying $\varepsilon_i / \|c_i\| \leq \|m_i\| < \varepsilon_i$ for each $i$, the inequality $\|f(m)\| \leq C \prod_{i} \|m_i\|$ holds. Then for all $m \in \prod_{i \in \iota} E_i$, the inequality $\|f(m)\| \leq C \prod_{i} \|m_i\|$ holds.

Mathlib.Analysis.NormedSpace.Multilinear.Basic

Main results

Implementation notes