Phase shifts of a complex-linear strongly continuous semigroup

For a C₀-semigroup S acting by complex-linear operators on a complex Banach space and a real number b, the phase shift is the semigroup

(S.phaseShift hS b) t = exp (-i b t) • S t.

Unlike the exponential shift t ↦ exp (-omega t) • S t of TauCeti/Analysis/Semigroups/ExponentialShift.lean, which damps the semigroup and moves its growth exponent, a phase shift multiplies by a unimodular scalar: it preserves every growth bound (omega, M) exactly, and it subtracts i b from the generator. Composing the two shifts realizes t ↦ exp (-lambda t) • S t for an arbitrary complex lambda.

This is the device that moves a spectral parameter parallel to the imaginary axis. Since the Laplace-transform resolvent of a C₀-semigroup is a real-variable construction, it only ever produces real points of the resolvent set; the phase shift converts a real point for the shifted semigroup into the point lambda = mu + i b for S, which is how the complex resolvent set of the complex generator is reached in TauCeti/Analysis/Semigroups/Resolvent/Complex.lean.

Main definitions and results

• TauCeti.Semigroups.StronglyContinuousSemigroup.phaseShift: the semigroup t ↦ exp (-i b t) • S t.
• TauCeti.Semigroups.StronglyContinuousSemigroup.IsComplexLinear.phaseShift and TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound.phaseShift: a phase shift is again complex linear, and has the same growth bounds.
• TauCeti.Semigroups.StronglyContinuousSemigroup.phaseShift_domain: a phase shift does not change the generator domain.
• TauCeti.Semigroups.StronglyContinuousSemigroup.complexGenerator_phaseShift: the complex generator of t ↦ exp (-i b t) • S t is A - i b.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.2.2 (rescaled semigroups).

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.phaseShift {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (b : ℝ) : StronglyContinuousSemigroup X

The phase shift of a complex-linear C₀-semigroup by b : ℝ: the semigroup t ↦ exp (-i b t) • S t.

Equations

• S.phaseShift hS b = { toFun := fun (t : NNReal) => Complex.exp (-(↑b * ↑↑t) * Complex.I) • S t, map_zero' := ⋯, map_add' := ⋯, continuousAt_zero' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.phaseShift_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (b : ℝ) (t : NNReal) : (S.phaseShift hS b) t = Complex.exp (-(↑b * ↑↑t) * Complex.I) • S t

The native nonnegative-time operator of a phase shift.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.phaseShift_apply_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (b : ℝ) (t : NNReal) (x : X) : ((S.phaseShift hS b) t) x = Complex.exp (-(↑b * ↑↑t) * Complex.I) • (S t) x

Pointwise form of StronglyContinuousSemigroup.phaseShift_apply.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.phaseShift_realOperator_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (b t : ℝ) (ht : 0 ≤ t) : (S.phaseShift hS b).realOperator t = Complex.exp (-(↑b * ↑t) * Complex.I) • S.realOperator t

Real-time form of a phase-shifted operator at nonnegative times.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.phaseShift_realOperator_apply_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (b t : ℝ) (ht : 0 ≤ t) (x : X) : ((S.phaseShift hS b).realOperator t) x = Complex.exp (-(↑b * ↑t) * Complex.I) • (S.realOperator t) x

Pointwise real-time form of a phase-shifted operator at nonnegative times.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.IsComplexLinear.phaseShift {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] {S : StronglyContinuousSemigroup X} (hS : S.IsComplexLinear) (b : ℝ) : (S.phaseShift hS b).IsComplexLinear

A phase shift is again complex linear.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.phaseShift_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) : S.phaseShift hS 0 = S

The zero phase shift is the original semigroup.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.phaseShift_phaseShift {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (b c : ℝ) : (S.phaseShift hS b).phaseShift ⋯ c = S.phaseShift hS (b + c)

Successive phase shifts add their parameters.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound.phaseShift {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] {S : StronglyContinuousSemigroup X} {omega M : ℝ} (hb : S.HasGrowthBound omega M) (hS : S.IsComplexLinear) (b : ℝ) : (S.phaseShift hS b).HasGrowthBound omega M

A phase shift multiplies by a unimodular scalar, so it preserves every growth bound.

The generator of a phase shift

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.phaseShift_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (b : ℝ) : (S.phaseShift hS b).domain = S.domain

A phase shift does not change the generator domain.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_phaseShift_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (b : ℝ) {x : X} (hx : x ∈ S.domain) : ↑(S.phaseShift hS b).generator ⟨x, ⋯⟩ = ↑S.generator ⟨x, ⋯⟩ - (↑b * Complex.I) • x

The generator of a phase-shifted semigroup acts as A - i b.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexGenerator_phaseShift {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (b : ℝ) : (S.phaseShift hS b).complexGenerator ⋯ = LinearPMap.subScalar (S.complexGenerator hS) (↑b * Complex.I)

The generator of a phase shift. The complex generator of t ↦ exp (-i b t) • S t is A - i b, where A is the complex generator of S.