Partially defined linear operators on Hilbert spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We will develop the basics of the theory of unbounded operators on Hilbert spaces.
Main definitions #
linear_pmap.is_formal_adjoint: An operatorTis a formal adjoint ofSif for allxin the domain ofTandyin the domain ofS, we have that⟪T x, y⟫ = ⟪x, S y⟫.linear_pmap.adjoint: The adjoint of a mapE →ₗ.[𝕜] Fas a mapF →ₗ.[𝕜] E.
Main statements #
linear_pmap.adjoint_is_formal_adjoint: The adjoint is a formal adjointlinear_pmap.is_formal_adjoint.le_adjoint: Every formal adjoint is contained in the adjointcontinuous_linear_map.to_pmap_adjoint_eq_adjoint_to_pmap_of_dense: The adjoint oncontinuous_linear_mapandlinear_pmapcoincide.
Notation #
- For
T : E →ₗ.[𝕜] Fthe adjoint can be written asT†. This notation is localized inlinear_pmap.
Implementation notes #
We use the junk value pattern to define the adjoint for all linear_pmaps. 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
linear_pmap.is_formal_adjoint
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
(T : E →ₗ.[𝕜] F)
(S : F →ₗ.[𝕜] E) :
Prop
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.is_formal_adjoint S = ∀ (x : ↥(T.domain)) (y : ↥(S.domain)), has_inner.inner (⇑T x) ↑y = has_inner.inner ↑x (⇑S y)
@[protected]
theorem
linear_pmap.is_formal_adjoint.symm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
{S : F →ₗ.[𝕜] E}
(h : T.is_formal_adjoint S) :
def
linear_pmap.adjoint_domain
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 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.adjoint_domain.
def
linear_pmap.adjoint_domain_mk_clm
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
(T : E →ₗ.[𝕜] F)
(y : ↥(T.adjoint_domain)) :
The operator λ x, ⟪y, T x⟫ considered as a continuous linear operator from T.adjoint_domain
to 𝕜.
Equations
- T.adjoint_domain_mk_clm y = {to_linear_map := (⇑(innerₛₗ 𝕜) ↑y).comp T.to_fun, cont := _}
theorem
linear_pmap.adjoint_domain_mk_clm_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
(T : E →ₗ.[𝕜] F)
(y : ↥(T.adjoint_domain))
(x : ↥(T.domain)) :
⇑(T.adjoint_domain_mk_clm y) x = has_inner.inner ↑y (⇑T x)
noncomputable
def
linear_pmap.adjoint_domain_mk_clm_extend
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
(hT : dense ↑(T.domain))
(y : ↥(T.adjoint_domain)) :
The unique continuous extension of the operator adjoint_domain_mk_clm to E.
Equations
- linear_pmap.adjoint_domain_mk_clm_extend hT y = (T.adjoint_domain_mk_clm y).extend T.domain.subtypeL _ linear_pmap.adjoint_domain_mk_clm_extend._proof_3
@[simp]
theorem
linear_pmap.adjoint_domain_mk_clm_extend_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
(hT : dense ↑(T.domain))
(y : ↥(T.adjoint_domain))
(x : ↥(T.domain)) :
⇑(linear_pmap.adjoint_domain_mk_clm_extend hT y) ↑x = has_inner.inner ↑y (⇑T x)
noncomputable
def
linear_pmap.adjoint_aux
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
(hT : dense ↑(T.domain))
[complete_space E] :
↥(T.adjoint_domain) →ₗ[𝕜] 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 linear_pmap without
the assumption that T.domain is dense.
Equations
- linear_pmap.adjoint_aux hT = {to_fun := λ (y : ↥(T.adjoint_domain)), ⇑((inner_product_space.to_dual 𝕜 E).symm) (linear_pmap.adjoint_domain_mk_clm_extend hT y), map_add' := _, map_smul' := _}
theorem
linear_pmap.adjoint_aux_inner
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
(hT : dense ↑(T.domain))
[complete_space E]
(y : ↥(T.adjoint_domain))
(x : ↥(T.domain)) :
has_inner.inner (⇑(linear_pmap.adjoint_aux hT) y) ↑x = has_inner.inner ↑y (⇑T x)
theorem
linear_pmap.adjoint_aux_unique
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
(hT : dense ↑(T.domain))
[complete_space E]
(y : ↥(T.adjoint_domain))
{x₀ : E}
(hx₀ : ∀ (x : ↥(T.domain)), has_inner.inner x₀ ↑x = has_inner.inner ↑y (⇑T x)) :
⇑(linear_pmap.adjoint_aux hT) y = x₀
noncomputable
def
linear_pmap.adjoint
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
(T : E →ₗ.[𝕜] F)
[complete_space E] :
The adjoint operator as a partially defined linear operator.
theorem
linear_pmap.mem_adjoint_domain_iff
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
(T : E →ₗ.[𝕜] F)
[complete_space E]
(y : F) :
theorem
linear_pmap.mem_adjoint_domain_of_exists
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
[complete_space E]
(y : F)
(h : ∃ (w : E), ∀ (x : ↥(T.domain)), has_inner.inner w ↑x = has_inner.inner y (⇑T x)) :
theorem
linear_pmap.adjoint_apply_of_not_dense
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
[complete_space E]
(hT : ¬dense ↑(T.domain))
(y : ↥(T.adjoint.domain)) :
theorem
linear_pmap.adjoint_apply_of_dense
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
(hT : dense ↑(T.domain))
[complete_space E]
(y : ↥(T.adjoint.domain)) :
⇑(T.adjoint) y = ⇑(linear_pmap.adjoint_aux hT) y
theorem
linear_pmap.adjoint_apply_eq
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
(hT : dense ↑(T.domain))
[complete_space E]
(y : ↥(T.adjoint.domain))
{x₀ : E}
(hx₀ : ∀ (x : ↥(T.domain)), has_inner.inner x₀ ↑x = has_inner.inner ↑y (⇑T x)) :
theorem
linear_pmap.adjoint_is_formal_adjoint
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
(hT : dense ↑(T.domain))
[complete_space E] :
The fundamental property of the adjoint.
theorem
linear_pmap.is_formal_adjoint.le_adjoint
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
{T : E →ₗ.[𝕜] F}
{S : F →ₗ.[𝕜] E}
(hT : dense ↑(T.domain))
[complete_space E]
(h : T.is_formal_adjoint S) :
The adjoint is maximal in the sense that it contains every formal adjoint.
theorem
continuous_linear_map.to_pmap_adjoint_eq_adjoint_to_pmap_of_dense
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[normed_add_comm_group F]
[inner_product_space 𝕜 F]
[complete_space E]
[complete_space F]
(A : E →L[𝕜] F)
{p : submodule 𝕜 E}
(hp : dense ↑p) :
Restricting A to a dense submodule and taking the linear_pmap.adjoint is the same
as taking the continuous_linear_map.adjoint interpreted as a linear_pmap.