Formally self-adjoint partial linear maps and their shifts #
For a formally self-adjoint partial linear map A on an inner-product space over an RCLike
field π (Mathlib's LinearPMap.IsFormalAdjoint A A, the symmetric operators), the quadratic
form βͺx, A xβ« is real, so for a scalar c the shift x β¦ c β’ x - A x satisfies
βc β’ x - A xβΒ² = (im c)Β² βxβΒ² + βre c β’ x - A xβΒ².
For im c β 0 the shift is therefore bounded below with respect to the graph norm of A; if A is
closed, its range is closed (LinearPMap.isClosed_range_smul_sub_of_graph_norm_le). When A is
self-adjoint the range is also dense, because a vector orthogonal to it is an eigenvector of Aβ
for the eigenvalue conj c (LinearPMap.exists_adjoint_apply_eq_of_inner_smul_sub_eq_zero), and a
symmetric operator has no nonreal eigenvalue
(LinearPMap.IsFormalAdjoint.eq_zero_of_apply_eq_smul). Hence every nonreal shift of a
self-adjoint operator is surjective (IsSelfAdjoint.smul_sub_surjective), and with the lower bound
it is bijective with bounded inverse (IsSelfAdjoint.smul_sub_bijective): the resolvent set
contains every nonreal point. The shifts Β± i - A are the classical deficiency operators, and
their surjectivity is the range condition that makes Β± i β’ A m-dissipative.
The file also provides the formal-adjointness and quadratic-form API of self-adjoint partial linear maps used by the semigroup development.
Main results #
IsSelfAdjoint.isFormalAdjoint: a self-adjoint partial linear map is formally self-adjoint.LinearPMap.IsFormalAdjoint.im_inner_self_apply: the quadratic form of a formally self-adjoint map is real.LinearPMap.IsFormalAdjoint.norm_smul_sub_sq: the square-sum identity for a shift, and the graph-norm lower boundsabs_im_mul_norm_le_norm_smul_sub(equivalently the resolvent boundnorm_le_inv_abs_im_mul_norm_smul_sub) andnorm_apply_le_mul_norm_smul_sub.LinearPMap.IsFormalAdjoint.eq_zero_of_apply_eq_smul: a formally self-adjoint map has no eigenvector for a nonreal eigenvalue.LinearPMap.exists_adjoint_apply_eq_of_inner_smul_sub_eq_zero: a vector orthogonal to the range of the shiftc β’ x - A xis an eigenvector of the adjointAβfor the eigenvalueconj c.LinearPMap.IsFormalAdjoint.isClosed_range_smul_sub,IsSelfAdjoint.denseRange_smul_subandIsSelfAdjoint.smul_sub_surjective: the range of a nonreal shift is closed (closed symmetric operator), dense and the whole space (self-adjoint operator).LinearPMap.IsFormalAdjoint.smul_sub_injectiveandIsSelfAdjoint.smul_sub_bijective: a nonreal shift is injective, and bijective for a self-adjoint operator.LinearPMap.adjoint_smul: the adjoint of a nonzero scalar multiple is the conjugate multiple of the adjoint;dense_domain_of_adjoint_eq_negandisSelfAdjoint_smul_of_adjoint_eq_neg: a skew-adjoint partial linear map has dense domain, and its multiple by a nonzero purely imaginary scalar is self-adjoint.
References #
- M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Theorem VIII.3 (the basic criterion for self-adjointness).
- J. Weidmann, Linear Operators in Hilbert Spaces, Chapter 5.
A self-adjoint partial linear map is formally self-adjoint on its domain.
The quadratic form of a formally self-adjoint partial linear map is real.
Deficiency vectors are adjoint eigenvectors. A vector orthogonal to the range of the shift
c β’ x - A x of a densely defined partial linear map lies in the domain of the adjoint Aβ , which
acts on it as multiplication by conj c.
For a formally self-adjoint partial linear map, the real cross term between c β’ x and A x
is re c times the (real) quadratic form. The inner product is conjugate-linear in its first
argument.
The mirror image of re_inner_smul_self_apply: the real cross term between c β’ A x and x
is re c times the quadratic form.
Square-sum identity for shifts. For a formally self-adjoint partial linear map and a scalar
c, βc β’ x - A xβΒ² = (im c)Β² βxβΒ² + βre c β’ x - A xβΒ².
A shift dominates the imaginary part of the scalar times the input.
The resolvent bound: a nonreal shift of a formally self-adjoint partial linear map dominates
|im c| times the input, so its inverse (where defined) has norm at most |im c|β»ΒΉ.
A nonreal shift of a formally self-adjoint partial linear map is injective.
A shift dominates the shift by the real part of the scalar.
A nonreal shift dominates the image, up to the constant 1 + |re c| / |im c|: together with
abs_im_mul_norm_le_norm_smul_sub this bounds the graph norm max βxβ βA xβ by the shift.
The range of a nonreal shift of a closed, formally self-adjoint partial linear map is closed:
the shift is bounded below with respect to the graph norm
(LinearPMap.isClosed_range_smul_sub_of_graph_norm_le).
A symmetric operator has no nonreal eigenvalue: the quadratic form at an eigenvector for
c is c * βxβΒ², whose imaginary part vanishes only if x = 0.
The range of a nonreal shift of a self-adjoint partial linear map is dense.
Nonreal shifts of a self-adjoint partial linear map are surjective: their ranges are closed and dense.
Nonreal shifts of a self-adjoint partial linear map are bijective. Together with the lower
bound IsFormalAdjoint.abs_im_mul_norm_le_norm_smul_sub, which bounds the inverse by
|im c|β»ΒΉ, this says that the resolvent set of a self-adjoint operator contains every nonreal
point.
The adjoint of a scalar multiple. For a densely defined partial linear map T and a nonzero
scalar c, (c β’ T)β = conj c β’ Tβ ; in particular the two adjoints have the same domain.
A partial linear map whose adjoint is its negative has dense domain: otherwise the adjoint is
the junk value 0, so the map vanishes and every vector lies in the adjoint domain.
A skew-adjoint map times a nonzero purely imaginary scalar is self-adjoint: if Gβ = -G
and re c = 0, c β 0, then c β’ G is self-adjoint. At c = Β± i this recovers the self-adjoint
operator behind a skew-adjoint generator.