ContinuousLinearMap.op_norm_lsmul
theorem ContinuousLinearMap.op_norm_lsmul :
β (π : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] (π' : Type u_3) [inst_3 : NormedField π'] [inst_4 : NormedAlgebra π π']
[inst_5 : NormedSpace π' E] [inst_6 : IsScalarTower π π' E] [inst_7 : Nontrivial E],
βContinuousLinearMap.lsmul π π'β = 1
This theorem states that for any given type π and type E (under the conditions that π is a non-trivially normed field, E is a normed additive commutative group, E is a normed space over π, and E is non-trivial), and for any additional type π' (under the conditions that π' is a normed field, E is a normed space over π', and π', π and E form a scalar tower), the operator norm of the left scalar multiplication continuous linear map from π to π' is equal to 1. In simpler terms, this theorem describes a property of scalar multiplication in certain mathematical structures, stating that when these conditions are met, the "size" (or norm) of the multiplication operation stays constant at 1.
More concisely: Given non-trivially normed fields π and π', a normed additive commutative group E that is a normed space over both π and π', and forms a scalar tower, the operator norm of the scalar multiplication map from π to π' is equal to 1.
|
ContinuousLinearMap.op_norm_lsmul_le
theorem ContinuousLinearMap.op_norm_lsmul_le :
β {π : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : SeminormedAddCommGroup E]
[inst_2 : NormedSpace π E] {π' : Type u_3} [inst_3 : NormedField π'] [inst_4 : NormedAlgebra π π']
[inst_5 : NormedSpace π' E] [inst_6 : IsScalarTower π π' E], βContinuousLinearMap.lsmul π π'β β€ 1
This theorem states that in any semi-normed group, the operator norm of the left scalar multiplication operator (`lsmul`) is at most 1. This is applicable for any non-trivially normed field `π`, any semi-normed add-commutative group `E` that is also a normed space over `π`, any normed field `π'` that is a normed algebra over `π` and a normed space over `π'`, and any scalar tower structure on `E` over `π` and `π'`.
More concisely: In any semi-normed group that is a normed space over a non-trivially normed field, the operator norm of the left scalar multiplication is bounded by 1.
|
RegularNormedAlgebra.isometry_mul'
theorem RegularNormedAlgebra.isometry_mul' :
β {π : Type u_1} [inst : NontriviallyNormedField π] {π' : Type u_3} [inst_1 : NonUnitalSeminormedRing π']
[inst_2 : NormedSpace π π'] [inst_3 : IsScalarTower π π' π'] [inst_4 : SMulCommClass π π' π']
[self : RegularNormedAlgebra π π'], Isometry β(ContinuousLinearMap.mul π π')
This theorem states that the left regular representation of an algebra on itself is an isometry. In other words, for any nontrivially normed field π and any non-unital seminormed ring π', given the circumstances where π' is a normed space over π, π is a scalar tower over π', and π and π' form a commutative multiplication class, and π' is a regular normed algebra over π, the continuous bilinear map representing multiplication in π' preserves the distance between elements when viewed as a function from π' to π'.
More concisely: The left regular representation of a regular normed algebra over a scalar tower preserves the distance between elements when viewed as a bilinear map from the algebra to the scalar field.
|