ContinuousLinearMap.lipschitz_apply
theorem ContinuousLinearMap.lipschitz_apply :
∀ {𝕜 : 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 σ₁₂] (x : E),
LipschitzWith ‖x‖₊ fun f => f x
The theorem `ContinuousLinearMap.lipschitz_apply` states that for any continuous linear map `f`, evaluating `f` at a specific point is Lipschitz continuous in `f`. Here, Lipschitz continuity means that the distance between the outputs `f(x)` and `f(y)` (as measured with the extended metric `edist`) is at most a constant `K` times the distance between `x` and `y`. In this specific case, the Lipschitz constant is the nonnegative real-valued norm of the point `x` (`‖x‖₊`). This result holds in the context of seminormed additive commutative groups and nontrivially normed fields, which are types of mathematical structures used to generalize the concepts of vector spaces and fields, respectively, with associated norms and distances. The theorem is also stated under the assumption that there is an isometric ring homomorphism between the two nontrivially normed fields.
More concisely: For any continuous linear map f between nontrivially normed fields with an isometric ring homomorphism, the evaluation of f is Lipschitz continuous with constant equal to the norm of the input, i.e., ‖f(x) - f(y)‖₊ ≤ ‖x - y‖₊.
|
ContinuousLinearMap.op_nnnorm_le_bound
theorem ContinuousLinearMap.op_nnnorm_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] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F) (M : NNReal), (∀ (x : E), ‖f x‖₊ ≤ M * ‖x‖₊) → ‖f‖₊ ≤ M
This theorem, known as an alias of `ContinuousLinearMap.opNNNorm_le_bound`, states that if for all vectors `x` in a seminormed additive commutative group `E`, the nonnegative norm of the image of `x` under a continuous linear map `f` is less than or equal to the product of a nonnegative real number `M` and the nonnegative norm of `x`, then the nonnegative norm of `f` itself is less than or equal to `M`. Note that `E` and `F` are normed spaces over normed fields `𝕜` and `𝕜₂` respectively, and `σ₁₂` is a isometric ring homomorphism from `𝕜` to `𝕜₂`.
More concisely: If for all x in a seminormed additive commutative group E, the norm of f(x) in the normed space F is less than or equal to M times the norm of x in E, then the norm of the continuous linear map f from E to F is less than or equal to M.
|
ContinuousLinearMap.op_nnnorm_le_bound'
theorem ContinuousLinearMap.op_nnnorm_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] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F) (M : NNReal), (∀ (x : E), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊) → ‖f‖₊ ≤ M
This theorem, named `ContinuousLinearMap.op_nnnorm_le_bound'`, states that given any two types `𝕜` and `𝕜₂`, and any two types `E` and `F` that are seminormed additive commutative groups over these respective non-trivially normed fields, along with a normed space structure on `E` over `𝕜` and `F` over `𝕜₂`. If we have a continuous linear map `f` from `E` to `F` under a ring homomorphism `σ₁₂` that is isometric. Then for any nonnegative real number `M`, if for every `x` in `E` with non-zero seminorm, the seminorm of `f x` is less than or equal to `M` times the seminorm of `x`, then the seminorm of the linear map `f` is less than or equal to `M`. In other words, if we have a control on the norm of the image of every non-zero element under a continuous linear map, then we have a control on the norm of the linear map itself.
More concisely: If `f` is a continuous linear map between normed spaces `E` and `F` over non-trivially normed fields with `σ₁₂` as the underlying ring homomorphism and `isometric`, and for all non-zero `x` in `E`, `||fx|| ≤ M ||x||`, then `||f|| ≤ M`.
|
ContinuousLinearMap.lipschitz
theorem ContinuousLinearMap.lipschitz :
∀ {𝕜 : 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), LipschitzWith ‖f‖₊ ⇑f
The theorem `ContinuousLinearMap.lipschitz` states that for every continuous linear map `f` from a seminormed additively commutative group `E` over a nontrivially normed field `𝕜` to a seminormed additively commutative group `F` over a nontrivially normed field `𝕜₂`, with `σ₁₂` being a ring homomorphism between `𝕜` and `𝕜₂`, the map `f` is Lipschitz continuous with Lipschitz constant being the norm of `f`. In mathematical terms, this means that for all `x,y` in `E`, the extended distance (`edist`) between `f(x)` and `f(y)` in `F` is less than or equal to the norm of `f` times the extended distance between `x` and `y` in `E`.
More concisely: For every continuous linear map $f$ from a seminormed additively commutative group $E$ over a nontrivially normed field $\mathbb{K}$ to a seminormed additively commutative group $F$ over a nontrivially normed field $\mathbb{K}_2$, with $\sigma\_1\_2$ being a ring homomorphism from $\mathbb{K}$ to $\mathbb{K}_2$, the Lipschitz constant of $f$ is equal to the norm of $f$, i.e., $\text{edist}(f(x), f(y)) \leq \|f\| \cdot \text{edist}(x, y)$, for all $x, y \in E$.
|
ContinuousLinearMap.op_nnnorm_le_of_unit_nnnorm
theorem ContinuousLinearMap.op_nnnorm_le_of_unit_nnnorm :
∀ {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 : NNReal},
(∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C) → ‖f‖₊ ≤ C
This theorem, known as an alias of `ContinuousLinearMap.opNNNorm_le_of_unit_nnnorm`, states that for any continuous real linear map `f` from a seminormed add commutative group `E` to another seminormed add commutative group `F` (both of which are also normed spaces over real numbers), if we are able to limit the nonnegative norm (`‖f x‖₊`) of any result `f x` where the nonnegative norm of `x` (`‖x‖₊`) equals 1, to a nonnegative real number `C`, then we can also limit the nonnegative norm of the linear map `f` (`‖f‖₊`) to the same `C`. In mathematical terms, if ∀ `x` in `E` such that `‖x‖₊ = 1`, we have `‖f x‖₊ ≤ C`, then `‖f‖₊ ≤ C`.
More concisely: If a continuous real linear map from a seminormed add commutative group to another seminormed add commutative group, both of which are normed spaces over real numbers, maps unit balls to bounded sets, then the norm of the linear map is bounded by the supremum of the norms of the images of the unit balls.
|