Skew multiples of self-adjoint operators are m-dissipative

Multiplication by a nonzero purely imaginary scalar c turns a self-adjoint partial linear map A on a complex Hilbert space into an m-dissipative real partial linear map: the quadratic form of c • A is purely imaginary, so its real restriction is dissipative, and the range condition, surjectivity of 1 - c • A, is the surjectivity of the nonreal shift c⁻¹ - A of A, since 1 - c • A = c • (c⁻¹ - A). Together with the density of the domain of a self-adjoint operator (IsSelfAdjoint.dense_domain), this is the hypothesis set of the Lumer--Phillips theorem; at c = ± i it produces the two contraction semigroups whose gluing is the unitary group e^{itA}.

Main results

• LinearPMap.IsFormalAdjoint.isDissipative_smul_restrictScalars: for a symmetric A and a purely imaginary c, the real restriction of c • A is dissipative.
• IsSelfAdjoint.one_smul_sub_smul_restrictScalars_surjective: for self-adjoint A and nonreal c, 1 - c • A is surjective.
• IsSelfAdjoint.isMDissipative_smul_restrictScalars: for self-adjoint A and a nonzero purely imaginary c, the real restriction of c • A is m-dissipative.

The statements are in the simp-normal form c • A.restrictScalars ℝ of LinearPMap.restrictScalars_smul.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Theorem II.3.24 (Stone's theorem) and the surrounding discussion.
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Theorem 1.10.8.

theorem LinearPMap.IsFormalAdjoint.isDissipative_smul_restrictScalars {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {A : E →ₗ.[ℂ] E} (hA : A.IsFormalAdjoint A) {c : ℂ} (hc : c.re = 0) : TauCeti.Semigroups.IsDissipative (c • restrictScalars ℝ A)

The real restriction of a purely imaginary multiple of a formally self-adjoint (symmetric) partial linear map is dissipative: its real quadratic form vanishes.

theorem IsSelfAdjoint.one_smul_sub_smul_restrictScalars_surjective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {A : E →ₗ.[ℂ] E} (hA : IsSelfAdjoint A) {c : ℂ} (hc : c.im ≠ 0) : Function.Surjective fun (x : ↥(c • LinearPMap.restrictScalars ℝ A).domain) => 1 • ↑x - ↑(c • LinearPMap.restrictScalars ℝ A) x

The range condition for a nonreal multiple c • A of a self-adjoint partial linear map: 1 - c • A = c • (c⁻¹ - A) is surjective because the nonreal shift c⁻¹ - A is.

theorem IsSelfAdjoint.isMDissipative_smul_restrictScalars {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {A : E →ₗ.[ℂ] E} (hA : IsSelfAdjoint A) {c : ℂ} (hc : c.re = 0) (hc0 : c ≠ 0) : TauCeti.Semigroups.IsMDissipative (c • LinearPMap.restrictScalars ℝ A)

c • A is m-dissipative for self-adjoint A and nonzero purely imaginary c. The real restriction of c • A is dissipative, because its quadratic form is purely imaginary, and 1 - c • A is surjective, because the nonreal shift c⁻¹ - A is.