Exponential shifts of strongly continuous semigroups

This file defines the exponentially shifted C₀-semigroup t ↦ exp (-lambda t) • S(t). Shifting is the standard way to move a growth bound (ω, M) to (ω - lambda, M), and in particular to turn a semigroup with bound (lambda, 1) into a contraction semigroup.

References

The construction is standard in the Hille--Yosida theory of C₀-semigroups; see Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Ch. II.

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.expShift {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (lambda : ℝ) : StronglyContinuousSemigroup X

The exponential shift of a C₀-semigroup by lambda.

At nonnegative time t, this is the semigroup exp (-lambda t) • S(t). It shifts growth exponents by subtracting lambda; see HasGrowthBound.expShift.

Equations

• S.expShift lambda = { toFun := fun (t : NNReal) => Real.exp (-(lambda * ↑t)) • S t, map_zero' := ⋯, map_add' := ⋯, continuousAt_zero' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.expShift_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (lambda : ℝ) (t : NNReal) : (S.expShift lambda) t = Real.exp (-(lambda * ↑t)) • S t

The native nonnegative-time operator of the exponential shift.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.expShift_apply_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (lambda : ℝ) (t : NNReal) (x : X) : ((S.expShift lambda) t) x = Real.exp (-(lambda * ↑t)) • (S t) x

Pointwise form of StronglyContinuousSemigroup.expShift_apply.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.expShift_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) : S.expShift 0 = S

The zero exponential shift is the original semigroup.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.expShift_expShift {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (lambda μ : ℝ) : (S.expShift lambda).expShift μ = S.expShift (lambda + μ)

Successive exponential shifts add their parameters.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.expShift_realOperator_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (lambda t : ℝ) (ht : 0 ≤ t) : (S.expShift lambda).realOperator t = Real.exp (-(lambda * t)) • S.realOperator t

Real-time form of the shifted operator at nonnegative times.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.expShift_realOperator_apply_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (lambda t : ℝ) (ht : 0 ≤ t) (x : X) : ((S.expShift lambda).realOperator t) x = Real.exp (-(lambda * t)) • (S.realOperator t) x

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

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound.expShift {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S : StronglyContinuousSemigroup X} {ω M lambda : ℝ} (hb : S.HasGrowthBound ω M) : (S.expShift lambda).HasGrowthBound (ω - lambda) M

Exponential shifting subtracts the shift parameter from the growth exponent.

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.expShiftContraction {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (lambda : ℝ) (hb : S.HasGrowthBound lambda 1) : ContractionSemigroup X

A semigroup with growth bound (lambda, 1) becomes a contraction semigroup after exponential shifting by lambda.

Equations

• S.expShiftContraction lambda hb = { toStronglyContinuousSemigroup := S.expShift lambda, contracting := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.expShiftContraction_toStronglyContinuousSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (lambda : ℝ) (hb : S.HasGrowthBound lambda 1) : (S.expShiftContraction lambda hb).toStronglyContinuousSemigroup = S.expShift lambda

The C₀-semigroup underlying expShiftContraction is the exponential shift.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.expShiftContraction_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (lambda : ℝ) (hb : S.HasGrowthBound lambda 1) (t : NNReal) : (S.expShiftContraction lambda hb) t = Real.exp (-(lambda * ↑t)) • S t

Native operator formula for expShiftContraction.