ContinuousLinearMap.continuous₂
theorem ContinuousLinearMap.continuous₂ :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G),
Continuous (Function.uncurry fun x y => (f x) y)
This theorem establishes the continuity of a function which is obtained by uncurrying a continuous bilinear map. More specifically, it states that for any non-trivially normed field `𝕜`, and any normed additive commutative groups `E`, `F`, `G` that are also normed over `𝕜`, given a continuous bilinear map `f` from `E` to `F` and then to `G`, the uncurried function `fun x y => (f x) y` is also continuous. The uncurried function takes as input a pair of values from `E` and `F` and returns a value in `G`. This theorem is particularly useful when combined with `Continuous.comp₂`.
More concisely: For any non-trivially normed field `𝕜` and normed additive commutative groups `E`, `F`, `G` over `𝕜`, the uncurried function `(x, y) ↦ f x y` is continuous if `f` is a continuous bilinear map from `E` to `F` to `G`.
|
isBoundedBilinearMap_smulRight
theorem isBoundedBilinearMap_smulRight :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
IsBoundedBilinearMap 𝕜 fun p => p.1.smulRight p.2
The theorem `isBoundedBilinearMap_smulRight` asserts that for any nontrivially normed field `𝕜`, and any normed add commutative groups `E` and `F` over `𝕜`, the function `ContinuousLinearMap.smulRight`, which associates to a continuous linear map `f : E → 𝕜` and a scalar `c : F` the tensor product `f ⊗ c` as a continuous linear map from `E` to `F`, is a bounded bilinear map. This means the function respects scalar multiplication and addition in both of its arguments, and its output can be bounded by a constant times the product of the norms of its input.
More concisely: For any nontrivially normed field 𝕜, and normed add commutative groups E and F over 𝕜, the function ContinuousLinearMap.smulRight from a continuous linear map f : E → 𝕜 and a scalar c : F to the tensor product f ⊗ c as a continuous linear map from E to F is a bounded bilinear map.
|
ContinuousLinearMap.isBoundedBilinearMap
theorem ContinuousLinearMap.isBoundedBilinearMap :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G),
IsBoundedBilinearMap 𝕜 fun x => (f x.1) x.2
This theorem states that for any non-trivially normed field `𝕜`, and any normed add commutative groups `E`, `F`, and `G` that are normed spaces over `𝕜`, if you have a continuous linear map `f` that takes an element of `E` and returns a linear map from `F` to `G`, then the map that takes a pair of elements from `E` and `F` respectively and applies the corresponding linear map is a bounded bilinear map over `𝕜`. This means that this map is linear in each argument and there exists a constant such that the norm of the image of a pair of vectors is less than this constant times the product of the norms of the vectors.
More concisely: Given a non-trivially normed field `𝕜`, and continuous linear maps `f : E → L(F, G)` between normed spaces `E`, `F`, and `G` over `𝕜`, the map `(x, y) ↦ f(x)(y)` is a bounded bilinear map.
|
isBoundedLinearMap_continuousMultilinearMap_comp_linear
theorem isBoundedLinearMap_continuousMultilinearMap_comp_linear :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {ι : Type u_5} [inst_7 : Fintype ι]
(g : G →L[𝕜] E), IsBoundedLinearMap 𝕜 fun f => f.compContinuousLinearMap fun x => g
This theorem states that for a certain continuous linear map `g`, the operation that takes a continuous multilinear map `f` and creates a new continuous multilinear map that applies `g` to each of its inputs is a bounded linear operation. In more mathematical language, if `g` is a continuous linear map from a normed vector space `G` to another normed vector space `E` over a nontrivially normed field `𝕜`, and `f` is a continuous multilinear map, then the map that sends `f` to `f compose g` is a bounded linear map.
More concisely: Given a continuous linear map `g` between normed vector spaces and a continuous multilinear map `f`, the map that sends `f` to the composition `f ∘ g` is a bounded linear map.
|
isBoundedLinearMap_prod_multilinear
theorem isBoundedLinearMap_prod_multilinear :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
{ι : Type u_5} [inst_5 : Fintype ι] {E : ι → Type u_6} [inst_6 : (i : ι) → NormedAddCommGroup (E i)]
[inst_7 : (i : ι) → NormedSpace 𝕜 (E i)], IsBoundedLinearMap 𝕜 fun p => p.1.prod p.2
The theorem `isBoundedLinearMap_prod_multilinear` states that for any non-trivially normed field `𝕜`, types `F` and `G` which have the structure of normed additive commutative groups and are normed spaces over `𝕜`, a finite type `ι`, and for any type `E` indexed by `ι` that is a normed additive commutative group and a normed space over `𝕜`, the operation of taking the cartesian product of two continuous multilinear maps is a bounded linear operation. In other words, the map that sends a pair of continuous multilinear maps to their cartesian product is itself a bounded linear map over `𝕜`.
More concisely: Given normed fields 𝕜, normed additive commutative groups and normed spaces F, G over 𝕜, and a finite type ι with a normed additive commutative group and normed space E indexed by ι, the operation of taking the cartesian product of two continuous multilinear maps from F x E to G and E to G is a bounded linear map from F x E ≅ E^ι to G.
|
isBoundedBilinearMap_apply
theorem isBoundedBilinearMap_apply :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
IsBoundedBilinearMap 𝕜 fun p => p.1 p.2
This theorem states that for any non-trivially normed field `𝕜`, and any normed spaces `E` and `F` over `𝕜`, the operation of applying an element of `E` to an element of `F` is a bounded bilinear map. In other words, this operation is linear in each argument and there exists a constant `C` such that the norm of the result is less than or equal to `C` times the product of the norms of the arguments.
More concisely: For any non-trivially normed field `𝕜`, and normed spaces `E` and `F` over `𝕜`, the bilinear map `E × F → 𝕜` given by `(x, y) ↦ x • y` is bounded.
|
isBoundedBilinearMap_compMultilinear
theorem isBoundedBilinearMap_compMultilinear :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
{ι : Type u_5} {E : ι → Type u_6} [inst_5 : Fintype ι] [inst_6 : (i : ι) → NormedAddCommGroup (E i)]
[inst_7 : (i : ι) → NormedSpace 𝕜 (E i)], IsBoundedBilinearMap 𝕜 fun p => p.1.compContinuousMultilinearMap p.2
This theorem states that for a nontrivially normed field 𝕜 and normed additive commutative groups F, G, and E indexed by ι, the operation of composing a continuous linear map (from F to G) with a continuous multilinear map (from E to F) is a bounded bilinear operation over 𝕜. This means that given any fixed continuous linear map or multilinear map, the composition operation is linear in the other variable, and there exists a constant such that the norm of the composed map is bounded by the product of the norms of the two maps times this constant.
More concisely: For a nontrivially normed field 𝕜 and normed additive commutative groups F, G, and E indexed by ι, the composition of a continuous linear map from F to G with a continuous multilinear map from E to F is a bounded bilinear operation over 𝕜.
|
IsBoundedBilinearMap.continuous
theorem IsBoundedBilinearMap.continuous :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G},
IsBoundedBilinearMap 𝕜 f → Continuous f
This theorem states that for all normed spaces E, F, G over a non-trivially normed field 𝕜, if a function `f` from the Cartesian product of E and F to G is a bounded bilinear map, then `f` is continuous. This theorem is particularly useful when used in combination with the `Continuous.comp₂` theorem.
More concisely: A bounded bilinear map between two normed spaces over a non-trivially normed field is continuous.
|
IsBoundedBilinearMap.isBoundedLinearMap_deriv
theorem IsBoundedBilinearMap.isBoundedLinearMap_deriv :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
{G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G}
(h : IsBoundedBilinearMap 𝕜 f), IsBoundedLinearMap 𝕜 fun p => h.deriv p
The theorem `IsBoundedBilinearMap.isBoundedLinearMap_deriv` states that, for any bounded bilinear map `f` from pairs of elements in normed spaces `E` and `F` to a normed space `G`, the function that maps a point `p` to the derivative of `f` at `p` is itself a bounded linear map. In other words, the process of taking derivatives of a bounded bilinear map produces another map that is linear and bounded. Here, `𝕜` is a non-trivially normed field, which can be thought of as a field equipped with a notion of size or absolute value that satisfies certain properties.
More concisely: The derivative of a bounded bilinear map between normed spaces is a bounded linear map.
|
IsLinearMap.with_bound
theorem IsLinearMap.with_bound :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
IsLinearMap 𝕜 f → ∀ (M : ℝ), (∀ (x : E), ‖f x‖ ≤ M * ‖x‖) → IsBoundedLinearMap 𝕜 f
This theorem, `IsLinearMap.with_bound`, states that for any nontrivial normed field `𝕜`, any normed additively commutative group `E` over `𝕜`, any normed additively commutative group `F` over `𝕜`, and any function `f` from `E` to `F`, if `f` is a linear map and there exists a real number `M` such that the norm of `f(x)` does not exceed `M` times the norm of `x` for any `x` in `E`, then `f` is a bounded linear map.
In other words, it asserts that a linear map is guaranteed to be a bounded linear map if each input's magnitude is expanded by no more than a constant factor after the map.
More concisely: A linear map from one normed additive commutative group to another, over a nontrivial normed field, is bounded if there exists a constant such that the norm of the image is less than or equal to the norm of the input multiplied by the constant for all inputs.
|
ContinuousLinearMap.isBoundedLinearMap
theorem ContinuousLinearMap.isBoundedLinearMap :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
(f : E →L[𝕜] F), IsBoundedLinearMap 𝕜 ⇑f
This theorem states that for any continuous linear map `f` from a normed vector space `E` over a nontrivially normed field `𝕜` to another normed vector space `F` over the same field, `f` satisfies the property of a bounded linear map. Here, 'bounded' means that there is a constant C such that the norm of `f(x)` is less than or equal to C times the norm of `x` for all `x` in `E`.
More concisely: For any continuous linear map `f` from a normed vector space `E` to another normed vector space `F` over the same nontrivially normed field, `f` is a bounded linear map with a constant `C` such that `‖f(x)‖ ≤ C * ‖x‖ for all `x` in `E`.
|