Documentation

Mathlib.Analysis.NormedSpace.Extend

Extending a continuous -linear map to a continuous 𝕜-linear map #

In this file we provide a way to extend a continuous -linear map to a continuous 𝕜-linear map in a way that bounds the norm by the norm of the original map, when 𝕜 is either (the extension is trivial) or . We formulate the extension uniformly, by assuming RCLike 𝕜.

We motivate the form of the extension as follows. Note that fc : F →ₗ[𝕜] 𝕜 is determined fully by re fc: for all x : F, fc (I • x) = I * fc x, so im (fc x) = -re (fc (I • x)). Therefore, given an fr : F →ₗ[ℝ] ℝ, we define fc x = fr x - fr (I • x) * I.

Main definitions #

Implementation details #

For convenience, the main definitions above operate in terms of RestrictScalars ℝ 𝕜 F. Alternate forms which operate on [IsScalarTower ℝ 𝕜 F] instead are provided with a primed name.

noncomputable def LinearMap.extendTo𝕜' {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Module F] [IsScalarTower 𝕜 F] (fr : F →ₗ[] ) :
F →ₗ[𝕜] 𝕜

Extend fr : F →ₗ[ℝ] ℝ to F →ₗ[𝕜] 𝕜 in a way that will also be continuous and have its norm bounded by ‖fr‖ if fr is continuous.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem LinearMap.extendTo𝕜'_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Module F] [IsScalarTower 𝕜 F] (fr : F →ₗ[] ) (x : F) :
    fr.extendTo𝕜' x = (fr x) - RCLike.I * (fr (RCLike.I x))
    @[simp]
    theorem LinearMap.extendTo𝕜'_apply_re {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Module F] [IsScalarTower 𝕜 F] (fr : F →ₗ[] ) (x : F) :
    RCLike.re (fr.extendTo𝕜' x) = fr x
    theorem LinearMap.norm_extendTo𝕜'_apply_sq {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [Module F] [IsScalarTower 𝕜 F] (fr : F →ₗ[] ) (x : F) :
    fr.extendTo𝕜' x ^ 2 = fr ((starRingEnd 𝕜) (fr.extendTo𝕜' x) x)
    theorem ContinuousLinearMap.norm_extendTo𝕜'_bound {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace F] [IsScalarTower 𝕜 F] (fr : F →L[] ) (x : F) :
    fr.extendTo𝕜' x fr * x

    The norm of the extension is bounded by ‖fr‖.

    noncomputable def ContinuousLinearMap.extendTo𝕜' {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace F] [IsScalarTower 𝕜 F] (fr : F →L[] ) :
    F →L[𝕜] 𝕜

    Extend fr : F →L[ℝ] ℝ to F →L[𝕜] 𝕜.

    Equations
    • fr.extendTo𝕜' = fr.extendTo𝕜'.mkContinuous fr
    Instances For
      theorem ContinuousLinearMap.extendTo𝕜'_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace F] [IsScalarTower 𝕜 F] (fr : F →L[] ) (x : F) :
      fr.extendTo𝕜' x = (fr x) - RCLike.I * (fr (RCLike.I x))
      @[simp]
      theorem ContinuousLinearMap.norm_extendTo𝕜' {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace F] [IsScalarTower 𝕜 F] (fr : F →L[] ) :
      fr.extendTo𝕜' = fr
      instance instNormedSpaceRestrictScalarsReal {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :
      Equations
      • instNormedSpaceRestrictScalarsReal = id inferInstance
      noncomputable def LinearMap.extendTo𝕜 {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : RestrictScalars 𝕜 F →ₗ[] ) :
      F →ₗ[𝕜] 𝕜

      Extend fr : RestrictScalars ℝ 𝕜 F →ₗ[ℝ] ℝ to F →ₗ[𝕜] 𝕜.

      Equations
      • fr.extendTo𝕜 = fr.extendTo𝕜'
      Instances For
        theorem LinearMap.extendTo𝕜_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : RestrictScalars 𝕜 F →ₗ[] ) (x : F) :
        fr.extendTo𝕜 x = (fr x) - RCLike.I * (fr (RCLike.I x))
        noncomputable def ContinuousLinearMap.extendTo𝕜 {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : RestrictScalars 𝕜 F →L[] ) :
        F →L[𝕜] 𝕜

        Extend fr : RestrictScalars ℝ 𝕜 F →L[ℝ] ℝ to F →L[𝕜] 𝕜.

        Equations
        • fr.extendTo𝕜 = fr.extendTo𝕜'
        Instances For
          theorem ContinuousLinearMap.extendTo𝕜_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : RestrictScalars 𝕜 F →L[] ) (x : F) :
          fr.extendTo𝕜 x = (fr x) - RCLike.I * (fr (RCLike.I x))
          @[simp]
          theorem ContinuousLinearMap.norm_extendTo𝕜 {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : RestrictScalars 𝕜 F →L[] ) :
          fr.extendTo𝕜 = fr