Strongly continuous one-parameter groups

A C₀-group on a real normed space X is a family U : ℝ → X →L[ℝ] X indexed by all of ℝ with U 0 = 1, U (s + t) = U s ∘ U t, and t ↦ U t x continuous at 0. It is not reached by the C₀-semigroup API: the two-sided law makes every U t invertible, with inverse U (-t), and forces the orbits to be continuous on the whole line rather than only on [0, ∞). The unitary group e^{itH} of a Schrödinger evolution is the motivating example.

This file sets up the object and the two ways of viewing it through the existing StronglyContinuousSemigroup theory:

• the forward semigroup U.toSemigroup, the restriction of U to [0, ∞);
• the time reversal U.reflect, the C₀-group t ↦ U (-t), whose forward semigroup is the backward half of U.

The growth bound is obtained by applying semigroup results to both halves. The generator API in TauCeti.Analysis.Semigroups.Group.Generator, including generator uniqueness, similarly uses U.reflect for the backward half.

Main definitions

• TauCeti.Semigroups.StronglyContinuousGroup: the C₀-group structure.
• TauCeti.Semigroups.StronglyContinuousGroup.toContinuousLinearEquiv: U t as a continuous linear equivalence, with inverse U (-t).
• TauCeti.Semigroups.StronglyContinuousGroup.reflect: the time-reversed group t ↦ U (-t).
• TauCeti.Semigroups.StronglyContinuousGroup.toSemigroup: the forward C₀-semigroup.
• TauCeti.Semigroups.StronglyContinuousGroup.HasGrowthBound: the two-sided growth bound ‖U t‖ ≤ M * exp (ω * |t|).

Main results

• TauCeti.Semigroups.StronglyContinuousGroup.continuous_orbit: the orbits of a C₀-group are continuous on all of ℝ, not merely at 0.
• TauCeti.Semigroups.StronglyContinuousGroup.existsGrowthBound: every C₀-group has a finite two-sided exponential growth bound.
• TauCeti.Semigroups.StronglyContinuousGroup.isometry_of_forall_norm_le_one: a C₀-group that contracts in both time directions is a group of isometries.
• TauCeti.Semigroups.StronglyContinuousGroup.tendsto_apply: joint strong continuity U (f i) (g i) → U r z, at every real time and without a sign restriction.

References

Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.3.11; Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Section 1.6.

structure TauCeti.Semigroups.StronglyContinuousGroup (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] : Type u_1

A strongly continuous one-parameter group (C₀-group) on a real normed space.

The family is indexed by all of ℝ; the axioms are U 0 = Id, U (s + t) = U s ∘ U t at every pair of real times, and strong continuity at 0. Completeness is imposed separately on results that require it, such as existsGrowthBound.

• toFun : ℝ → X →L[ℝ] X

  The group operator at time t : ℝ.

• map_zero' : self.toFun 0 = ContinuousLinearMap.id ℝ X

  U 0 = Id.

• map_add' (s t : ℝ) : self.toFun (s + t) = self.toFun s ∘SL self.toFun t

  U (s + t) = U s ∘ U t, at every pair of real times.

• continuousAt_zero' (x : X) : ContinuousAt (fun (t : ℝ) => (self.toFun t) x) 0

  Strong continuity at 0.

@[instance_reducible]

instance TauCeti.Semigroups.StronglyContinuousGroup.instFunLike {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : FunLike (StronglyContinuousGroup X) ℝ (X →L[ℝ] X)

Equations

• TauCeti.Semigroups.StronglyContinuousGroup.instFunLike = { coe := TauCeti.Semigroups.StronglyContinuousGroup.toFun, coe_injective := ⋯ }

theorem TauCeti.Semigroups.StronglyContinuousGroup.ext {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U V : StronglyContinuousGroup X} (h : ∀ (t : ℝ), U t = V t) : U = V

theorem TauCeti.Semigroups.StronglyContinuousGroup.ext_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U V : StronglyContinuousGroup X} : U = V ↔ ∀ (t : ℝ), U t = V t

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.map_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) : U 0 = ContinuousLinearMap.id ℝ X

The group operator at time 0 is the identity.

theorem TauCeti.Semigroups.StronglyContinuousGroup.map_zero_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (x : X) : (U 0) x = x

