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} [AddCommGroup F] [Module ℝ 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
  • fr.extendTođť•ś' = { toFun := fun (x : F) => ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x)), map_add' := â‹Ż, map_smul' := â‹Ż }
Instances For
    theorem LinearMap.extendTo𝕜'_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ 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} [AddCommGroup F] [Module ℝ 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} [AddCommGroup F] [Module ℝ 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] :
      NormedSpace đť•ś (RestrictScalars â„ť đť•ś 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‖