Documentation

Mathlib.Analysis.InnerProductSpace.LinearPMap

Partially defined linear operators on Hilbert spaces #

We will develop the basics of the theory of unbounded operators on Hilbert spaces.

Main definitions #

Main statements #

Notation #

Implementation notes #

We use the junk value pattern to define the adjoint for all LinearPMaps. In the case that T : E →ₗ.[𝕜] F is not densely defined the adjoint T† is the zero map from T.adjoint.domain to E.

References #

Tags #

Unbounded operators, closed operators

def LinearPMap.IsFormalAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) (S : F →ₗ.[𝕜] E) :

An operator T is a formal adjoint of S if for all x in the domain of T and y in the domain of S, we have that ⟪T x, y⟫ = ⟪x, S y⟫.

Equations
  • T.IsFormalAdjoint S = ∀ (x : T.domain) (y : S.domain), T x, y⟫_𝕜 = x, S y⟫_𝕜
Instances For
    theorem LinearPMap.IsFormalAdjoint.symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} {S : F →ₗ.[𝕜] E} (h : T.IsFormalAdjoint S) :
    S.IsFormalAdjoint T
    def LinearPMap.adjointDomain {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) :
    Submodule 𝕜 F

    The domain of the adjoint operator.

    This definition is needed to construct the adjoint operator and the preferred version to use is T.adjoint.domain instead of T.adjointDomain.

    Equations
    • T.adjointDomain = { carrier := {y : F | Continuous ((innerₛₗ 𝕜) y ∘ₗ T.toFun)}, add_mem' := , zero_mem' := , smul_mem' := }
    Instances For
      def LinearPMap.adjointDomainMkCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) (y : T.adjointDomain) :
      T.domain →L[𝕜] 𝕜

      The operator fun x ↦ ⟪y, T x⟫ considered as a continuous linear operator from T.adjointDomain to 𝕜.

      Equations
      • T.adjointDomainMkCLM y = { toLinearMap := (innerₛₗ 𝕜) y ∘ₗ T.toFun, cont := }
      Instances For
        theorem LinearPMap.adjointDomainMkCLM_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) (y : T.adjointDomain) (x : T.domain) :
        (T.adjointDomainMkCLM y) x = y, T x⟫_𝕜
        def LinearPMap.adjointDomainMkCLMExtend {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) (y : T.adjointDomain) :
        E →L[𝕜] 𝕜

        The unique continuous extension of the operator adjointDomainMkCLM to E.

        Equations
        Instances For
          @[simp]
          theorem LinearPMap.adjointDomainMkCLMExtend_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) (y : T.adjointDomain) (x : T.domain) :
          (LinearPMap.adjointDomainMkCLMExtend hT y) x = y, T x⟫_𝕜
          def LinearPMap.adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [CompleteSpace E] :
          T.adjointDomain →ₗ[𝕜] E

          The adjoint as a linear map from its domain to E.

          This is an auxiliary definition needed to define the adjoint operator as a LinearPMap without the assumption that T.domain is dense.

          Equations
          Instances For
            theorem LinearPMap.adjointAux_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [CompleteSpace E] (y : T.adjointDomain) (x : T.domain) :
            (LinearPMap.adjointAux hT) y, x⟫_𝕜 = y, T x⟫_𝕜
            theorem LinearPMap.adjointAux_unique {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [CompleteSpace E] (y : T.adjointDomain) {x₀ : E} (hx₀ : ∀ (x : T.domain), x₀, x⟫_𝕜 = y, T x⟫_𝕜) :
            def LinearPMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) [CompleteSpace E] :
            F →ₗ.[𝕜] E

            The adjoint operator as a partially defined linear operator.

            Equations
            Instances For
              theorem LinearPMap.mem_adjoint_domain_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F) [CompleteSpace E] (y : F) :
              y T.adjoint.domain Continuous ((innerₛₗ 𝕜) y ∘ₗ T.toFun)
              theorem LinearPMap.mem_adjoint_domain_of_exists {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} [CompleteSpace E] (y : F) (h : ∃ (w : E), ∀ (x : T.domain), w, x⟫_𝕜 = y, T x⟫_𝕜) :
              y T.adjoint.domain
              theorem LinearPMap.adjoint_apply_of_not_dense {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} [CompleteSpace E] (hT : ¬Dense T.domain) (y : T.adjoint.domain) :
              T.adjoint y = 0
              theorem LinearPMap.adjoint_apply_of_dense {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [CompleteSpace E] (y : T.adjoint.domain) :
              T.adjoint y = (LinearPMap.adjointAux hT) y
              theorem LinearPMap.adjoint_apply_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [CompleteSpace E] (y : T.adjoint.domain) {x₀ : E} (hx₀ : ∀ (x : T.domain), x₀, x⟫_𝕜 = y, T x⟫_𝕜) :
              T.adjoint y = x₀
              theorem LinearPMap.adjoint_isFormalAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} (hT : Dense T.domain) [CompleteSpace E] :
              T.adjoint.IsFormalAdjoint T

              The fundamental property of the adjoint.

              theorem LinearPMap.IsFormalAdjoint.le_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F} {S : F →ₗ.[𝕜] E} (hT : Dense T.domain) [CompleteSpace E] (h : T.IsFormalAdjoint S) :
              S T.adjoint

              The adjoint is maximal in the sense that it contains every formal adjoint.

              theorem ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) {p : Submodule 𝕜 E} (hp : Dense p) :
              ((A).toPMap p).adjoint = ((ContinuousLinearMap.adjoint A)).toPMap

              Restricting A to a dense submodule and taking the LinearPMap.adjoint is the same as taking the ContinuousLinearMap.adjoint interpreted as a LinearPMap.

              instance LinearPMap.instStar {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :
              Star (E →ₗ.[𝕜] E)
              Equations
              • LinearPMap.instStar = { star := fun (A : E →ₗ.[𝕜] E) => A.adjoint }
              theorem LinearPMap.isSelfAdjoint_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →ₗ.[𝕜] E} :
              IsSelfAdjoint A A.adjoint = A
              theorem IsSelfAdjoint.dense_domain {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) :
              Dense A.domain

              Every self-adjoint LinearPMap has dense domain.

              This is not true by definition since we define the adjoint without the assumption that the domain is dense, but the choice of the junk value implies that a LinearPMap cannot be self-adjoint if it does not have dense domain.