Pointwise form of StronglyContinuousGroup.map_zero.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.map_add {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (s t : ℝ) : U (s + t) = U s ∘SL U t

The two-sided group law.

theorem TauCeti.Semigroups.StronglyContinuousGroup.map_add_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (s t : ℝ) (x : X) : (U (s + t)) x = (U s) ((U t) x)

Pointwise form of StronglyContinuousGroup.map_add.

theorem TauCeti.Semigroups.StronglyContinuousGroup.map_comm {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (s t : ℝ) (x : X) : (U s) ((U t) x) = (U t) ((U s) x)

Operators at different times commute.

Invertibility

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.map_neg_apply_map_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : ℝ) (x : X) : (U (-t)) ((U t) x) = x

U (-t) is a left inverse of U t.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.map_apply_map_neg_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : ℝ) (x : X) : (U t) ((U (-t)) x) = x

U (-t) is a right inverse of U t.

def TauCeti.Semigroups.StronglyContinuousGroup.toContinuousLinearEquiv {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : ℝ) : X ≃L[ℝ] X

The group operator at time t, packaged as a continuous linear equivalence whose inverse is the operator at time -t.

Equations

• U.toContinuousLinearEquiv t = ContinuousLinearEquiv.equivOfInverse (U t) (U (-t)) ⋯ ⋯

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.toContinuousLinearEquiv_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : ℝ) (x : X) : (U.toContinuousLinearEquiv t) x = (U t) x

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.toContinuousLinearEquiv_symm_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : ℝ) (x : X) : (U.toContinuousLinearEquiv t).symm x = (U (-t)) x

theorem TauCeti.Semigroups.StronglyContinuousGroup.bijective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : ℝ) : Function.Bijective ⇑(U t)

Every operator of a C₀-group is bijective.

Strong continuity on the whole line

theorem TauCeti.Semigroups.StronglyContinuousGroup.continuous_orbit {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (x : X) : Continuous fun (t : ℝ) => (U t) x

The orbits of a C₀-group are continuous on all of ℝ. The two-sided group law turns the increment at t₀ into an increment at 0, where continuity is assumed.

Time reversal and the forward semigroup

def TauCeti.Semigroups.StronglyContinuousGroup.reflect {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) : StronglyContinuousGroup X

The time-reversed C₀-group t ↦ U (-t).

Equations

• U.reflect = { toFun := fun (t : ℝ) => U (-t), map_zero' := ⋯, map_add' := ⋯, continuousAt_zero' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.reflect_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : ℝ) : U.reflect t = U (-t)

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.reflect_reflect {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) : U.reflect.reflect = U

def TauCeti.Semigroups.StronglyContinuousGroup.toSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) : StronglyContinuousSemigroup X

The forward C₀-semigroup of a C₀-group: the restriction of U to nonnegative times.

Equations

• U.toSemigroup = { toFun := fun (t : NNReal) => U ↑t, map_zero' := ⋯, map_add' := ⋯, continuousAt_zero' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.toSemigroup_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : NNReal) : U.toSemigroup t = U ↑t

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.toSemigroup_realOperator_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) {t : ℝ} (ht : 0 ≤ t) : U.toSemigroup.realOperator t = U t

At a nonnegative real time the forward semigroup's real-time shim is the group operator.

theorem TauCeti.Semigroups.StronglyContinuousGroup.reflect_toSemigroup_realOperator_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) {t : ℝ} (ht : 0 ≤ t) : U.reflect.toSemigroup.realOperator t = U (-t)

At a nonnegative real time the reversed group's forward semigroup runs U backwards.

Not a simp lemma: simp already reaches this form through toSemigroup_realOperator_of_nonneg and reflect_apply, so tagging it duplicates a rule simp derives anyway.

Two-sided growth bounds

def TauCeti.Semigroups.StronglyContinuousGroup.HasGrowthBound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (ω M : ℝ) : Prop

A C₀-group has exponential growth bound (ω, M), with M ≥ 1, if ‖U t‖ ≤ M e^{ω |t|} at every real time. The absolute value is what distinguishes this from the semigroup bound: a C₀-group grows at most exponentially in both time directions.

Equations

• U.HasGrowthBound ω M = (1 ≤ M ∧ ∀ (t : ℝ), ‖U t‖ ≤ M * Real.exp (ω * |t|))

theorem TauCeti.Semigroups.StronglyContinuousGroup.HasGrowthBound.one_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : StronglyContinuousGroup X} {ω M : ℝ} (hb : U.HasGrowthBound ω M) : 1 ≤ M

The multiplicative constant in a growth bound is at least one.

theorem TauCeti.Semigroups.StronglyContinuousGroup.HasGrowthBound.bound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : StronglyContinuousGroup X} {ω M : ℝ} (hb : U.HasGrowthBound ω M) (t : ℝ) : ‖U t‖ ≤ M * Real.exp (ω * |t|)

The operator-norm estimate supplied by a growth bound.

