Unitary strongly continuous groups

A strongly continuous group on a complex Hilbert space is represented by real continuous linear maps, in accordance with the real-Banach-first convention of the semigroup development. Such a group is unitary when every operator preserves the complex inner product. Inner-product preservation forces the real-linear operators to be complex-linear, and the same is true of the infinitesimal generator on its natural domain.

This file packages that complex generator without replacing the real generator: it is the complex generator of the forward semigroup from TauCeti.Analysis.Semigroups.Generator.ComplexLinear, which applies because a unitary group is complex linear (IsUnitary.isComplexLinear). Its domain has the same carrier as TauCeti.Semigroups.StronglyContinuousGroup.domain, now regarded as a complex submodule, and its values are exactly those of the existing generator. Differentiating preservation of the inner product gives the infinitesimal unitary identity

⟪A x, y⟫ = -⟪x, A y⟫.

The resolvent-range theorems for the forward and reversed contraction semigroups then identify the adjoint domain and upgrade this identity to A† = -A: the generator is skew-adjoint. This completes the generator direction of Stone's theorem; the converse construction is in TauCeti.Analysis.Semigroups.Group.Stone.Unbounded.

Main declarations

• TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary: every group operator preserves the complex inner product.
• TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.map_smul and TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.isComplexLinear: a unitary group represented real-linearly is automatically complex-linear, and so is its forward semigroup.
• TauCeti.Semigroups.StronglyContinuousGroup.complexDomain: the generator domain as a complex submodule.
• TauCeti.Semigroups.StronglyContinuousGroup.complexGenerator: the generator as a complex LinearPMap.
• TauCeti.Semigroups.StronglyContinuousGroup.isUnitary_of_isComplexLinear_of_opNorm_le_one: a contractive C₀-group whose forward semigroup is complex linear is unitary; isUnitary_toGroupOfInverse: a complex-linear contraction semigroup and an inverse contraction semigroup glue into a unitary group.
• TauCeti.Semigroups.StronglyContinuousGroup.complexGenerator_restrictScalars, complexGenerator_eq_of_generator_eq_restrictScalars and eq_of_complexGenerator_eq: the real generator is the real restriction of the complex one, which is therefore determined by the real generator and determines the unitary group.
• TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.complexGenerator_isFormalAdjoint_neg: the generator is skew-symmetric.
• TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.complexGenerator_adjoint_eq_neg: the generator is skew-adjoint.

References

• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Theorem VIII.8.
• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.3.11.
• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part A (C₀-groups and Stone's theorem stretch target).

def TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) : Prop

A strongly continuous group on a complex Hilbert space is unitary when every operator preserves the complex inner product. Although the underlying group is represented by real-linear operators, this condition forces complex linearity; see IsUnitary.map_smul.

Equations

• U.IsUnitary = ∀ (t : ℝ) (x y : H), inner ℂ ((U t) x) ((U t) y) = inner ℂ x y

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.intro {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : ∀ (t : ℝ) (x y : H), inner ℂ ((U t) x) ((U t) y) = inner ℂ x y) : U.IsUnitary

Construct a unitary group from inner-product preservation by each of its operators.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.inner_map_map {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : U.IsUnitary) (t : ℝ) (x y : H) : inner ℂ ((U t) x) ((U t) y) = inner ℂ x y

Every operator of a unitary strongly continuous group preserves the complex inner product.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.norm_map {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : U.IsUnitary) (t : ℝ) (x : H) : ‖(U t) x‖ = ‖x‖

Every operator of a unitary strongly continuous group preserves norms.

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.isometry {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : U.IsUnitary) (t : ℝ) : Isometry ⇑(U t)

Every operator of a unitary strongly continuous group is an isometry.

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.opNorm_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : U.IsUnitary) (t : ℝ) : ‖U t‖ ≤ 1

Every operator of a unitary strongly continuous group has operator norm at most one.

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.hasGrowthBound_zero_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : U.IsUnitary) : U.HasGrowthBound 0 1

A unitary strongly continuous group has the sharp two-sided growth bound (0, 1).

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.reflect {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : U.IsUnitary) : U.reflect.IsUnitary

The time reversal of a unitary strongly continuous group is unitary.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.map_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : U.IsUnitary) (t : ℝ) (z : ℂ) (x : H) : (U t) (z • x) = z • (U t) x

Inner-product preservation forces every operator of a unitary strongly continuous group to be complex-linear, even though StronglyContinuousGroup represents it as a real-linear map.

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.isComplexLinear {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : U.IsUnitary) : U.toSemigroup.IsComplexLinear

The forward semigroup of a unitary strongly continuous group is complex linear.

theorem TauCeti.Semigroups.StronglyContinuousGroup.isUnitary_of_isComplexLinear_of_opNorm_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hlin : U.toSemigroup.IsComplexLinear) (h : ∀ (t : ℝ), ‖U t‖ ≤ 1) : U.IsUnitary

A contractive C₀-group whose forward semigroup is complex linear is unitary: complex linearity at negative times follows from that at nonnegative times through the group law.

