ContinuousMultilinearMap.le_op_nnnorm
theorem ContinuousMultilinearMap.le_op_nnnorm :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G)
(m : (i : ι) → E i), ‖f m‖₊ ≤ ‖f‖₊ * Finset.univ.prod fun i => ‖m i‖₊
The theorem `ContinuousMultilinearMap.le_op_nnnorm` asserts that for a given continuous multilinear map `f`, from a vector space `E` indexed by `ι` to a vector space `G`, both over a nontrivially normed field `𝕜`, and for a given function `m` that assigns to each `i in ι` an element of `E i`, the nonnegative norm of `f m`, denoted as `‖f m‖₊`, is bounded by the nonnegative norm of `f`, denoted as `‖f‖₊`, times the product of the nonnegative norms of `m i` for each `i` in the universal finite set of type `Finset ι`. The universal finite set of type `Finset ι` is implied from the assumption `Fintype ι`. This is a fundamental property of the operator norm of a continuous multilinear map in the nonnegative norm version.
More concisely: Given a continuous multilinear map from a finite-type vector space to a normed field, the operator norm is greater than or equal to the product of the map's norm and the product of the norms of its arguments.
|
MultilinearMap.norm_map_coord_zero
theorem MultilinearMap.norm_map_coord_zero :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
[inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G),
Continuous ⇑f → ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
The theorem, `MultilinearMap.norm_map_coord_zero`, states that for a continuous multilinear map `f` in a finitely many variables domain `E` and an element `m` from the product of `E i`, if any of the `m i` has a norm of `0`, then the norm of `f m` would also be `0`. The continuity assumption for `f` is required, because without it, there can be cases where the domain has zero norm but the codomain does not, which would not satisfy the condition.
More concisely: If `f` is a continuous multilinear map from a finite-dimensional vector space `E` to a normed vector space, and `m` is an element of the product of `E` with i-th component having norm 0, then the norm of `f` applied to `m` is 0.
|
ContinuousMultilinearMap.op_norm_add_le
theorem ContinuousMultilinearMap.op_norm_add_le :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f g : ContinuousMultilinearMap 𝕜 E G),
‖f + g‖ ≤ ‖f‖ + ‖g‖
This theorem, known as "ContinuousMultilinearMap.op_norm_add_le" or the triangle inequality for operator norms, states that for any field `𝕜`, index type `ι`, types `E` and `G` where `E` depends on `ι`, given that `ι` is finite, `𝕜` is a normed field, `E i` and `G` are seminormed commutative additive groups, and `E i` and `G` are normed spaces over `𝕜`, the operator norm of the sum of two continuous multilinear maps `f` and `g` from `𝕜` and `E` to `G` is less than or equal to the sum of the operator norms of `f` and `g`. In mathematical terms, ‖f + g‖ ≤ ‖f‖ + ‖g‖.
More concisely: Given a finite index type `ι`, a normed field `𝕜`, and continuous multilinear maps `f` and `g` from `𝕜` to a normed space `G` over `𝕜`, where `E ι` is a seminormed commutative additive group and a normed space over `𝕜`, the operator norm of `f + g` is less than or equal to the sum of the operator norms of `f` and `g`, that is, ‖`f + g`‖ ≤ ‖`f`‖ + ‖`g`‖.
|
MultilinearMap.mkContinuous_norm_le'
theorem MultilinearMap.mkContinuous_norm_le' :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {C : ℝ}
(H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖), ‖f.mkContinuous C H‖ ≤ max C 0
The theorem `MultilinearMap.mkContinuous_norm_le'` states that for any multilinear map `f`, defined on a nontrivially normed field `𝕜` and seminormed add commutative groups `E i` for each `i` in a finite type `ι`, with values in a seminormed add commutative group `G`, if it is made continuous using the constructor `mkContinuous` with a nonnegative bound `C`, then the norm of the resulting continuous multilinear map is bounded by `max(C, 0)`. Here, the constructor `mkContinuous` generates a continuous multilinear map from `f` such that for any `m` in the cartesian product of `E i` over `ι`, the norm of `f(m)` is less than or equal to `C` times the product of norms of `m i` over all `i` in the universal set of `ι`.
More concisely: For any multilinear map `f` from a product of seminormed add commutative groups `E i` over a finite type `ι`, defined on a nontrivially normed field `𝕜`, if `f` is made continuous using the constructor `mkContinuous` with a nonnegative bound `C`, then the norm of the resulting continuous multilinear map is bounded by `max(C, 0)`.
|
MultilinearMap.norm_image_sub_le_of_bound'
theorem MultilinearMap.norm_image_sub_le_of_bound' :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) [inst_6 : DecidableEq ι]
{C : ℝ},
0 ≤ C →
(∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖) →
∀ (m₁ m₂ : (i : ι) → E i),
‖f m₁ - f m₂‖ ≤
C *
Finset.univ.sum fun i => Finset.univ.prod fun j => if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
This theorem, `MultilinearMap.norm_image_sub_le_of_bound'`, establishes a bound on the difference of the images under a multilinear map `f` at two different points `m₁` and `m₂`. The theorem is defined over a nontrivially normed field `𝕜`, a set `ι` of indices, and seminormed additive commutative group spaces `E` and `G`. The theorem assumes that `f` satisfies a boundedness condition, specifically that its norm at any point `m` is at most `C` times the product of the norms of `m`'s components. Given these conditions, the theorem asserts that the norm of the image of `f` at `m₁` subtracted from its image at `m₂` is bounded by a quantity involving `C`, the difference of the norms of the components of `m₁` and `m₂`, and the maximum norm of the components of `m₁` and `m₂`. The theorem applies to all possible selections of `m₁` and `m₂`.
More concisely: For a multilinear map `f` over a nontrivially normed field with bounded norm condition, the norm of `f(m₁) - f(m₂)` is bounded by `C` times the maximum of the difference of the norms of `m₁` and `m₂`, and the maximum norm of `m₁` and `m₂`.
|
ContinuousMultilinearMap.norm_image_sub_le
theorem ContinuousMultilinearMap.norm_image_sub_le :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (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 theorem `ContinuousMultilinearMap.norm_image_sub_le` states that for any multilinear map `f`, the norm of the difference `f m₁ - f m₂` is bounded by the expression `‖f‖ * card ι * ‖m₁ - m₂‖ * (max ‖m₁‖ ‖m₂‖) ^ (card ι - 1)`. This equation implies that the magnitude of the difference between the image of `m₁` and the image of `m₂` under `f` is controlled by the norm of `f`, the number of elements in `ι`, the norm of the difference between `m₁` and `m₂`, and the maximum norm of `m₁` and `m₂` raised to the power of the number of elements in `ι` minus one. Here, `ι` represents a finite set of indices, `𝕜` is a nontrivial normed field, `E` is a seminormed group indexed by `ι`, `G` is another seminormed group, and `f` is a continuous multilinear map from `E` to `G`.
More concisely: The norm of the difference between the images of two arguments under a continuous multilinear map is bounded by the product of the map's norm, the cardinality of the domain's index set, and the maximum of the arguments' norms raised to the power of the cardinality minus one.
|
ContinuousMultilinearMap.le_mul_prod_of_le_opNorm_of_le
theorem ContinuousMultilinearMap.le_mul_prod_of_le_opNorm_of_le :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ContinuousMultilinearMap 𝕜 E G}
{m : (i : ι) → E i} {C : ℝ} {b : ι → ℝ},
‖f‖ ≤ C → (∀ (i : ι), ‖m i‖ ≤ b i) → ‖f m‖ ≤ C * Finset.univ.prod fun i => b i
The theorem `ContinuousMultilinearMap.le_mul_prod_of_le_opNorm_of_le` states that for all types 𝕜, ι, E, and G, with 𝕜 being a nontrivially normed field, E and G being normed spaces over 𝕜, where E is indexed over ι (which is a finite type), and G being a seminormed add commutative group, if we have a continuous multilinear map `f` from E to G, a function `m` mapping every index in ι to E, a real number `C`, and a function `b` mapping every index in ι to a real number, such that the norm of `f` is less than or equal to `C`, and for every index in ι, the norm of `m` at that index is less than or equal to `b` at that index, then the norm of `f` at `m` will be less than or equal to `C` times the product of `b` at every index in the universal finite set of type `Finset ι`. This theorem essentially establishes an upper bound for the norm of a continuous multilinear map applied to a family of vectors.
More concisely: For a continuous multilinear map from a finite-indexed normed space to a seminormed add commutative group, with input vectors bounded by real numbers, the norm of the map's application to the vectors is bounded by the product of the input bounds and the map's operator norm.
|
ContinuousMultilinearMap.unit_le_op_norm
theorem ContinuousMultilinearMap.unit_le_op_norm :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G)
(m : (i : ι) → E i), ‖m‖ ≤ 1 → ‖f m‖ ≤ ‖f‖
This theorem, known as `ContinuousMultilinearMap.unit_le_op_norm` or sometimes as the "Alias" of `ContinuousMultilinearMap.unit_le_opNorm`, states that for any type `𝕜` representing a nontrivially normed field, any finite type `ι`, any types `E` and `G` representing seminormed additive commutative groups where each element `i` of `ι` can map to an element of `E` or `G`, and any continuous multilinear map `f` from `𝕜` to `E` and `G`, if the norm of a map `m` (from `ι` to `E`) is less than or equal to 1, then the norm of `f(m)` is less than or equal to the norm of `f`. In simpler terms, the image of the unit ball under a continuous multilinear map is bounded.
More concisely: For any nontrivially normed field 𝕜, seminormed additive commutative groups E and G, and continuous multilinear map f from 𝕜 to E and G, if the norm of a map m from the finite index set to E or G is less than or equal to 1, then the norm of f(m) is less than or equal to the norm of f.
|
ContinuousMultilinearMap.le_opNorm
theorem ContinuousMultilinearMap.le_opNorm :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G)
(m : (i : ι) → E i), ‖f m‖ ≤ ‖f‖ * Finset.univ.prod fun i => ‖m i‖
This theorem states the fundamental property of the operator norm of a continuous multilinear map. Specifically, for any continuous multilinear map `f` from a normed field `𝕜` to a space `E` indexed by a finite type `ι`, and for a given mapping `m` from `ι` to `E`, the norm of `f(m)` is bounded by the product of the norm of `f` and the product of the norms of `m i` for every `i` in the universal set of `ι`. In mathematical notation, this is expressed as `‖f m‖ ≤ ‖f‖ * ∏ i ∈ ι, ‖m i‖`.
More concisely: The norm of a continuous multilinear map applied to a vector valued function is bounded by the product of the map's norm and the product of the norms of the function values.
|
MultilinearMap.norm_image_sub_le_of_bound
theorem MultilinearMap.norm_image_sub_le_of_bound :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {C : ℝ},
0 ≤ C →
(∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖) →
∀ (m₁ m₂ : (i : ι) → E i),
‖f m₁ - f m₂‖ ≤ C * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖
This theorem, named `MultilinearMap.norm_image_sub_le_of_bound`, makes a statement about a bound on the difference of the images of two elements under a multilinear map `f`. Specifically, if `f` satisfies a particular boundedness property around `0`, which in this case is that the norm of `f(m)` is less than or equal to `C` times the product of the norms of `m`'s components for any `m`, then the norm of the difference `f(m₁) - f(m₂)` can be bounded by a certain expression involving `C`, the cardinality of the index set `ι`, the maximum norm of `m₁` and `m₂`, and the norm of the difference `m₁ - m₂`. This bound is given by `C * card ι * ‖m₁ - m₂‖ * (max ‖m₁‖ ‖m₂‖) ^ (card ι - 1)`. This theorem provides a less precise but more usable version of the bound, compared to `norm_image_sub_le_of_bound'`.
More concisely: Given a multilinear map `f` with component-wise bounded norm at `0` (satisfying `∀ i, ‖f (a i)‖ ≤ C ∏ i (‖ai‖)` for all `i` in the index set `ι` and `a i` in the domain), the difference of images of any two elements `m₁` and `m₂` can be bounded by `C * card ι * ‖m₁ - m₂‖ * (max ‖m₁‖ ‖m₂‖) ^ (card ι - 1)`.
|
ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le
theorem ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G)
{m : (i : ι) → E i} {b : ℝ}, ‖m‖ ≤ b → ‖f m‖ ≤ ‖f‖ * b ^ Fintype.card ι
The theorem `ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le` states that for a given continuous multilinear map `f` from a nontrivially normed field `𝕜` to a normed space `G`, and a tuple `m` from a finitely indexed family of seminormed additive commutative groups `E`, if the norm of `m` is less than or equal to a real number `b`, then the norm of the image of `m` under `f` is less than or equal to the operator norm of `f` times `b` raised to the power of the cardinality (the number of elements) of the index set `ι`. The norm, operator norm, and cardinality are all defined in the usual way for their respective mathematical objects.
More concisely: For a continuous multilinear map from a nontrivially normed field to a normed space and a tuple from a finitely indexed family of seminormed additive commutative groups with norm less than or equal to a real number, the image norm is less than or equal to the operator norm times the number raising to the power of the cardinality of the index set.
|
ContinuousMultilinearMap.continuous_eval
theorem ContinuousMultilinearMap.continuous_eval :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst : NontriviallyNormedField 𝕜]
[inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G], Continuous fun p => p.1 p.2
The theorem `ContinuousMultilinearMap.continuous_eval` states that for any given field `𝕜` with a nontrivial norm, any finite type `ι`, any seminormed additive commutative groups `E i` and `G` where `i` belongs to `ι` and `E i` and `G` are normed spaces over `𝕜`, the application of a multilinear map to a vector is a continuous function. In other words, if you have a multilinear map and a vector, changing the map or the vector slightly will only change the result of the map slightly.
More concisely: Given a multilinear map and vectors from normed spaces over a nontrivial field, the map application is a continuous function.
|
MultilinearMap.mkContinuous_norm_le
theorem MultilinearMap.mkContinuous_norm_le :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {C : ℝ},
0 ≤ C → ∀ (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖), ‖f.mkContinuous C H‖ ≤ C
This theorem states that if a continuous multilinear map is created from a multilinear map using the `mkContinuous` constructor, then the norm of this map is bounded by the bound provided to the constructor, provided that this bound is nonnegative. More precisely, for every mapping `f` from the multilinear map and every nonnegative real number `C`, if for all `m` such that `m` is a function from `ι` to `E i` and the norm of `f m` is less than or equal to `C` times the product of the norms of `m i` for all `i` in the universal finite set of type `Finset ι`, then the norm of `f.mkContinuous C H` is less than or equal to `C`.
More concisely: If a multilinear map is continuous and its norm is bounded by a given constant with respect to the product of the norms of its arguments, then the norm of the continuous multilinear map is also bounded by that constant.
|
ContinuousMultilinearMap.op_norm_zero_iff
theorem ContinuousMultilinearMap.op_norm_zero_iff :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G),
‖f‖ = 0 ↔ f = 0
This theorem, named `ContinuousMultilinearMap.op_norm_zero_iff`, establishes an equivalence for any continuous multilinear map `f` from a type `E` to a type `G` over a nontrivially normed field `𝕜`. Specifically, it states that the norm of `f` equals zero if and only if `f` is the zero map. This theorem is useful in functional analysis, particularly in the study of normed vector spaces, where the norm of a map provides a measure of its 'size' or 'magnitude'.
More concisely: For any continuous multilinear map `f` from a normed vector space `E` to a normed vector space `G` over a nontrivially normed field, `f` has norm zero if and only if `f` is the zero map.
|
ContinuousMultilinearMap.norm_image_sub_le'
theorem ContinuousMultilinearMap.norm_image_sub_le' :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G)
[inst_6 : DecidableEq ι] (m₁ m₂ : (i : ι) → E i),
‖f m₁ - f m₂‖ ≤
‖f‖ * Finset.univ.sum fun i => Finset.univ.prod fun j => if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
This theorem states that for any continuous multilinear map `f`, the difference `f m₁ - f m₂` is bounded by the product of the operator norm of `f` and the sum over all `i` of the product over all `j` of the difference `‖m₁ i - m₂ i‖` for `j = i` and the maximum of `‖m₁ j‖` and `‖m₂ j‖` for `j ≠ i`. To be explicit, the bound is given by `‖f‖ * ∑i (∏j (if j = i then ‖m₁ i - m₂ i‖ else max(‖m₁ j‖, ‖m₂ j‖)))`.
This theorem provides a precise control on the change of values of a continuous multilinear map with respect to its arguments, given a change in the input. The change is measured in terms of the operator norm of the multilinear map and the difference of the arguments.
More concisely: For any continuous multilinear map `f` and matrices `m₁` and `m₂`, the norm of `f(m₁) - f(m₂)` is bounded by the product of the operator norm of `f` and the sum over all `i`, of the maximum over all `j ≠ i` of the maximum of the norms of `m₁ j` and `m₂ j`, multiplied by the norm of the `i`-th difference between `m₁` and `m₂`.
|
MultilinearMap.exists_bound_of_continuous
theorem MultilinearMap.exists_bound_of_continuous :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G),
Continuous ⇑f → ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖
The theorem `MultilinearMap.exists_bound_of_continuous` states that if we have a multilinear map `f` that operates on finitely many variables in normed spaces and is continuous, then there exists a positive constant `C` such that the norm of `f m` is less than or equal to `C` multiplied by the product of the norms of `m i` for all `i` in the universal finite set of the domain's index type. In other words, the theorem guarantees the existence of a bound on the norm of the multilinear map's output in terms of the input norms, under the condition of continuity.
More concisely: If `f` is a continuous multilinear map from the product of finite normed spaces into a normed space, then there exists a constant `C` such that `||f (m_1, ..., m_n)|| ≤ C · ∏₋ₙ ||m_i||` for all `m_i` in the respective normed spaces.
|
ContinuousMultilinearMap.opNorm_le_bound
theorem ContinuousMultilinearMap.opNorm_le_bound :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {M : ℝ},
0 ≤ M → (∀ (m : (i : ι) → E i), ‖f m‖ ≤ M * Finset.univ.prod fun i => ‖m i‖) → ‖f‖ ≤ M
This theorem states that in a nontrivially normed field with a continuous multilinear map, if the upper bound of the norm of every instance of the map is controlled (i.e., it is less than or equal to some non-negative real number `M` multiplied by the product of the norms of the elements in the finite universal set), then the norm of the map itself is also controlled and is less than or equal to `M`. In other words, if each individual component of a multilinear operation is bounded, then the operation as a whole is also bounded.
More concisely: In a nontrivially normed field, if every instance of a continuous multilinear map has norm bounded by `M` times the product of the norms of its arguments, then the norm of the map is also bounded by `M`.
|
ContinuousMultilinearMap.op_norm_le_bound
theorem ContinuousMultilinearMap.op_norm_le_bound :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) {M : ℝ},
0 ≤ M → (∀ (m : (i : ι) → E i), ‖f m‖ ≤ M * Finset.univ.prod fun i => ‖m i‖) → ‖f‖ ≤ M
This theorem, known as an alias of `ContinuousMultilinearMap.opNorm_le_bound`, asserts the following: for any type `𝕜`, index set `ι`, function types `E` and `G` with `Fintype ι`, `NontriviallyNormedField 𝕜`, `SeminormedAddCommGroup` for each `E i`, `NormedSpace 𝕜` for each `E i` and `G`, and any continuous multilinear map `f` from `𝕜` to `E` to `G`, if we have a non-negative real number `M` such that the norm of `f m` is less than or equal to `M` times the product of the norms of `m i` over all `i` in the universal finite set of `ι`, then the norm of `f` is less than or equal to `M`. This theorem provides a bound on the operator norm of a continuous multilinear map in terms of the norms of its inputs and a scalar multiplier.
More concisely: Given a continuous multilinear map between normed spaces, if the norm of the map on any input is bounded by the product of the input norms and a scalar, then the operator norm of the map is also bounded by that scalar.
|
MultilinearMap.continuous_of_bound
theorem MultilinearMap.continuous_of_bound :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) (C : ℝ),
(∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖) → Continuous ⇑f
The theorem `MultilinearMap.continuous_of_bound` in Lean 4 states that for any multilinear map `f`, from a finite set of vectors, each from a different seminormed addition group under a nontrivially normed field into a seminormed addition group, if there exists a real number `C` such that the norm of `f(m)` is bounded by `C` times the product of the norms of elements of `m` over all vectors `m`, then `f` is continuous. Essentially, this theorem connects the boundedness of a multilinear map with its continuity in the context of normed spaces.
More concisely: A multilinear map between finite sets of vectors in normed fields is continuous if and only if it is bounded by the product of the norms of its arguments.
|
MultilinearMap.bound_of_shell_of_continuous
theorem MultilinearMap.bound_of_shell_of_continuous :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G),
Continuous ⇑f →
∀ {ε : ι → ℝ} {C : ℝ},
(∀ (i : ι), 0 < ε i) →
∀ {c : ι → 𝕜},
(∀ (i : ι), 1 < ‖c i‖) →
(∀ (m : (i : ι) → E i),
(∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
(∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖) →
∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖
The theorem states that given a continuous multilinear map `f` on normed spaces, if it satisfies an inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖` on a shell defined by `ε i / ‖c i‖ < ‖m i‖ < ε i` for some positive numbers `ε i` and elements `c i` of type `𝕜`, with `1 < ‖c i‖`, then this inequality is also satisfied for all `m`. Here, `𝕜` is a non-trivially normed field, `ι` is a finite type, `E` is a function from `ι` to seminormed add commutative groups that are also normed spaces over `𝕜`, and `G` is a seminormed add commutative group that's a normed space over `𝕜`. The shell is a region in the space of the `E i` where the norm of each `m i` is bounded below by `ε i / ‖c i‖` and above by `ε i`. The product `∏ i, ‖m i‖` is taken over all elements of the finite set `Finset.univ`, which includes all possible elements of type `ι`.
More concisely: Given a continuous multilinear map `f` on normed spaces `E i` over a non-trivially normed field `𝕜`, if `‖f m‖` satisfies the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖` for all `m` in the shell defined by `ε i / ‖c i‖ < ‖m i‖ < ε i`, then this inequality holds for all `m` in the product space `G^ι`.
|
ContinuousMultilinearMap.le_op_norm
theorem ContinuousMultilinearMap.le_op_norm :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G)
(m : (i : ι) → E i), ‖f m‖ ≤ ‖f‖ * Finset.univ.prod fun i => ‖m i‖
The theorem `ContinuousMultilinearMap.le_op_norm` states a fundamental property of the operator norm of a continuous multilinear map: the norm of a multilinear map `f` applied to a collection `m` is bounded by the norm of `f` times the product of the norms of each element in `m`. More formally, for any non-trivially normed field `𝕜`, any finite index set `ι`, any seminormed add commutative group `E` indexed by `ι`, and any seminormed add commutative group `G`, if `f` is a continuous multilinear map from `E` to `G`, and `m` is a function from `ι` to `E`, then the norm of `f` applied to `m`, denoted by `‖f m‖`, is less than or equal to the product of the norm of `f` and the product of the norms of `m i` for each `i` in the finite set `Finset.univ`.
More concisely: For any continuous multilinear map f from a seminormed add commutative group E to another seminormed add commutative group G, and any function m from a finite index set to E, the operator norm of f applied to m is less than or equal to the product of the norm of f and the product of the norms of m(i) for all i in the index set.
|
ContinuousMultilinearMap.opNorm_nonneg
theorem ContinuousMultilinearMap.opNorm_nonneg :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G), 0 ≤ ‖f‖
This theorem states that for any continuous multilinear map `f` from a nontrivially normed field `𝕜` and semi-normed additive commutative group `E i` to another semi-normed additive commutative group `G` with `E i` and `G` being normed spaces over `𝕜`, the operator norm of `f` is always nonnegative, i.e., `0 ≤ ‖f‖`. This is a property of norms in general, which are always nonnegative.
More concisely: For any continuous multilinear map from a nontrivially normed field into two semi-normed additive commutative groups, where these spaces are normed over the field, the operator norm is nonnegative.
|
ContinuousMultilinearMap.norm_ofSubsingleton
theorem ContinuousMultilinearMap.norm_ofSubsingleton :
∀ {𝕜 : Type u} {ι : Type v} {G : Type wG} {G' : Type wG'} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : SeminormedAddCommGroup G] [inst_3 : NormedSpace 𝕜 G] [inst_4 : SeminormedAddCommGroup G']
[inst_5 : NormedSpace 𝕜 G'] [inst_6 : Subsingleton ι] (i : ι) (f : G →L[𝕜] G'),
‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G' i) f‖ = ‖f‖
This theorem states that for a continuous multilinear map specifically defined over a subsingleton set, the norm of that map equals the norm of the input function. Here, the set ι is a subsingleton (i.e., it contains at most one element), 𝕜 is a nontrivially normed field, G and G' are semi-normed additive commutative groups with 𝕜 as their scalar field. The function `f` is a bounded linear map from G to G', and `i` is an element of ι. The theorem applies to the special case where a continuous multilinear map is created from a bounded linear map with respect to a subsingleton set, asserting that the norm of such a multilinear map is the same as the norm of the original linear map.
More concisely: The norm of a continuous, multilinear map defined over a subsingleton set from a nontrivially normed field to a semi-normed additive commutative group, derived from a bounded linear map, equals the norm of the original linear map.
|
MultilinearMap.restr_norm_le
theorem MultilinearMap.restr_norm_le :
∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup G]
[inst_2 : NormedSpace 𝕜 G] [inst_3 : SeminormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] {k n : ℕ}
(f : MultilinearMap 𝕜 (fun x => G) G') (s : Finset (Fin n)) (hk : s.card = k) (z : G) {C : ℝ},
(∀ (m : Fin n → G), ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖) →
∀ (v : Fin k → G), ‖(f.restr s hk z) v‖ ≤ C * ‖z‖ ^ (n - k) * Finset.univ.prod fun i => ‖v i‖
This theorem states that for any multilinear map `f` in `n` variables over a non-trivially normed field `𝕜`, if we restrict `f` to `k` variables (indexed by a finite set `s` of cardinality `k`) by assigning the vector `z` to the other `n - k` variables, then the norm of the restricted function applied to a vector `v` is bounded above by `C` times the norm of `z` raised to the power `n - k` times the product of the norms of the components of `v`. This bound holds if the original function `f` has a norm which is bounded above by `C` times the product of the norms of the components of the input vector. In other words, the restriction of a bounded multilinear map remains bounded.
More concisely: For any multilinear map `f` over a non-trivially normed field with input size `n` and norm bound `C`, the restriction of `f` to any `k` variables with input `z` and the remaining `n-k` variables assigned arbitrary values has a norm bound of `C * ||z||^(n-k) * prod (||x_i||)` for any input vector `[x_1, ..., x_n]` with `||x_i||` denoting the norm of `x_i`.
|
MultilinearMap.bound_of_shell
theorem MultilinearMap.bound_of_shell :
∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
[inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : MultilinearMap 𝕜 E G) {ε : ι → ℝ} {C : ℝ},
(∀ (i : ι), 0 < ε i) →
∀ {c : ι → 𝕜},
(∀ (i : ι), 1 < ‖c i‖) →
(∀ (m : (i : ι) → E i),
(∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
(∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖) →
∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * Finset.univ.prod fun i => ‖m i‖
The theorem `MultilinearMap.bound_of_shell` states that, for a given multilinear map `f` defined on a finitely-sized set of normed spaces, if there exists some positive constants `ε i` and elements `c i : 𝕜` such that `1 < ‖c i‖` and `f` satisfies the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖` on a shell given by `ε i / ‖c i‖ < ‖m i‖ < ε i`, then `f` satisfies this inequality for all `m`. Here, `C` is a real number, `ε i` are positive real numbers, and `m` is a map from the set `ι` to the normed spaces `E i`. The product is taken over all elements in the finite set. This theorem essentially provides a generalization of a bound on the norm of a multilinear map from a specific shell to the entire domain of the map.
More concisely: Given a multilinear map `f` on finitely-sized normed spaces and constants `ε i` and `c i` such that `1 < ||ci||` and `||fm|| ≤ C * ∏i ||mi||` for all `mi` in the shell `εi / ||ci|| < ||mi|| < εi, f` satisfies this inequality for all `mi`.
|