theorem TauCeti.Semigroups.StronglyContinuousGroup.HasGrowthBound.mono {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : StronglyContinuousGroup X} {ω M ω' M' : ℝ} (hb : U.HasGrowthBound ω M) (hω : ω ≤ ω') (hM : M ≤ M') : U.HasGrowthBound ω' M'

A two-sided growth bound can be weakened by increasing both the exponential rate and the multiplicative constant.

theorem TauCeti.Semigroups.StronglyContinuousGroup.HasGrowthBound.mono_omega {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : StronglyContinuousGroup X} {ω M ω' : ℝ} (hb : U.HasGrowthBound ω M) (hω : ω ≤ ω') : U.HasGrowthBound ω' M

A two-sided growth bound can be weakened by increasing the exponential rate.

theorem TauCeti.Semigroups.StronglyContinuousGroup.HasGrowthBound.mono_const {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : StronglyContinuousGroup X} {ω M M' : ℝ} (hb : U.HasGrowthBound ω M) (hM : M ≤ M') : U.HasGrowthBound ω M'

A two-sided growth bound can be weakened by increasing the multiplicative constant.

theorem TauCeti.Semigroups.StronglyContinuousGroup.hasGrowthBound_of_bound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : StronglyContinuousGroup X} {ω M : ℝ} (hM : 1 ≤ M) (hbound : ∀ (t : ℝ), ‖U t‖ ≤ M * Real.exp (ω * |t|)) : U.HasGrowthBound ω M

Constructor for a two-sided growth bound from the multiplicative lower bound and the operator-norm estimate.

theorem TauCeti.Semigroups.StronglyContinuousGroup.HasGrowthBound.toSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : StronglyContinuousGroup X} {ω M : ℝ} (hb : U.HasGrowthBound ω M) : U.toSemigroup.HasGrowthBound ω M

A two-sided growth bound restricts to a growth bound for the forward semigroup.

theorem TauCeti.Semigroups.StronglyContinuousGroup.HasGrowthBound.reflect {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {U : StronglyContinuousGroup X} {ω M : ℝ} (hb : U.HasGrowthBound ω M) : U.reflect.HasGrowthBound ω M

A two-sided growth bound is invariant under time reversal.

theorem TauCeti.Semigroups.StronglyContinuousGroup.hasGrowthBound_zero_one_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) : U.HasGrowthBound 0 1 ↔ ∀ (t : ℝ), ‖U t‖ ≤ 1

Growth bound (0, 1) is exactly contractivity at every real time.

Contraction groups are groups of isometries

theorem TauCeti.Semigroups.StronglyContinuousGroup.norm_map_apply_eq_of_norm_le_one {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : ℝ) (ht : ‖U t‖ ≤ 1) (ht' : ‖U (-t)‖ ≤ 1) (x : X) : ‖(U t) x‖ = ‖x‖

A C₀-group that contracts in both time directions preserves norms. A strict contraction at time t would have to be undone by an expansion at time -t, which contractivity forbids. This is the norm preservation behind unitary groups such as e^{itH}.

theorem TauCeti.Semigroups.StronglyContinuousGroup.isometry_of_forall_norm_le_one {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (h : ∀ (t : ℝ), ‖U t‖ ≤ 1) (t : ℝ) : Isometry ⇑(U t)

Every operator of a contractive C₀-group is an isometry.

theorem TauCeti.Semigroups.StronglyContinuousGroup.existsGrowthBound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (U : StronglyContinuousGroup X) : ∃ (ω : ℝ) (M : ℝ), U.HasGrowthBound ω M

Every C₀-group has a finite two-sided exponential growth bound. The forward and backward halves are C₀-semigroups, so each has a growth bound; taking the larger exponent and the larger constant covers both time directions at once.

theorem TauCeti.Semigroups.StronglyContinuousGroup.tendsto_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {ι : Type u_2} {l : Filter ι} (U : StronglyContinuousGroup X) {f : ι → ℝ} {g : ι → X} {r : ℝ} {z : X} (hf : Filter.Tendsto f l (nhds r)) (hg : Filter.Tendsto g l (nhds z)) : Filter.Tendsto (fun (i : ι) => (U (f i)) (g i)) l (nhds ((U r) z))

Joint strong continuity of a C₀-group: if f i → r and g i → z, then U (f i) (g i) → U r z.

This is the two-sided counterpart of TauCeti.Semigroups.StronglyContinuousSemigroup.tendsto_realOperator_apply, and needs no sign hypothesis on the times: the group has a growth bound valid on the whole line, which supplies the uniform operator bound that strong continuity alone does not.