ContinuousLinearMap.norm_id_of_nontrivial_seminorm
theorem ContinuousLinearMap.norm_id_of_nontrivial_seminorm :
∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : NormedSpace 𝕜 E], (∃ x, ‖x‖ ≠ 0) → ‖ContinuousLinearMap.id 𝕜 E‖ = 1
This theorem states that given a seminormed additive commutative group `E` and a nontrivially normed field `𝕜` that forms a normed space with `E`, if there exists an element in `E` whose norm is not zero, then the norm of the identity map (which is a continuous linear map from `E` to `E`) equals `1`.
It's important to note that this theorem is specifically for the case when we are working with seminorms, as the existence of a non-trivial element (an element with norm different from `0`) in the space `E` is not enough to ensure the norm of the identity map equals `1`.
More concisely: If `E` is a seminormed additive commutative group with a nontrivially normed field `𝕜` forming a normed space with `E`, and there exists an element in `E` with non-zero norm, then the norm of the identity map from `E` to `E` equals 1.
|
ContinuousLinearMap.opNorm_eq_of_bounds
theorem ContinuousLinearMap.opNorm_eq_of_bounds :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {φ : E →SL[σ₁₂] F} {M : ℝ},
0 ≤ M → (∀ (x : E), ‖φ x‖ ≤ M * ‖x‖) → (∀ N ≥ 0, (∀ (x : E), ‖φ x‖ ≤ N * ‖x‖) → M ≤ N) → ‖φ‖ = M
This theorem states that for any normed add-commutative group `E` and `F` over nontrivially normed fields `𝕜` and `𝕜₂` respectively, and a continuous linear map `φ` from `E` to `F` respecting the linear structures of `𝕜` and `𝕜₂`, if there exists a non-negative real number `M` such that the norm of `φ` applied to any element `x` of `E` is less than or equal to `M` times the norm of `x`, and for any non-negative number `N` such that the norm of `φ` applied to any element `x` of `E` is less than or equal to `N` times the norm of `x`, `M` is less than or equal to `N`, then the operator norm of `φ` is equal to `M`. Essentially, this theorem states the conditions for a continuous linear map to have a specific operator norm.
More concisely: Given a continuous linear map φ between normed add-commutative groups over nontrivially normed fields, if there exists a constant M such that ||φ(x)|| ≤ M ||x|| for all x and a constant N with the same property where M ≤ N, then the operator norm of φ equals M.
|
ContinuousLinearMap.op_norm_le_bound'
theorem ContinuousLinearMap.op_norm_le_bound' :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ},
0 ≤ M → (∀ (x : E), ‖x‖ ≠ 0 → ‖f x‖ ≤ M * ‖x‖) → ‖f‖ ≤ M
This theorem, named `ContinuousLinearMap.op_norm_le_bound'`, states that if the norm of the output of a continuous linear map `A` (in this context represented as `f`) on any non-zero vector `x` can be bounded above by a non-negative scalar `M` times the norm of `x`, then the operator norm of `A` itself is also bounded above by `M`. Here, the norm of a vector and the operator norm of a linear map are considered in the context of normed spaces over non-trivially normed fields.
More concisely: If for every non-zero vector x in a normed space, the norm of the image of x under a continuous linear map A is bounded above by M times the norm of x, then the operator norm of A is bounded above by M.
|
ContinuousLinearMap.unit_le_opNorm
theorem ContinuousLinearMap.unit_le_opNorm :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F) (x : E), ‖x‖ ≤ 1 → ‖f x‖ ≤ ‖f‖
This theorem states that for any continuous linear map 'f' from a normed vector space 'E' over a nontrivially normed field '𝕜' to a normed vector space 'F' over a nontrivially normed field '𝕜₂', the norm of the image of any vector 'x' from 'E' (with a norm less than or equal to 1) under 'f' is less than or equal to the operator norm of 'f'. The operator norm here is the maximum multiple by which 'f' expands a vector.
More concisely: For any continuous linear map $f$ from normed vector space $E$ over a nontrivially normed field $\mathbb{K}$ to normed vector space $F$ over a nontrivially normed field $\mathbb{K}_2$, the norm of $f(x)$ with respect to $F$ is less than or equal to the operator norm of $f$ times the norm of $x$ with respect to $E$, for all $x$ in $E$ with norm less than or equal to 1.
|
LinearMap.mkContinuous_norm_le'
theorem LinearMap.mkContinuous_norm_le' :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ₁₂] F) {C : ℝ}
(h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖), ‖f.mkContinuous C h‖ ≤ max C 0
The theorem states that for any continuous linear map, constructed from a linear map `f` using the constructor `mkContinuous`, its norm is either bounded by a certain real number `C` or zero, if `C` is negative. Here, the map `f` is between two normed vector spaces `E` and `F` over two general non-trivially normed fields `𝕜` and `𝕜₂`, with an assumption 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 : E → F` constructed from a normed linear map `x : E → F` with `∀x ∈ E, ||x||₂ ≤ C ||f x||₂`, the map `f` has a norm bounded by `C` in the second normed vector space `F` over field `𝕜₂`, or is the zero map if `C` is negative.
|
ContinuousLinearMap.le_opNorm
theorem ContinuousLinearMap.le_opNorm :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F) (x : E), ‖f x‖ ≤ ‖f‖ * ‖x‖
This theorem, `ContinuousLinearMap.le_opNorm`, states the fundamental property of the operator norm for continuous linear maps. It applies to two nontrivial normed fields, 𝕜 and 𝕜₂, and two seminormed additive commutative groups, E and F. The theorem asserts that for any continuous linear map `f` from E to F and any element `x` in E, the norm of the result of applying `f` to `x` is less than or equal to the product of the operator norm of `f` and the norm of `x`. In mathematical notation, this is written as `‖f x‖ ≤ ‖f‖ * ‖x‖`.
More concisely: For any continuous linear map between normed vector spaces and any vector in the domain, the norm of the image is less than or equal to the operator norm of the map times the norm of the vector.
|
ContinuousLinearMap.op_norm_zero
theorem ContinuousLinearMap.op_norm_zero :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂}, ‖0‖ = 0
This theorem, titled "Alias of ContinuousLinearMap.opNorm_zero", states that the operator norm of the zero operator is zero. The theorem applies in the context of two seminormed additive commutative groups `E` and `F`, two non-trivially normed fields `𝕜` and `𝕜₂`, and normed spaces over these fields. The type `σ₁₂` is a ring homomorphism from `𝕜` to `𝕜₂`. The operator norm ‖0‖ of the zero operator (which is essentially a measure of the "size" or "magnitude" of the operator) is proven to be equal to zero.
More concisely: The operator norm of the zero linear map from a normed space over a field to another normed space over another field is equal to zero.
|
ContinuousLinearMap.le_of_opNorm_le
theorem ContinuousLinearMap.le_of_opNorm_le :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F) {c : ℝ}, ‖f‖ ≤ c → ∀ (x : E), ‖f x‖ ≤ c * ‖x‖
This theorem, `ContinuousLinearMap.le_of_opNorm_le`, states that for any continuous linear map `f` from a normed space `E` over a nontrivially normed field `𝕜` to a normed space `F` over a nontrivially normed field `𝕜₂`, given a real number `c`, if the operator norm (or "opNorm") of `f` is less than or equal to `c`, then for any vector `x` in `E`, the norm of `f(x)` is less than or equal to `c` times the norm of `x`. This theorem essentially bounds the norm of the image of a vector under a continuous linear map in terms of the norm of the vector itself and a constant factor determined by the operator norm of the map.
More concisely: For any continuous linear map between normed spaces and a real constant, if the operator norm of the map is less than or equal to the constant, then the norm of the image of any vector under the map is less than or equal to the constant times the norm of the vector.
|
ContinuousLinearMap.unit_le_op_norm
theorem ContinuousLinearMap.unit_le_op_norm :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F) (x : E), ‖x‖ ≤ 1 → ‖f x‖ ≤ ‖f‖
The theorem `ContinuousLinearMap.unit_le_op_norm` states that for any two types `𝕜` and `𝕜₂` representing scalar fields, and any two types `E` and `F` representing seminormed add commutative groups (which can be thought of as vector spaces over the scalar fields `𝕜` and `𝕜₂` respectively), if `f` is a continuous linear map from `E` to `F` and `x` is any element of `E` with a norm less than or equal to 1, then the norm of the image of `x` under `f` is less than or equal to the operator norm (`‖f‖`) of `f`. This means the image of the unit ball under a continuous linear map is bounded.
More concisely: For any continuous linear map `f` between seminormed add commutative groups `E` and `F` over scalar fields `𝕜` and `𝕜₂`, respectively, and any `x` in `E` with norm less than or equal to 1, the norm of `f(x)` is less than or equal to the operator norm of `f`.
|
norm_image_of_norm_zero
theorem norm_image_of_norm_zero :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {𝓕 : Type u_10} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : FunLike 𝓕 E F]
[inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕), Continuous ⇑f → ∀ {x : E}, ‖x‖ = 0 → ‖f x‖ = 0
The theorem `norm_image_of_norm_zero` states that for any semi-normed additive commutative group `E` and `F`, nontrivially normed fields `𝕜` and `𝕜₂`, any type `𝓕` that has an injective function to map from `E` to `F`, any semilinear map from `𝓕` to `σ₁₂`, and any continuous function `f` from `E` to `F`, if the norm of a vector `x` in `E` is zero, then the norm of the image of `x` under `f` is also zero. In simpler terms, if a vector in one normed space has a norm of zero, then its image under a continuous function in another normed space also has a norm of zero.
More concisely: If `f` is a continuous semilinear map from the normed space `(E, ‖·‖)` to the normed space `(F, ‖⋅‖)`, and `x` is an element of `E` with `‖x‖ = 0`, then `‖f(x)‖ = 0`.
|
ContinuousLinearMap.opNorm_le_bound
theorem ContinuousLinearMap.opNorm_le_bound :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ},
0 ≤ M → (∀ (x : E), ‖f x‖ ≤ M * ‖x‖) → ‖f‖ ≤ M
This theorem states that for a continuous linear map `f` from a normed vector space `E` over a nontrivially normed field `𝕜` to a normed vector space `F` over another nontrivially normed field `𝕜₂`, if there exists a non-negative real number `M` such that the norm of `f(x)` is always less than or equal to `M` times the norm of `x` for all `x` in `E`, then the operator norm of `f` is less than or equal to `M`. In other words, if you can bound the norm of the image of any vector `x` by a constant times the norm of `x`, then you can bound the operator norm of the linear map by the same constant.
More concisely: If a continuous linear map between two normed vector spaces satisfies the condition that the norm of its image is less than or equal to a constant times the norm of the input for all inputs, then the operator norm of the map is less than or equal to that constant.
|
ContinuousLinearMap.op_norm_le_bound
theorem ContinuousLinearMap.op_norm_le_bound :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ},
0 ≤ M → (∀ (x : E), ‖f x‖ ≤ M * ‖x‖) → ‖f‖ ≤ M
This theorem, `ContinuousLinearMap.op_norm_le_bound`, states a property for continuous linear maps between normed spaces. Specifically, for a continuous linear map `f` from a normed space `E` over a nontrivially normed field `𝕜` to a normed space `F` over another nontrivially normed field `𝕜₂`, given a real number `M` which is greater than or equal to zero, if the norm of `f x` is less than or equal to `M` times the norm of `x` for every `x` in `E`, then the operator norm of `f`, denoted as `‖f‖`, is less than or equal to `M`.
More concisely: Given a continuous linear map `f` between normed spaces over nontrivially normed fields, if `‖fx‖ ≤ M‖x‖` for all `x` in the domain, then `‖f‖ ≤ M`.
|
LinearMap.mkContinuous_norm_le
theorem LinearMap.mkContinuous_norm_le :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ₁₂] F) {C : ℝ},
0 ≤ C → ∀ (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖), ‖f.mkContinuous C h‖ ≤ C
This theorem states that if a continuous linear map is constructed from a given linear map using the `mkContinuous` constructor with a nonnegative real number as the bound, then the norm of the resulting continuous map is bounded by that nonnegative real number. This holds for all elements of the input space, such that the norm of the linear map applied to any element is less than or equal to the product of the bound and the norm of the element. The spaces involved are normed spaces over nontrivially normed fields.
More concisely: Given a continuous linear map created from a linear map using `mkContinuous` with a bound, the norm of the continuous map is bounded by the product of the bound and the element's norm, provided the linear map's norm times the element's norm is less than or equal to the bound.
|
ContinuousLinearMap.op_norm_comp_le
theorem ContinuousLinearMap.op_norm_comp_le :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
[inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
[inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
[inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomIsometric σ₁₂]
[inst_11 : RingHomIsometric σ₂₃] (h : F →SL[σ₂₃] G) (f : E →SL[σ₁₂] F), ‖h.comp f‖ ≤ ‖h‖ * ‖f‖
This theorem, named `ContinuousLinearMap.op_norm_comp_le`, states that the operator norm is submultiplicative over continuous linear maps. Specifically, for any three types corresponding to seminormed additive commutative groups `E`, `F`, and `G` and variables `h` and `f` that are continuous linear maps from `F` to `G` and from `E` to `F` respectively, the norm of the composition of `h` and `f` is less than or equal to the product of the norms of `h` and `f`. This is true across three non-trivially normed fields `𝕜`, `𝕜₂`, and `𝕜₃` with appropriate ring homomorphism triples and isometric properties.
More concisely: For any continuous linear maps $f : E \to F$ and $h : F \to G$ between seminormed additive commutative groups over non-trivially normed fields, the operator norm of their composition $h \circ f$ is less than or equal to the product of the operator norms of $h$ and $h$.
|
SemilinearMapClass.bound_of_continuous
theorem SemilinearMapClass.bound_of_continuous :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {𝓕 : Type u_10} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : FunLike 𝓕 E F]
[inst_7 : RingHomIsometric σ₁₂] [inst_8 : SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕),
Continuous ⇑f → ∃ C, 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
The theorem `SemilinearMapClass.bound_of_continuous` states that for any continuous semilinear map `f` between two seminormed spaces `E` and `F` over nontrivially normed fields `𝕜` and `𝕜₂` respectively, there exists a positive constant `C` such that the norm of the image of any element `x` from `E` under `f` is less than or equal to `C` times the norm of `x`. Here, continuity of `f` implies its boundedness within a certain ball of radius `ε`. The nontriviality of the norm allows us to rescale any element into an element whose norm is in the range `[ε/C, ε]` and its image under `f` has a controlled norm. The norm control for the original element is achieved by rescaling accordingly.
More concisely: For any continuous semilinear map between two seminormed spaces over nontrivially normed fields, there exists a constant C such that the norm of the image of any element is bounded by C times the norm of the element.
|
ContinuousLinearMap.le_opNorm_of_le
theorem ContinuousLinearMap.le_opNorm_of_le :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F) {c : ℝ} {x : E}, ‖x‖ ≤ c → ‖f x‖ ≤ ‖f‖ * c
The theorem `ContinuousLinearMap.le_opNorm_of_le` states that for any two seminormed additive commutative groups `E` and `F`, two nontrivially normed fields `𝕜` and `𝕜₂`, a normed space structure over `E` and `F` with respect to `𝕜` and `𝕜₂` respectively, a ring homomorphism `σ₁₂` from `𝕜` to `𝕜₂` which is an isometry, and a continuous linear map `f` from `E` to `F`, if the norm of an element `x` from `E` is less than or equal to a real number `c`, then the norm of `f(x)` is less than or equal to the operator norm of `f` multiplied by `c`. This theorem expresses a bounding property of continuous linear maps in the context of normed spaces.
More concisely: For a continuous linear map between normed spaces, the norm of the image of any element is less than or equal to the operator norm times the norm of the element.
|
ContinuousLinearMap.op_norm_le_of_unit_norm
theorem ContinuousLinearMap.op_norm_le_of_unit_norm :
∀ {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F]
[inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace ℝ F] {f : E →L[ℝ] F} {C : ℝ},
0 ≤ C → (∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C) → ‖f‖ ≤ C
This theorem, "ContinuousLinearMap.op_norm_le_of_unit_norm", states that for any continuous real linear map `f` from a seminormed addition commutative group `E` to a seminormed addition commutative group `F`, and for any real number `C` that is greater than or equal to zero, if the norm of every `f x` where `‖x‖` equals 1 is less than or equal to `C`, then the norm of `f` itself is also less than or equal to `C`. This theorem, in essence, provides a way to control the norm of `f` using the norm of `f x` where `x` is a unit vector.
More concisely: For any continuous real linear map between seminormed additive commutative groups with the property that the norm of the image of every unit vector is less than or equal to a constant C, the norm of the linear map itself is also less than or equal to C.
|
ContinuousLinearMap.norm_id_le
theorem ContinuousLinearMap.norm_id_le :
∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : NormedSpace 𝕜 E], ‖ContinuousLinearMap.id 𝕜 E‖ ≤ 1
The theorem `ContinuousLinearMap.norm_id_le` states that the norm of the identity map on a non-trivial normed space over a non-trivially normed field is at most `1`. More specifically, it assures that the norm of the identity map as a continuous linear map from a space to itself does not exceed `1`. However, the norm is indeed `1`, except when the space itself is trivial, in which case it is `0`. This entails that one cannot establish a stronger result than this inequality in a general case.
More concisely: The norm of the identity map as a continuous linear operator on a non-trivial normed space over a non-trivially normed field does not exceed 1.
|
ContinuousLinearMap.le_of_opNorm_le_of_le
theorem ContinuousLinearMap.le_of_opNorm_le_of_le :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F) {x : E} {a b : ℝ}, ‖f‖ ≤ a → ‖x‖ ≤ b → ‖f x‖ ≤ a * b
This theorem states that for every seminormed additive commutative group `E` and `F`, nontrivially normed fields `𝕜` and `𝕜₂`, and normed spaces over `E` and `F` with respect to `𝕜` and `𝕜₂` respectively, if a continuous linear map `f` from `E` to `F` exists under a ring homomorphism `σ₁₂` from `𝕜` to `𝕜₂`, then for every element `x` in `E` and real numbers `a` and `b`, if the operator norm of `f` is less than or equal to `a` and the norm of `x` is less than or equal to `b`, then the norm of the result of applying `f` to `x` is less than or equal to the product of `a` and `b`.
More concisely: Given a seminormed additive commutative group `E`, nontrivially normed fields `𝕜` and `𝕜₂`, normed spaces `X` over `E` with respect to `𝕜` and `Y` over `F` with respect to `𝕜₂`, a continuous linear map `f : E → F` under a ring homomorphism `σ₁₂ : 𝕜 → 𝕜₂`, if the operator norm of `f` is less than or equal to a and the norm of every x in E is less than or equal to b, then the norm of `f(x)` in Y is less than or equal to `a * b`.
|
ContinuousLinearMap.opNorm_nonneg
theorem ContinuousLinearMap.opNorm_nonneg :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F), 0 ≤ ‖f‖
This theorem states that for any continuous linear map `f` from a normed vector space `E` over a non-trivially normed field `𝕜` to another normed vector space `F` over a non-trivially normed field `𝕜₂`, the operator norm of `f` is always non-negative. In other words, the norm of a continuous linear map is never less than zero.
More concisely: For any continuous linear map between two normed vector spaces over non-trivially normed fields, the operator norm is non-negative.
|
ContinuousLinearMap.le_op_norm
theorem ContinuousLinearMap.le_op_norm :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F) (x : E), ‖f x‖ ≤ ‖f‖ * ‖x‖
This is an alias of the `ContinuousLinearMap.le_opNorm` theorem in Lean 4. It establishes a fundamental property of the operator norm for continuous linear maps between seminormed groups over non-trivially normed fields. Specifically, the property states that the norm of the image of a vector under a continuous linear map is less than or equal to the product of the operator norm of the map and the norm of the vector itself. In mathematical notation, this is written as `‖f x‖ ≤ ‖f‖ * ‖x‖`, where `f` is the continuous linear map and `x` is a vector in the domain of `f`.
More concisely: The operator norm of a continuous linear map between seminormed groups over non-trivially normed fields satisfies the inequality ‖f(x)‖ ≤ ‖f‖ * ‖x‖ for all vectors x in the domain of f.
|
ContinuousLinearMap.op_norm_add_le
theorem ContinuousLinearMap.op_norm_add_le :
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f g : E →SL[σ₁₂] F), ‖f + g‖ ≤ ‖f‖ + ‖g‖
The theorem `ContinuousLinearMap.op_norm_add_le` states that for any two continuous linear maps `f` and `g` from a normed space `E` over a nontrivially normed field `𝕜` to another normed space `F` over another nontrivially normed field `𝕜₂`, with a ring homomorphism `σ₁₂` from `𝕜` to `𝕜₂` that is an isometry, the operator norm (denoted by `‖‖`) of the sum of `f` and `g` is less than or equal to the sum of the operator norms of `f` and `g`. This is essentially stating that the operator norm satisfies the triangle inequality in the context of continuous linear maps.
More concisely: For continuous linear maps `f` and `g` from a normed space over isometrically embedded fields, the operator norm of their sum is less than or equal to the sum of their individual operator norms.
|