# Operator norm on the space of continuous multilinear maps #

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

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

## Main results #

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

- `exists_bound_of_continuous` asserts that, if `f` is continuous, then there exists `C > 0` with `‖f m‖ ≤ C * ∏ i, ‖m i‖` for all `m`.
- `continuous_of_bound`, conversely, asserts that this bound implies continuity.
- `mkContinuous` constructs the associated continuous multilinear map.

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

- `‖f‖` is its norm, i.e., the smallest number such that `‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖` for all `m`.
- `le_opNorm f m` asserts the fundamental inequality `‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖`.
- `norm_image_sub_le f m₁ m₂` gives a control of the difference `f m₁ - f m₂` in terms of `‖f‖` and `‖m₁ - m₂‖`.

## Implementation notes #

We mostly follow the API (and the proofs) of `OperatorNorm.lean`, with the additional complexity that we should deal with multilinear maps in several variables.

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

### Type variables #

We use the following type variables in this file:

- `𝕜` : a `NontriviallyNormedField`;
- `ι`, `ι'` : finite index types with decidable equality;
- `E`, `E₁` : families of normed vector spaces over `𝕜` indexed by `i : ι`;
- `E'` : a family of normed vector spaces over `𝕜` indexed by `i' : ι'`;
- `Ei` : a family of normed vector spaces over `𝕜` indexed by `i : Fin (Nat.succ n)`;
- `G`, `G'` : normed vector spaces over `𝕜`.

source
instance ContinuousMultilinearMap.instContinuousEval {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [Finite ι] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module 𝕜 F] :
ContinuousEval (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) F
source
theorem ContinuousLinearMap.continuous_uncurry_of_multilinear {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [Finite ι] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module 𝕜 F] {G : Type u_5} [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] [ContinuousConstSMul 𝕜 F] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) :
Continuous fun (p : G × ((i : ι) → E i)) => (f p.1) p.2
source
theorem ContinuousLinearMap.continuousOn_uncurry_of_multilinear {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [Finite ι] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module 𝕜 F] {G : Type u_5} [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] [ContinuousConstSMul 𝕜 F] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {s : Set (G × ((i : ι) → E i))} :
ContinuousOn (fun (p : G × ((i : ι) → E i)) => (f p.1) p.2) s
source
theorem ContinuousLinearMap.continuousAt_uncurry_of_multilinear {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [Finite ι] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module 𝕜 F] {G : Type u_5} [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] [ContinuousConstSMul 𝕜 F] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {x : G × ((i : ι) → E i)} :
ContinuousAt (fun (p : G × ((i : ι) → E i)) => (f p.1) p.2) x
source
theorem ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [Finite ι] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module 𝕜 F] {G : Type u_5} [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] [ContinuousConstSMul 𝕜 F] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {s : Set (G × ((i : ι) → E i))} {x : G × ((i : ι) → E i)} :
ContinuousWithinAt (fun (p : G × ((i : ι) → E i)) => (f p.1) p.2) s x

### Continuity properties of multilinear maps #

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

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

If `f` is a continuous multilinear map 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.

