Documentation

Mathlib.Analysis.NormedSpace.OperatorNorm.Mul

Results about operator norms in normed algebras #

This file (split off from OperatorNorm.lean) contains results about the operator norm of multiplication and scalar-multiplication operations in normed algebras and normed modules.

noncomputable def ContinuousLinearMap.mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] :
𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

Multiplication in a non-unital normed algebra as a continuous bilinear map.

Equations
Instances For
    @[simp]
    theorem ContinuousLinearMap.mul_apply' (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') :
    ((ContinuousLinearMap.mul 𝕜 𝕜') x) y = x * y
    @[simp]
    theorem ContinuousLinearMap.opNorm_mul_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') :
    @[deprecated ContinuousLinearMap.opNorm_mul_apply_le]
    theorem ContinuousLinearMap.op_norm_mul_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') :

    Alias of ContinuousLinearMap.opNorm_mul_apply_le.

    theorem ContinuousLinearMap.opNorm_mul_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] :
    @[deprecated ContinuousLinearMap.opNorm_mul_le]
    theorem ContinuousLinearMap.op_norm_mul_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] :

    Alias of ContinuousLinearMap.opNorm_mul_le.

    noncomputable def NonUnitalAlgHom.Lmul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] :
    𝕜' →ₙₐ[𝕜] 𝕜' →L[𝕜] 𝕜'

    Multiplication on the left in a non-unital normed algebra 𝕜' as a non-unital algebra homomorphism into the algebra of continuous linear maps. This is the left regular representation of A acting on itself.

    This has more algebraic structure than ContinuousLinearMap.mul, but there is no longer continuity bundled in the first coordinate. An alternative viewpoint is that this upgrades NonUnitalAlgHom.lmul from a homomorphism into linear maps to a homomorphism into continuous linear maps.

    Equations
    Instances For
      @[simp]
      theorem NonUnitalAlgHom.coe_Lmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_3} [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] :
      (NonUnitalAlgHom.Lmul 𝕜 𝕜') = (ContinuousLinearMap.mul 𝕜 𝕜')
      noncomputable def ContinuousLinearMap.mulLeftRight (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] :
      𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

      Simultaneous left- and right-multiplication in a non-unital normed algebra, considered as a continuous trilinear map. This is akin to its non-continuous version LinearMap.mulLeftRight, but there is a minor difference: LinearMap.mulLeftRight is uncurried.

      Equations
      Instances For
        @[simp]
        theorem ContinuousLinearMap.mulLeftRight_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') (z : 𝕜') :
        (((ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x) y) z = x * z * y
        theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') :
        @[deprecated ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le]
        theorem ContinuousLinearMap.op_norm_mulLeftRight_apply_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') :

        Alias of ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le.

        theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') :
        @[deprecated ContinuousLinearMap.opNorm_mulLeftRight_apply_le]
        theorem ContinuousLinearMap.op_norm_mulLeftRight_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') :

        Alias of ContinuousLinearMap.opNorm_mulLeftRight_apply_le.

        theorem ContinuousLinearMap.opNorm_mulLeftRight_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] :
        @[deprecated ContinuousLinearMap.opNorm_mulLeftRight_le]
        theorem ContinuousLinearMap.op_norm_mulLeftRight_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] :

        Alias of ContinuousLinearMap.opNorm_mulLeftRight_le.

        class RegularNormedAlgebra (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] :

        This is a mixin class for non-unital normed algebras which states that the left-regular representation of the algebra on itself is isometric. Every unital normed algebra with ‖1‖ = 1 is a regular normed algebra (see NormedAlgebra.instRegularNormedAlgebra). In addition, so is every C⋆-algebra, non-unital included (see CStarRing.instRegularNormedAlgebra), but there are yet other examples. Any algebra with an approximate identity (e.g., $$L^1$$) is also regular.

        This is a useful class because it gives rise to a nice norm on the unitization; in particular it is a C⋆-norm when the norm on A is a C⋆-norm.

        Instances
          theorem RegularNormedAlgebra.isometry_mul' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_3} [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [self : RegularNormedAlgebra 𝕜 𝕜'] :

          The left regular representation of the algebra on itself is an isometry.

          noncomputable instance NormedAlgebra.instRegularNormedAlgebra {𝕜 : Type u_4} {𝕜' : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] :

          Every (unital) normed algebra such that ‖1‖ = 1 is a RegularNormedAlgebra.

          Equations
          • =
          theorem ContinuousLinearMap.isometry_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] :
          @[simp]
          theorem ContinuousLinearMap.opNorm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] (x : 𝕜') :
          @[deprecated ContinuousLinearMap.opNorm_mul_apply]
          theorem ContinuousLinearMap.op_norm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] (x : 𝕜') :

          Alias of ContinuousLinearMap.opNorm_mul_apply.

          @[simp]
          theorem ContinuousLinearMap.opNNNorm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] (x : 𝕜') :
          @[deprecated ContinuousLinearMap.opNNNorm_mul_apply]
          theorem ContinuousLinearMap.op_nnnorm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] (x : 𝕜') :

          Alias of ContinuousLinearMap.opNNNorm_mul_apply.

          noncomputable def ContinuousLinearMap.mulₗᵢ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] :
          𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜'

          Multiplication in a normed algebra as a linear isometry to the space of continuous linear maps.

          Equations
          Instances For
            @[simp]
            theorem ContinuousLinearMap.coe_mulₗᵢ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] :
            noncomputable def ContinuousLinearMap.ring_lmap_equiv_selfₗ (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
            (𝕜 →L[𝕜] E) ≃ₗ[𝕜] E

            If M is a normed space over 𝕜, then the space of maps 𝕜 →L[𝕜] M is linearly equivalent to M. (See ring_lmap_equiv_self for a stronger statement.)

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def ContinuousLinearMap.ring_lmap_equiv_self (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
              (𝕜 →L[𝕜] E) ≃ₗᵢ[𝕜] E

              If M is a normed space over 𝕜, then the space of maps 𝕜 →L[𝕜] M is linearly isometrically equivalent to M.

              Equations
              Instances For
                noncomputable def ContinuousLinearMap.lsmul (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (𝕜' : Type u_3) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :
                𝕜' →L[𝕜] E →L[𝕜] E

                Scalar multiplication as a continuous bilinear map.

                Equations
                Instances For
                  @[simp]
                  theorem ContinuousLinearMap.lsmul_apply (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (𝕜' : Type u_3) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (c : 𝕜') (x : E) :
                  ((ContinuousLinearMap.lsmul 𝕜 𝕜') c) x = c x
                  theorem ContinuousLinearMap.opNorm_lsmul_apply_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_3} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (x : 𝕜') :
                  @[deprecated ContinuousLinearMap.opNorm_lsmul_apply_le]
                  theorem ContinuousLinearMap.op_norm_lsmul_apply_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_3} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (x : 𝕜') :

                  Alias of ContinuousLinearMap.opNorm_lsmul_apply_le.

                  theorem ContinuousLinearMap.opNorm_lsmul_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_3} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :

                  The norm of lsmul is at most 1 in any semi-normed group.

                  @[deprecated ContinuousLinearMap.opNorm_lsmul_le]
                  theorem ContinuousLinearMap.op_norm_lsmul_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_3} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :

                  Alias of ContinuousLinearMap.opNorm_lsmul_le.


                  The norm of lsmul is at most 1 in any semi-normed group.

                  @[simp]
                  theorem ContinuousLinearMap.opNorm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] :
                  @[deprecated ContinuousLinearMap.opNorm_mul]
                  theorem ContinuousLinearMap.op_norm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] :

                  Alias of ContinuousLinearMap.opNorm_mul.

                  @[simp]
                  theorem ContinuousLinearMap.opNNNorm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] :
                  @[deprecated ContinuousLinearMap.opNNNorm_mul]
                  theorem ContinuousLinearMap.op_nnnorm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] :

                  Alias of ContinuousLinearMap.opNNNorm_mul.

                  @[simp]
                  theorem ContinuousLinearMap.opNorm_lsmul (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (𝕜' : Type u_3) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [Nontrivial E] :

                  The norm of lsmul equals 1 in any nontrivial normed group.

                  This is ContinuousLinearMap.opNorm_lsmul_le as an equality.

                  @[deprecated ContinuousLinearMap.opNorm_lsmul]
                  theorem ContinuousLinearMap.op_norm_lsmul (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (𝕜' : Type u_3) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [Nontrivial E] :

                  Alias of ContinuousLinearMap.opNorm_lsmul.


                  The norm of lsmul equals 1 in any nontrivial normed group.

                  This is ContinuousLinearMap.opNorm_lsmul_le as an equality.