ContinuousLinearMap.antilipschitz_of_embedding
theorem ContinuousLinearMap.antilipschitz_of_embedding :
β {π : Type u_1} {E : Type u_4} {Fβ : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup Fβ]
[inst_2 : NontriviallyNormedField π] [inst_3 : NormedSpace π E] [inst_4 : NormedSpace π Fβ] (f : E βL[π] Fβ),
Embedding βf β β K, AntilipschitzWith K βf
The theorem `ContinuousLinearMap.antilipschitz_of_embedding` states that for any continuous linear map `f` from a normed additive commutative group `E` over a non-trivially normed field `π` to another normed additive commutative group `Fβ` over the same field, if `f` is an embedding (i.e., a function that preserves the topology), then there exists a non-negative real number `K` such that `f` is `AntilipschitzWith K`. This means that for any two points `x` and `y` in `E`, the extended distance (or edist) between `x` and `y` is less than or equal to `K` times the edist between `f(x)` and `f(y)` in `Fβ`. In essence, the theorem asserts that a continuous linear embedding expands distances by a positive factor.
More concisely: For any continuous linear embedding of normed additive commutative groups over a non-trivially normed field, there exists a constant K such that the extended distance between any two points in the domain is less than or equal to K times the extended distance between their images.
|
ContinuousLinearMap.norm_smulRight_apply
theorem ContinuousLinearMap.norm_smulRight_apply :
β {π : Type u_1} {E : Type u_4} {Fβ : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup Fβ]
[inst_2 : NontriviallyNormedField π] [inst_3 : NormedSpace π E] [inst_4 : NormedSpace π Fβ] (c : E βL[π] π)
(f : Fβ), βc.smulRight fβ = βcβ * βfβ
This theorem states that for any scalar linear map 'c' from a normed space 'E' to a field 'π' and any element 'f' of a normed space 'Fβ', the norm of the tensor product of 'c' and 'f' (denoted as `ContinuousLinearMap.smulRight c f`) is equal to the product of the individual norms of 'c' and 'f'. In other words, βContinuousLinearMap.smulRight c fβ = βcβ * βfβ. This is valid in the context where 'E' and 'Fβ' are normed additive commutative groups, 'π' is a non-trivially normed field, and both 'E' and 'Fβ' are normed spaces over 'π'.
More concisely: The norm of the tensor product of a continuous linear map and an element from two normed spaces is equal to the product of their individual norms.
|
LinearIsometry.norm_toContinuousLinearMap_comp
theorem LinearIsometry.norm_toContinuousLinearMap_comp :
β {π : Type u_1} {πβ : Type u_2} {πβ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup 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 Οββ]
(f : F βββα΅’[Οββ] G) {g : E βSL[Οββ] F}, βf.toContinuousLinearMap.comp gβ = βgβ
This theorem states that for any types π, πβ, πβ, E, F, and G, given that E, F, and G are normed add commutative groups, π, πβ, and πβ are nontrivially normed fields, E is a normed space over π, F is a normed space over πβ, G is a normed space over πβ, Οββ, Οββ, and Οββ are ring homomorphisms, and Οββ is a ring homomorphism isometry, for any linear isometry `f` from F to G under Οββ and any continuous linear map `g` from E to F under Οββ, the operator norm (or spectral norm) of the composition of `f` and `g` is equal to the operator norm of `g`. This essentially means that applying a linear isometry after a continuous linear map does not change the operator norm of the original continuous linear map.
More concisely: Given normed add commutative groups E, F, G, nontrivially normed fields π, πβ, πβ, ring homomorphisms Οββ (an isometry), Οββ, and continuous linear maps f : F β G and g : E β F, the operator norm of the composition g β f equals the operator norm of g.
|
LinearIsometry.norm_toContinuousLinearMap
theorem LinearIsometry.norm_toContinuousLinearMap :
β {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField π] [inst_3 : NontriviallyNormedField πβ]
[inst_4 : NormedSpace π E] [inst_5 : NormedSpace πβ F] {Οββ : π β+* πβ} [inst_6 : Nontrivial E]
[inst_7 : RingHomIsometric Οββ] (f : E βββα΅’[Οββ] F), βf.toContinuousLinearMapβ = 1
The theorem `LinearIsometry.norm_toContinuousLinearMap` states that for any given linear isometry `f` from a normed space `E` over a non-trivially normed field `π` to another normed space `F` over a non-trivially normed field `πβ`, with a isometric ring homomorphism `Οββ` between `π` and `πβ`, the norm of the continuous linear map corresponding to `f`, obtained using the function `LinearIsometry.toContinuousLinearMap`, is equal to 1. This underlines the fact that the linear isometry preserves the norm when it is interpreted or converted into a continuous linear map.
More concisely: For any linear isometry between two normed spaces over non-trivially normed fields with a given isometric ring homomorphism, the norm of the resulting continuous linear map is equal to 1.
|
ContinuousLinearMap.norm_id
theorem ContinuousLinearMap.norm_id :
β {π : Type u_1} {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NontriviallyNormedField π]
[inst_2 : NormedSpace π E] [inst_3 : Nontrivial E], βContinuousLinearMap.id π Eβ = 1
This theorem states that if we have a non-trivial normed space (denoted by `E`), then the norm of the identity map on that space equals `1`. Here, `π` is a field (like the real or complex numbers) which is both normed and non-trivial (i.e., not all elements have zero norm). `E` is a vector space over `π` which is also a topological space where the topology is defined by a norm. The identity map is a continuous linear map from the normed space to itself. In this context, the norm of a continuous linear map is a measure of how much it can "stretch" vectors in the normed space. The theorem is saying that the identity map, which doesn't stretch vectors at all, has norm `1`.
More concisely: In a non-trivial normed space, the norm of the identity map is equal to 1.
|
LinearMap.bound_of_ball_bound
theorem LinearMap.bound_of_ball_bound :
β {π : Type u_1} {E : Type u_4} {Fβ : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup Fβ]
[inst_2 : NontriviallyNormedField π] [inst_3 : NormedSpace π E] [inst_4 : NormedSpace π Fβ] {r : β},
0 < r β β (c : β) (f : E ββ[π] Fβ), (β z β Metric.ball 0 r, βf zβ β€ c) β β C, β (z : E), βf zβ β€ C * βzβ
The theorem `LinearMap.bound_of_ball_bound` states that for any normed additive commutative groups `E` and `Fβ` over a nontrivially normed field `π`, given positive number `r`, another number `c`, and a linear map `f` from `E` to `Fβ`, if for all `z` in the open ball centered at 0 with radius `r`, the norm of `f(z)` is less than or equal to `c`, then there exists a constant `C` such that for all `z` in `E`, the norm of `f(z)` is less than or equal to `C` times the norm of `z`. In other words, if a linear map is bounded in some open ball around 0, it is bounded everywhere.
More concisely: If a linear map between normed additive commutative groups is bounded in some open ball, then it is uniformly continuous and therefore has a constant upper bound on the norm of the image for all inputs.
|
ContinuousLinearMap.op_norm_comp_linearIsometryEquiv
theorem ContinuousLinearMap.op_norm_comp_linearIsometryEquiv :
β {πβ : Type u_2} {πβ : Type u_3} {F : Type u_6} {G : Type u_8} [inst : NormedAddCommGroup F]
[inst_1 : NormedAddCommGroup G] [inst_2 : NontriviallyNormedField πβ] [inst_3 : NontriviallyNormedField πβ]
[inst_4 : NormedSpace πβ F] [inst_5 : NormedSpace πβ G] {Οββ : πβ β+* πβ} {πβ' : Type u_11}
[inst_6 : NontriviallyNormedField πβ'] {F' : Type u_12} [inst_7 : NormedAddCommGroup F']
[inst_8 : NormedSpace πβ' F'] {Οβ' : πβ' β+* πβ} {Οβ'' : πβ β+* πβ'} {Οββ' : πβ' β+* πβ}
[inst_9 : RingHomInvPair Οβ' Οβ''] [inst_10 : RingHomInvPair Οβ'' Οβ'] [inst_11 : RingHomCompTriple Οβ' Οββ Οββ']
[inst_12 : RingHomCompTriple Οβ'' Οββ' Οββ] [inst_13 : RingHomIsometric Οββ] [inst_14 : RingHomIsometric Οβ']
[inst_15 : RingHomIsometric Οβ''] [inst_16 : RingHomIsometric Οββ'] (f : F βSL[Οββ] G) (g : F' βββα΅’[Οβ'] F),
βf.comp g.toLinearIsometry.toContinuousLinearMapβ = βfβ
This theorem, named `ContinuousLinearMap.op_norm_comp_linearIsometryEquiv`, states that for a continuous linear map `f` and a linear isometry `g`, the operator norm of the composition of `f` and `g` is equal to the operator norm of `f`. This means that pre-composing with a linear isometry does not change the operator norm. This is true in the setting where `F`, `F'`, and `G` are normed add commutative groups over normed fields `πβ`, `πβ'`, and `πβ` and under certain restrictions on ring homomorphisms between these fields. The operator norm, designated by `β...β`, measures the "size" of a linear map in terms of its maximum amplification of input vectors.
More concisely: The operator norm of the composition of a continuous linear map and a linear isometry is equal to the operator norm of the linear map.
|
ContinuousLinearMap.op_norm_zero_iff
theorem ContinuousLinearMap.op_norm_zero_iff :
β {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField π] [inst_3 : NontriviallyNormedField πβ]
[inst_4 : NormedSpace π E] [inst_5 : NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F)
[inst_6 : RingHomIsometric Οββ], βfβ = 0 β f = 0
This theorem asserts that for a continuous linear map `f` from one normed space `E` to another normed space `F`, both the norm of `f` being zero and `f` being the zero map are equivalent conditions. This is under the context that `E` and `F` are normed additive commutative groups over nontrivially normed fields `π` and `πβ` respectively. The mapping from `π` to `πβ` is given by the ring homomorphism `Οββ` which is assumed to be isometric.
More concisely: A continuous linear map `f` from normed space `E` to normed space `F` over fields `π` and `πβ` with isometric ring homomorphism `Οββ` from `π` to `πβ` has zero norm if and only if it is the zero map.
|
ContinuousLinearMap.nnnorm_smulRight_apply
theorem ContinuousLinearMap.nnnorm_smulRight_apply :
β {π : Type u_1} {E : Type u_4} {Fβ : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup Fβ]
[inst_2 : NontriviallyNormedField π] [inst_3 : NormedSpace π E] [inst_4 : NormedSpace π Fβ] (c : E βL[π] π)
(f : Fβ), βc.smulRight fββ = βcββ * βfββ
This theorem states that for any scalar linear map 'c' and any element 'f' of a normed space, the non-negative norm of the tensor product of 'c' and 'f', denoted as βc.smulRight fββ, equals the product of the non-negative norms of 'c' and 'f', denoted as βcββ * βfββ. The types π, E, and Fβ are such that π is a nontrivially normed field and E and Fβ are normed additive commutative groups over which π is a normed space.
More concisely: For any scalar linear map 'c' and element 'f' in normed spaces E and F over a nontrivially normed field π, βc.smulRight fββ = βcββ * βfββ.
|