source
theorem MultilinearMap.bound_of_shell_of_norm_map_coord_zero {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : MultilinearMap 𝕜 E G) (hf₀ : ∀ {m : (i : ι) → E i} {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‖

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.

source
theorem MultilinearMap.bound_of_shell_of_continuous {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (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‖

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

source
theorem MultilinearMap.exists_bound_of_continuous {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : MultilinearMap 𝕜 E G) (hf : Continuous ⇑f) :
∃ (C : ℝ), 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

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

source
theorem MultilinearMap.norm_image_sub_le_of_bound' {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [DecidableEq ι] (f : MultilinearMap 𝕜 E G) {C : ℝ} (hC : 0 ≤ C) (H : ∀ (m : (i : ι) → E i), ‖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‖

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

source
theorem MultilinearMap.norm_image_sub_le_of_bound {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : MultilinearMap 𝕜 E G) {C : ℝ} (hC : 0 ≤ C) (H : ∀ (m : (i : ι) → E i), ‖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₂‖

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)`.

source
theorem MultilinearMap.continuous_of_bound {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : MultilinearMap 𝕜 E G) (C : ℝ) (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) :
Continuous ⇑f

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

source
noncomputable def MultilinearMap.mkContinuous {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : MultilinearMap 𝕜 E G) (C : ℝ) (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) :
ContinuousMultilinearMap 𝕜 E G

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

Equations

- f.mkContinuous C H = { toMultilinearMap := f, cont := ⋯ }

Instances For

source
@[simp]
theorem MultilinearMap.coe_mkContinuous {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : MultilinearMap 𝕜 E G) (C : ℝ) (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) :
⇑(f.mkContinuous C H) = ⇑f
source
theorem MultilinearMap.restr_norm_le {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k n : ℕ} (f : MultilinearMap 𝕜 (fun (x : Fin n) => G) G') (s : Finset (Fin n)) (hk : s.card = k) (z : G) {C : ℝ} (H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i : Fin n, ‖m i‖) (v : Fin k → G) :
‖(f.restr s hk z) v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i : Fin k, ‖v i‖

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

### Continuous multilinear maps #

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

source
theorem ContinuousMultilinearMap.bound {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) :
∃ (C : ℝ), 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
source
noncomputable def ContinuousMultilinearMap.opNorm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) :
ℝ

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

Equations

- f.opNorm = sInf {c : ℝ | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}

Instances For

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

- ContinuousMultilinearMap.hasOpNorm = { norm := ContinuousMultilinearMap.opNorm }

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

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

Equations

- ContinuousMultilinearMap.hasOpNorm' = ContinuousMultilinearMap.hasOpNorm

source
theorem ContinuousMultilinearMap.norm_def {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) :
‖f‖ = sInf {c : ℝ | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
source
theorem ContinuousMultilinearMap.bounds_nonempty {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {f : ContinuousMultilinearMap 𝕜 E G} :
∃ (c : ℝ), c ∈ {c : ℝ | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
source
theorem ContinuousMultilinearMap.bounds_bddBelow {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {f : ContinuousMultilinearMap 𝕜 E G} :
BddBelow {c : ℝ | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
source
theorem ContinuousMultilinearMap.isLeast_opNorm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) :
IsLeast {c : ℝ | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖} ‖f‖
source
theorem ContinuousMultilinearMap.opNorm_nonneg {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) :
0 ≤ ‖f‖
source
theorem ContinuousMultilinearMap.le_opNorm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) :
‖f m‖ ≤ ‖f‖ * ∏ i : ι, ‖m i‖

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

source
theorem ContinuousMultilinearMap.le_mul_prod_of_opNorm_le_of_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {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
source
theorem ContinuousMultilinearMap.le_opNorm_mul_prod_of_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) {m : (i : ι) → E i} {b : ι → ℝ} (hm : ∀ (i : ι), ‖m i‖ ≤ b i) :
‖f m‖ ≤ ‖f‖ * ∏ i : ι, b i
source
theorem ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) {m : (i : ι) → E i} {b : ℝ} (hm : ‖m‖ ≤ b) :
‖f m‖ ≤ ‖f‖ * b ^ Fintype.card ι
source
theorem ContinuousMultilinearMap.le_opNorm_mul_pow_of_le {𝕜 : Type u} {G : Type wG} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} {Ei : Fin n → Type u_1} [(i : Fin n) → SeminormedAddCommGroup (Ei i)] [(i : Fin n) → NormedSpace 𝕜 (Ei i)] (f : ContinuousMultilinearMap 𝕜 Ei G) {m : (i : Fin n) → Ei i} {b : ℝ} (hm : ‖m‖ ≤ b) :
‖f m‖ ≤ ‖f‖ * b ^ n
source
theorem ContinuousMultilinearMap.le_of_opNorm_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ} (h : ‖f‖ ≤ C) (m : (i : ι) → E i) :
‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
source
theorem ContinuousMultilinearMap.ratio_le_opNorm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) :
‖f m‖ / ∏ i : ι, ‖m i‖ ≤ ‖f‖
source
theorem ContinuousMultilinearMap.unit_le_opNorm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) {m : (i : ι) → E i} (h : ‖m‖ ≤ 1) :
‖f m‖ ≤ ‖f‖

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

source
theorem ContinuousMultilinearMap.opNorm_le_bound {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {f : ContinuousMultilinearMap 𝕜 E G} {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ M * ∏ i : ι, ‖m i‖) :
‖f‖ ≤ M

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

source
theorem ContinuousMultilinearMap.opNorm_le_iff {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ} (hC : 0 ≤ C) :
‖f‖ ≤ C ↔ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
source
theorem ContinuousMultilinearMap.opNorm_add_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f g : ContinuousMultilinearMap 𝕜 E G) :
‖f + g‖ ≤ ‖f‖ + ‖g‖

The operator norm satisfies the triangle inequality.

source
theorem ContinuousMultilinearMap.opNorm_zero {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] :
‖0‖ = 0
source
theorem ContinuousMultilinearMap.opNorm_smul_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {𝕜' : Type u_1} [NormedField 𝕜'] [NormedSpace 𝕜' G] [SMulCommClass 𝕜 𝕜' G] (c : 𝕜') (f : ContinuousMultilinearMap 𝕜 E G) :
‖c • f‖ ≤ ‖c‖ * ‖f‖
source
def ContinuousMultilinearMap.seminorm (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] :
Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G)

Operator seminorm on the space of continuous multilinear maps, as `Seminorm`.

We use this seminorm to define a `SeminormedAddCommGroup` structure on `ContinuousMultilinearMap 𝕜 E G`, but we have to override the projection `UniformSpace` so that it is definitionally equal to the one coming from the topologies on `E` and `G`.

Equations

- ContinuousMultilinearMap.seminorm 𝕜 E G = Seminorm.ofSMulLE norm ⋯ ⋯ ⋯

Instances For

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

- ContinuousMultilinearMap.instPseudoMetricSpace = (ContinuousMultilinearMap.seminorm 𝕜 E G).toSeminormedAddCommGroup.replaceUniformity ⋯

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

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

Equations

- One or more equations did not get rendered due to their size.

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

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

Equations

- ContinuousMultilinearMap.seminormedAddCommGroup' = ContinuousMultilinearMap.seminormedAddCommGroup

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

- ContinuousMultilinearMap.normedSpace = { toModule := ContinuousMultilinearMap.instModule, norm_smul_le := ⋯ }

source
noncomputable instance ContinuousMultilinearMap.normedSpace' {𝕜 : Type u} {ι : Type v} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] {𝕜' : Type u_1} [NormedField 𝕜'] [NormedSpace 𝕜' G] [SMulCommClass 𝕜 𝕜' G] :
NormedSpace 𝕜' (ContinuousMultilinearMap 𝕜 (fun (x : ι) => G') G)

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

Equations

- ContinuousMultilinearMap.normedSpace' = ContinuousMultilinearMap.normedSpace

source
theorem ContinuousMultilinearMap.le_opNNNorm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i) :
‖f m‖₊ ≤ ‖f‖₊ * ∏ i : ι, ‖m i‖₊

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

source
theorem ContinuousMultilinearMap.le_of_opNNNorm_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) {C : NNReal} (h : ‖f‖₊ ≤ C) (m : (i : ι) → E i) :
‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊
source
theorem ContinuousMultilinearMap.opNNNorm_le_iff {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {f : ContinuousMultilinearMap 𝕜 E G} {C : NNReal} :
‖f‖₊ ≤ C ↔ ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊
source
theorem ContinuousMultilinearMap.isLeast_opNNNorm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) :
IsLeast {C : NNReal | ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊} ‖f‖₊
source
theorem ContinuousMultilinearMap.opNNNorm_prod {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :
‖f.prod g‖₊ = max ‖f‖₊ ‖g‖₊
source
theorem ContinuousMultilinearMap.opNorm_prod {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :
‖f.prod g‖ = max ‖f‖ ‖g‖
source
theorem ContinuousMultilinearMap.opNNNorm_pi {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} [Fintype ι'] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] [(i' : ι') → SeminormedAddCommGroup (E' i')] [(i' : ι') → NormedSpace 𝕜 (E' i')] (f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')) :
‖pi f‖₊ = ‖f‖₊
source
theorem ContinuousMultilinearMap.opNorm_pi {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'} [(i' : ι') → SeminormedAddCommGroup (E' i')] [(i' : ι') → NormedSpace 𝕜 (E' i')] (f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')) :
‖pi f‖ = ‖f‖
source
@[simp]
theorem ContinuousMultilinearMap.norm_ofSubsingleton {𝕜 : Type u} {ι : Type v} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] [Subsingleton ι] (i : ι) (f : G →L[𝕜] G') :
‖(ofSubsingleton 𝕜 G G' i) f‖ = ‖f‖
source
@[simp]
theorem ContinuousMultilinearMap.nnnorm_ofSubsingleton {𝕜 : Type u} {ι : Type v} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] [Subsingleton ι] (i : ι) (f : G →L[𝕜] G') :
‖(ofSubsingleton 𝕜 G G' i) f‖₊ = ‖f‖₊
source
noncomputable def ContinuousMultilinearMap.ofSubsingletonₗᵢ (𝕜 : Type u) {ι : Type v} (G : Type wG) {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] [Subsingleton ι] (i : ι) :
(G →L[𝕜] G') ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) G'

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.ofSubsingletonₗᵢ_apply (𝕜 : Type u) {ι : Type v} (G : Type wG) {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] [Subsingleton ι] (i : ι) (a✝ : G →L[𝕜] G') :
(ofSubsingletonₗᵢ 𝕜 G i) a✝ = (ofSubsingleton 𝕜 G G' i).toFun a✝
source
@[simp]
theorem ContinuousMultilinearMap.ofSubsingletonₗᵢ_symm_apply (𝕜 : Type u) {ι : Type v} (G : Type wG) {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] [Subsingleton ι] (i : ι) (a✝ : ContinuousMultilinearMap 𝕜 (fun (x : ι) => G) G') :
(ofSubsingletonₗᵢ 𝕜 G i).symm a✝ = (ofSubsingleton 𝕜 G G' i).invFun a✝
source
theorem ContinuousMultilinearMap.norm_ofSubsingleton_id_le (𝕜 : Type u) {ι : Type v} (G : Type wG) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [Subsingleton ι] (i : ι) :
‖(ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖ ≤ 1
source
theorem ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le (𝕜 : Type u) {ι : Type v} (G : Type wG) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [Subsingleton ι] (i : ι) :
‖(ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖₊ ≤ 1
source
@[simp]
theorem ContinuousMultilinearMap.norm_constOfIsEmpty (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [IsEmpty ι] (x : G) :
‖constOfIsEmpty 𝕜 E x‖ = ‖x‖
source
@[simp]
theorem ContinuousMultilinearMap.nnnorm_constOfIsEmpty (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [IsEmpty ι] (x : G) :
‖constOfIsEmpty 𝕜 E x‖₊ = ‖x‖₊
source
noncomputable def ContinuousMultilinearMap.prodL (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) (G' : Type wG') [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] :
ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G' ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 E (G × G')

`ContinuousMultilinearMap.prod` as a `LinearIsometryEquiv`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.prodL_symm_apply (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) (G' : Type wG') [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (a✝ : ContinuousMultilinearMap 𝕜 E (G × G')) :
(prodL 𝕜 E G G').symm a✝ = prodEquiv.invFun a✝
source
@[simp]
theorem ContinuousMultilinearMap.prodL_apply (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) (G' : Type wG') [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (a✝ : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G') :
(prodL 𝕜 E G G') a✝ = prodEquiv.toFun a✝
source
noncomputable def ContinuousMultilinearMap.piₗᵢ (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'} [(i' : ι') → NormedAddCommGroup (E' i')] [(i' : ι') → NormedSpace 𝕜 (E' i')] :
((i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')) ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 E ((i : ι') → E' i)

`ContinuousMultilinearMap.pi` as a `LinearIsometryEquiv`.

Equations

- ContinuousMultilinearMap.piₗᵢ 𝕜 E = { toLinearEquiv := ContinuousMultilinearMap.piLinearEquiv, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.piₗᵢ_apply (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'} [(i' : ι') → NormedAddCommGroup (E' i')] [(i' : ι') → NormedSpace 𝕜 (E' i')] (a✝ : (i : ι') → ContinuousMultilinearMap 𝕜 E (E' i)) :
(piₗᵢ 𝕜 E) a✝ = pi a✝
source
@[simp]
theorem ContinuousMultilinearMap.piₗᵢ_symm_apply (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [Fintype ι] {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'} [(i' : ι') → NormedAddCommGroup (E' i')] [(i' : ι') → NormedSpace 𝕜 (E' i')] (a✝ : ContinuousMultilinearMap 𝕜 E ((i : ι') → E' i)) (i : ι') :
(piₗᵢ 𝕜 E).symm a✝ i = (ContinuousLinearMap.proj i).compContinuousMultilinearMap a✝
source
@[simp]
theorem ContinuousMultilinearMap.norm_restrictScalars {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {𝕜' : Type u_1} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' G] [IsScalarTower 𝕜' 𝕜 G] [(i : ι) → NormedSpace 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] (f : ContinuousMultilinearMap 𝕜 E G) :
‖restrictScalars 𝕜' f‖ = ‖f‖
source
noncomputable def ContinuousMultilinearMap.restrictScalarsₗᵢ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (𝕜' : Type u_1) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' G] [IsScalarTower 𝕜' 𝕜 G] [(i : ι) → NormedSpace 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] :
ContinuousMultilinearMap 𝕜 E G →ₗᵢ[𝕜'] ContinuousMultilinearMap 𝕜' E G

`ContinuousMultilinearMap.restrictScalars` as a `LinearIsometry`.

Equations

- ContinuousMultilinearMap.restrictScalarsₗᵢ 𝕜' = { toFun := ContinuousMultilinearMap.restrictScalars 𝕜', map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

Instances For

source
theorem ContinuousMultilinearMap.norm_image_sub_le' {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [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‖

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

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

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

source
theorem MultilinearMap.mkContinuous_norm_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : MultilinearMap 𝕜 E G) {C : ℝ} (hC : 0 ≤ C) (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) :
‖f.mkContinuous C H‖ ≤ C

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.

source
theorem MultilinearMap.mkContinuous_norm_le' {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : MultilinearMap 𝕜 E G) {C : ℝ} (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖) :
‖f.mkContinuous C H‖ ≤ max C 0

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.

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

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

Equations

- f.restr s hk z = (f.restr s hk z).mkContinuous (‖f‖ * ‖z‖ ^ (n - k)) ⋯

Instances For

source
theorem ContinuousMultilinearMap.norm_restr {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k n : ℕ} (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => G) G') (s : Finset (Fin n)) (hk : s.card = k) (z : G) :
‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)
source
@[simp]
theorem ContinuousMultilinearMap.norm_mkPiAlgebra_le {𝕜 : Type u} {ι : Type v} [NontriviallyNormedField 𝕜] [Fintype ι] {A : Type u_1} [NormedCommRing A] [NormedAlgebra 𝕜 A] [Nonempty ι] :
‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ 1
source
theorem ContinuousMultilinearMap.norm_mkPiAlgebra_of_empty {𝕜 : Type u} {ι : Type v} [NontriviallyNormedField 𝕜] [Fintype ι] {A : Type u_1} [NormedCommRing A] [NormedAlgebra 𝕜 A] [IsEmpty ι] :
‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = ‖1‖
source
@[simp]
theorem ContinuousMultilinearMap.norm_mkPiAlgebra {𝕜 : Type u} {ι : Type v} [NontriviallyNormedField 𝕜] [Fintype ι] {A : Type u_1} [NormedCommRing A] [NormedAlgebra 𝕜 A] [NormOneClass A] :
‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1
source
theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin_succ_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {n : ℕ} {A : Type u_1} [SeminormedRing A] [NormedAlgebra 𝕜 A] :
‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1
source
theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos {𝕜 : Type u} [NontriviallyNormedField 𝕜] {n : ℕ} {A : Type u_1} [SeminormedRing A] [NormedAlgebra 𝕜 A] (hn : 0 < n) :
‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ 1
source
theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {A : Type u_1} [SeminormedRing A] [NormedAlgebra 𝕜 A] :
‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖1‖
source
theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {n : ℕ} {A : Type u_1} [SeminormedRing A] [NormedAlgebra 𝕜 A] :
‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ max 1 ‖1‖
source
@[simp]
theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {n : ℕ} {A : Type u_1} [SeminormedRing A] [NormedAlgebra 𝕜 A] [NormOneClass A] :
‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ = 1
source
@[simp]
theorem ContinuousMultilinearMap.nnnorm_smulRight {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊
source
@[simp]
theorem ContinuousMultilinearMap.norm_smulRight {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
‖f.smulRight z‖ = ‖f‖ * ‖z‖
source
@[simp]
theorem ContinuousMultilinearMap.norm_mkPiRing {𝕜 : Type u} {ι : Type v} {G : Type wG} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (z : G) :
‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖
source
noncomputable def ContinuousMultilinearMap.smulRightL (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] :
ContinuousMultilinearMap 𝕜 E 𝕜 →L[𝕜] G →L[𝕜] ContinuousMultilinearMap 𝕜 E G

Continuous bilinear map realizing `(f, z) ↦ f.smulRight z`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.smulRightL_apply {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
((smulRightL 𝕜 E G) f) z = f.smulRight z
source
theorem ContinuousMultilinearMap.norm_smulRightL_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] :
‖smulRightL 𝕜 E G‖ ≤ 1
source
def ContinuousMultilinearMap.piFieldEquiv (𝕜 : Type u) (ι : Type v) (G : Type wG) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] :
G ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) => 𝕜) G

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
noncomputable def MultilinearMap.mkContinuousLinear {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ) (H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖) :
G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'

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

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

Equations

- MultilinearMap.mkContinuousLinear f C H = { toFun := fun (x : G) => (f x).mkContinuous (C * ‖x‖) ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (max C 0) ⋯

Instances For

source
theorem MultilinearMap.mkContinuousLinear_norm_le' {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ) (H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖) :
‖mkContinuousLinear f C H‖ ≤ max C 0
source
theorem MultilinearMap.mkContinuousLinear_norm_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') {C : ℝ} (hC : 0 ≤ C) (H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖) :
‖mkContinuousLinear f C H‖ ≤ C
source
noncomputable def MultilinearMap.mkContinuousMultilinear {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [Fintype ι'] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [(i : ι') → SeminormedAddCommGroup (E' i)] [(i : ι') → NormedSpace 𝕜 (E' i)] (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ) (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖) :
ContinuousMultilinearMap 𝕜 E (ContinuousMultilinearMap 𝕜 E' G)

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

Equations

- f.mkContinuousMultilinear C H = { toFun := fun (m : (i : ι) → E i) => (f m).mkContinuous (C * ∏ i : ι, ‖m i‖) ⋯, map_update_add' := ⋯, map_update_smul' := ⋯ }.mkContinuous (max C 0) ⋯

Instances For

source
@[simp]
theorem MultilinearMap.mkContinuousMultilinear_apply {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [Fintype ι'] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [(i : ι') → SeminormedAddCommGroup (E' i)] [(i : ι') → NormedSpace 𝕜 (E' i)] (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ} (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖) (m : (i : ι) → E i) :
⇑((f.mkContinuousMultilinear C H) m) = ⇑(f m)
source
theorem MultilinearMap.mkContinuousMultilinear_norm_le' {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [Fintype ι'] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [(i : ι') → SeminormedAddCommGroup (E' i)] [(i : ι') → NormedSpace 𝕜 (E' i)] (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ) (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖) :
‖f.mkContinuousMultilinear C H‖ ≤ max C 0
source
theorem MultilinearMap.mkContinuousMultilinear_norm_le {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [Fintype ι'] [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [(i : ι') → SeminormedAddCommGroup (E' i)] [(i : ι') → NormedSpace 𝕜 (E' i)] (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ} (hC : 0 ≤ C) (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖) :
‖f.mkContinuousMultilinear C H‖ ≤ C
source
theorem ContinuousLinearMap.norm_compContinuousMultilinearMap_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (g : G →L[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) :
‖g.compContinuousMultilinearMap f‖ ≤ ‖g‖ * ‖f‖
source
noncomputable def ContinuousLinearMap.compContinuousMultilinearMapL (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) (G' : Type wG') [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] :
(G →L[𝕜] G') →L[𝕜] ContinuousMultilinearMap 𝕜 E G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'

`ContinuousLinearMap.compContinuousMultilinearMap` as a bundled continuous bilinear map.

Equations

- ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G G' = (LinearMap.mk₂ 𝕜 ContinuousLinearMap.compContinuousMultilinearMap ⋯ ⋯ ⋯ ⋯).mkContinuous₂ 1 ⋯

Instances For

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

`ContinuousLinearMap.compContinuousMultilinearMap` as a bundled continuous linear equiv.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm {𝕜 : Type u} {ι : Type v} (E : ι → Type wE) {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (g : G ≃L[𝕜] G') :
(continuousMultilinearMapCongrRight E g).symm = continuousMultilinearMapCongrRight E g.symm
source
@[simp]
theorem ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (g : G ≃L[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) :
(continuousMultilinearMapCongrRight E g) f = (↑g).compContinuousMultilinearMap f
source
noncomputable def ContinuousLinearMap.flipMultilinear {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') :
ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousLinearMap.flipMultilinear_apply_apply {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') (m : (i : ι) → E i) (x : G) :
(f.flipMultilinear m) x = (f x) m
source
noncomputable def ContinuousMultilinearMap.flipLinear {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')) :
G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.flipLinear_apply_apply {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')) (x : G) (m : (i : ι) → E i) :
(f.flipLinear x) m = (f m) x
source
@[simp]
theorem ContinuousLinearMap.flipLinear_flipMultilinear {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') :
f.flipMultilinear.flipLinear = f
source
@[simp]
theorem ContinuousMultilinearMap.flipMultilinear_flipLinear {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')) :
f.flipLinear.flipMultilinear = f
source
noncomputable def ContinuousLinearMap.flipMultilinearEquivₗ (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) (G' : Type wG') [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] :
(G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') ≃ₗ[𝕜] ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')

Flipping arguments gives a linear equivalence between `G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'` and `ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
noncomputable def ContinuousLinearMap.flipMultilinearEquiv (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (G : Type wG) (G' : Type wG') [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] :
(G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') ≃L[𝕜] ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')

Flipping arguments gives a continuous linear equivalence between `G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'` and `ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')`

Equations

- ContinuousLinearMap.flipMultilinearEquiv 𝕜 E G G' = (ContinuousLinearMap.flipMultilinearEquivₗ 𝕜 E G G').toContinuousLinearEquivOfBounds 1 1 ⋯ ⋯

Instances For

source
@[simp]
theorem ContinuousLinearMap.coe_flipMultilinearEquiv {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] :
⇑(flipMultilinearEquiv 𝕜 E G G') = flipMultilinear
source
@[simp]
theorem ContinuousLinearMap.coe_symm_flipMultilinearEquiv {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] :
⇑(flipMultilinearEquiv 𝕜 E G G').symm = ContinuousMultilinearMap.flipLinear
source
theorem LinearIsometry.norm_compContinuousMultilinearMap {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] [Fintype ι] (g : G →ₗᵢ[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) :
‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖
source
theorem ContinuousMultilinearMap.norm_compContinuousLinearMap_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i →L[𝕜] E₁ i) :
‖g.compContinuousLinearMap f‖ ≤ ‖g‖ * ∏ i : ι, ‖f i‖
source
theorem ContinuousMultilinearMap.norm_compContinuous_linearIsometry_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i) :
‖g.compContinuousLinearMap fun (i : ι) => (f i).toContinuousLinearMap‖ ≤ ‖g‖
source
theorem ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i) :
‖g.compContinuousLinearMap fun (i : ι) => ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }‖ = ‖g‖
source
noncomputable def ContinuousMultilinearMap.compContinuousLinearMapL {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : (i : ι) → E i →L[𝕜] E₁ i) :
ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G

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

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

For a version fixing `g` and varying `f`, see `compContinuousLinearMapLRight`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.compContinuousLinearMapL_apply {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i →L[𝕜] E₁ i) :
(compContinuousLinearMapL f) g = g.compContinuousLinearMap f
source
theorem ContinuousMultilinearMap.norm_compContinuousLinearMapL_le {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} (G : Type wG) [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : (i : ι) → E i →L[𝕜] E₁ i) :
‖compContinuousLinearMapL f‖ ≤ ∏ i : ι, ‖f i‖
source
noncomputable def ContinuousMultilinearMap.compContinuousLinearMapLRight {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : ContinuousMultilinearMap 𝕜 E₁ G) :
ContinuousMultilinearMap 𝕜 (fun (i : ι) => E i →L[𝕜] E₁ i) (ContinuousMultilinearMap 𝕜 E G)

`ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear map. This implementation fixes `g : ContinuousMultilinearMap 𝕜 E₁ G`.

Actually, the map is linear in `g`, see `ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear`.

For a version fixing `f` and varying `g`, see `compContinuousLinearMapL`.

Equations

- g.compContinuousLinearMapLRight = { toFun := fun (f : (i : ι) → E i →L[𝕜] E₁ i) => g.compContinuousLinearMap f, map_update_add' := ⋯, map_update_smul' := ⋯ }.mkContinuous ‖g‖ ⋯

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.compContinuousLinearMapLRight_apply {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i →L[𝕜] E₁ i) :
g.compContinuousLinearMapLRight f = g.compContinuousLinearMap f
source
theorem ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le {𝕜 : Type u} {ι : Type v} (E : ι → Type wE) {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : ContinuousMultilinearMap 𝕜 E₁ G) :
‖g.compContinuousLinearMapLRight‖ ≤ ‖g‖
source
noncomputable def ContinuousMultilinearMap.compContinuousLinearMapMultilinear (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (E₁ : ι → Type wE₁) (G : Type wG) [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] :
MultilinearMap 𝕜 (fun (i : ι) => E i →L[𝕜] E₁ i) (ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)

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

Equations

- ContinuousMultilinearMap.compContinuousLinearMapMultilinear 𝕜 E E₁ G = { toFun := ContinuousMultilinearMap.compContinuousLinearMapL, map_update_add' := ⋯, map_update_smul' := ⋯ }

Instances For

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

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

Equations

- ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 E E₁ G = (ContinuousMultilinearMap.compContinuousLinearMapMultilinear 𝕜 E E₁ G).mkContinuous 1 ⋯

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear_apply_apply (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) (E₁ : ι → Type wE₁) (G : Type wG) [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : (i : ι) → E i →L[𝕜] E₁ i) (g : ContinuousMultilinearMap 𝕜 E₁ G) :
((compContinuousLinearMapContinuousMultilinear 𝕜 E E₁ G) f) g = g.compContinuousLinearMap f
source
noncomputable def ContinuousMultilinearMap.fderivCompContinuousLinearMap {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap 𝕜 E₁ G) (g : (i : ι) → E i →L[𝕜] E₁ i) :
((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E G

Fréchet derivative of `compContinuousLinearMap f g` with respect to `g`. The derivative with respect to `f` is given by `compContinuousLinearMapL`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] [DecidableEq ι] (f : ContinuousMultilinearMap 𝕜 E₁ G) (g dg : (i : ι) → E i →L[𝕜] E₁ i) (v : (i : ι) → E i) :
((f.fderivCompContinuousLinearMap g) dg) v = ∑ i : ι, f fun (j : ι) => (Function.update g i (dg i) j) (v j)
source
noncomputable def ContinuousLinearEquiv.continuousMultilinearMapCongrLeft {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} (G : Type wG) [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : (i : ι) → E i ≃L[𝕜] E₁ i) :
ContinuousMultilinearMap 𝕜 E₁ G ≃L[𝕜] ContinuousMultilinearMap 𝕜 E G

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} (G : Type wG) [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : (i : ι) → E i ≃L[𝕜] E₁ i) :
(continuousMultilinearMapCongrLeft G f).symm = continuousMultilinearMapCongrLeft G fun (i : ι) => (f i).symm
source
@[simp]
theorem ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i ≃L[𝕜] E₁ i) :
(continuousMultilinearMapCongrLeft G f) g = g.compContinuousLinearMap fun (i : ι) => ↑(f i)
source
noncomputable def ContinuousMultilinearMap.iteratedFDerivComponent {𝕜 : Type u} {ι : Type v} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {α : Type u_1} [Fintype α] (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ ↑s) [DecidablePred fun (x : ι) => x ∈ s] :
ContinuousMultilinearMap 𝕜 (fun (i : { a : ι // a ∉ s }) => E₁ ↑i) (ContinuousMultilinearMap 𝕜 (fun (x : α) => (i : ι) → E₁ i) G)

One of the components of the iterated derivative of a continuous multilinear map. Given a bijection `e` between a type `α` (typically `Fin k`) and a subset `s` of `ι`, this component is a continuous multilinear map of `k` vectors `v₁, ..., vₖ`, mapping them to `f (x₁, (v_{e.symm 2})₂, x₃, ...)`, where at indices `i` in `s` one uses the `i`-th coordinate of the vector `v_{e.symm i}` and otherwise one uses the `i`-th coordinate of a reference vector `x`. This is continuous multilinear in the components of `x` outside of `s`, and in the `v_j`.

Equations

- f.iteratedFDerivComponent e = (f.iteratedFDerivComponent e).mkContinuousMultilinear ‖f‖ ⋯

Instances For

source
@[simp]
theorem ContinuousMultilinearMap.iteratedFDerivComponent_apply {𝕜 : Type u} {ι : Type v} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {α : Type u_1} [Fintype α] (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ ↑s) [DecidablePred fun (x : ι) => x ∈ 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⟩
source
theorem ContinuousMultilinearMap.norm_iteratedFDerivComponent_le {𝕜 : Type u} {ι : Type v} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {α : Type u_1} [Fintype α] (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ ↑s) [DecidablePred fun (x : ι) => x ∈ s] (x : (i : ι) → E₁ i) :
‖(f.iteratedFDerivComponent e) fun (x_1 : { a : ι // a ∉ s }) => x ↑x_1‖ ≤ ‖f‖ * ‖x‖ ^ (Fintype.card ι - Fintype.card α)
source
def ContinuousMultilinearMap.iteratedFDeriv {𝕜 : Type u} {ι : Type v} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E₁ G) (k : ℕ) (x : (i : ι) → E₁ i) :
ContinuousMultilinearMap 𝕜 (fun (x : Fin k) => (i : ι) → E₁ i) G

The `k`-th iterated derivative of a continuous multilinear map `f` at the point `x`. It is a continuous multilinear map of `k` vectors `v₁, ..., vₖ` (with the same type as `x`), mapping them to `∑ f (x₁, (v_{i₁})₂, x₃, ...)`, where at each index `j` one uses either `xⱼ` or one of the `(vᵢ)ⱼ`, and each `vᵢ` has to be used exactly once. The sum is parameterized by the embeddings of `Fin k` in the index type `ι` (or, equivalently, by the subsets `s` of `ι` of cardinality `k` and then the bijections between `Fin k` and `s`).

The fact that this is indeed the iterated Fréchet derivative is proved in `ContinuousMultilinearMap.iteratedFDeriv_eq`.

Equations

- f.iteratedFDeriv k x = ∑ e : Fin k ↪ ι, (f.iteratedFDerivComponent e.toEquivRange) ((Pi.compRightL 𝕜 E₁ Subtype.val) x)

Instances For

source
theorem ContinuousMultilinearMap.norm_iteratedFDeriv_le' {𝕜 : Type u} {ι : Type v} {E₁ : ι → Type wE₁} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E₁ i)] [(i : ι) → NormedSpace 𝕜 (E₁ i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E₁ G) (k : ℕ) (x : (i : ι) → E₁ i) :
‖f.iteratedFDeriv k x‖ ≤ ↑((Fintype.card ι).descFactorial k) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

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

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

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

A continuous linear map is zero iff its norm vanishes.

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

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

Equations

- ContinuousMultilinearMap.normedAddCommGroup = NormedAddCommGroup.ofSeparation ⋯

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

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

Equations

- ContinuousMultilinearMap.normedAddCommGroup' = ContinuousMultilinearMap.normedAddCommGroup

source
theorem ContinuousMultilinearMap.norm_ofSubsingleton_id (𝕜 : Type u) {ι : Type v} (G : Type wG) [Fintype ι] [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [Subsingleton ι] [Nontrivial G] (i : ι) :
‖(ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖ = 1
source
theorem ContinuousMultilinearMap.nnnorm_ofSubsingleton_id (𝕜 : Type u) {ι : Type v} (G : Type wG) [Fintype ι] [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [Subsingleton ι] [Nontrivial G] (i : ι) :
‖(ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖₊ = 1

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

source
theorem MultilinearMap.bound_of_shell {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [Fintype ι] [NontriviallyNormedField 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {ε : ι → ℝ} {C : ℝ} {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‖

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