theorem TauCeti.Semigroups.StronglyContinuousGroup.isUnitary_toGroupOfInverse {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (S T : ContractionSemigroup H) (hS : S.IsComplexLinear) (hST : ∀ (t : NNReal), S.toStronglyContinuousSemigroup t ∘SL T.toStronglyContinuousSemigroup t = ContinuousLinearMap.id ℝ H) (hTS : ∀ (t : NNReal), T.toStronglyContinuousSemigroup t ∘SL S.toStronglyContinuousSemigroup t = ContinuousLinearMap.id ℝ H) : (S.toGroupOfInverse T.toStronglyContinuousSemigroup hST hTS).IsUnitary

A complex-linear contraction semigroup and an inverse contraction semigroup glue into a unitary C₀-group (complex linearity of the inverse half follows from the group law).

noncomputable def TauCeti.Semigroups.StronglyContinuousGroup.complexDomain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) : Submodule ℂ H

The generator domain of a unitary strongly continuous group, regarded as a complex submodule: the complex generator domain of its forward semigroup. Its carrier is the real generator domain.

Equations

• U.complexDomain hU = U.toSemigroup.complexDomain ⋯

theorem TauCeti.Semigroups.StronglyContinuousGroup.complexDomain_def {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) : U.complexDomain hU = U.toSemigroup.complexDomain ⋯

The complex generator domain of a unitary group is that of its forward semigroup.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.mem_complexDomain_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) (x : H) : x ∈ U.complexDomain hU ↔ x ∈ U.domain

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.coe_complexDomain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) : ↑(U.complexDomain hU) = ↑U.domain

The complex generator domain has the real generator domain as its underlying set.

theorem TauCeti.Semigroups.StronglyContinuousGroup.dense_complexDomain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) : Dense ↑(U.complexDomain hU)

The generator domain of a unitary strongly continuous group is dense, also when regarded as a complex submodule.

noncomputable def TauCeti.Semigroups.StronglyContinuousGroup.complexGenerator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) : H →ₗ.[ℂ] H

The infinitesimal generator of a unitary strongly continuous group as a complex-linear partially defined map: the complex generator of its forward semigroup. It has the same domain and values as the existing real generator.

Equations

• U.complexGenerator hU = U.toSemigroup.complexGenerator ⋯

theorem TauCeti.Semigroups.StronglyContinuousGroup.complexGenerator_def {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) : U.complexGenerator hU = U.toSemigroup.complexGenerator ⋯

The complex generator of a unitary group is that of its forward semigroup.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.complexGenerator_domain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) : (U.complexGenerator hU).domain = U.complexDomain hU

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.complexGenerator_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) (x : ↥(U.complexGenerator hU).domain) : ↑(U.complexGenerator hU) x = ↑U.generator ⟨↑x, ⋯⟩

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.complexGenerator_restrictScalars {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) : LinearPMap.restrictScalars ℝ (U.complexGenerator hU) = U.generator

The real generator of a unitary C₀-group is the real restriction of its complex generator.

theorem TauCeti.Semigroups.StronglyContinuousGroup.complexGenerator_eq_of_generator_eq_restrictScalars {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : StronglyContinuousGroup H) (hU : U.IsUnitary) {A : H →ₗ.[ℂ] H} (hA : U.generator = LinearPMap.restrictScalars ℝ A) : U.complexGenerator hU = A

The complex generator of a unitary C₀-group whose real generator is the real restriction of the complex-linear partial map A is A itself.

theorem TauCeti.Semigroups.StronglyContinuousGroup.eq_of_complexGenerator_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U V : StronglyContinuousGroup H} (hU : U.IsUnitary) (hV : V.IsUnitary) (h : U.complexGenerator hU = V.complexGenerator hV) : U = V

A unitary C₀-group is determined by its complex generator.

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.inner_complexGenerator_eq_neg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : U.IsUnitary) (x y : ↥(U.complexGenerator hU).domain) : inner ℂ (↑(U.complexGenerator hU) x) ↑y = -inner ℂ (↑x) (↑(U.complexGenerator hU) y)

The infinitesimal generator of a unitary strongly continuous group is skew-symmetric. For vectors x and y in its natural complex domain, inner (A x) y = -inner x (A y).

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.complexGenerator_isFormalAdjoint_neg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} (hU : U.IsUnitary) : (U.complexGenerator hU).IsFormalAdjoint (-U.complexGenerator hU)

The complex generator of a unitary strongly continuous group is a formal adjoint of its negative, Mathlib's unbounded-operator formulation of skew-symmetry.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.complexGenerator_adjoint_eq_neg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : StronglyContinuousGroup H} [CompleteSpace H] (hU : U.IsUnitary) : (U.complexGenerator hU).adjoint = -U.complexGenerator hU

The infinitesimal generator of a unitary strongly continuous group is skew-adjoint. Its Hilbert-space adjoint is its negative. The reverse inclusion of adjoint domains uses the surjectivity of both 1 - A and 1 + A, supplied by the resolvents of the forward and reversed contraction semigroups.