The generator of a strongly continuous group

The generator of a C₀-group U is the generator of its forward semigroup. What is new on a group is that the difference quotient converges from both sides: the time-reversed group U.reflect has the same generator domain and the negated generator (TauCeti.Semigroups.StronglyContinuousGroup.reflect_generator), and combining the two one-sided limits upgrades the right derivative of an orbit to a genuine two-sided derivative on all of ℝ. So for x ∈ D(A) the orbit u (t) = U t x is a classical solution of u' = A u on the whole line, not just on [0, ∞).

Because a semigroup is determined by its generator, so is a group: the generator fixes the forward half directly and the backward half through U.reflect.

Main results

• TauCeti.Semigroups.StronglyContinuousGroup.reflect_generator: the generator of the time-reversed group is -A, on the same domain.
• TauCeti.Semigroups.StronglyContinuousGroup.hasDerivAt: for x ∈ D(A) the orbit t ↦ U t x is differentiable at every real time, with derivative U t (A x).
• TauCeti.Semigroups.StronglyContinuousGroup.map_mem_domain and TauCeti.Semigroups.StronglyContinuousGroup.generator_map: D(A) is invariant under the whole group and A commutes with it.
• TauCeti.Semigroups.StronglyContinuousGroup.eq_of_generator_eq: a C₀-group is determined by its generator.
• TauCeti.Semigroups.StronglyContinuousGroup.ofBounded: the C₀-group t ↦ exp (t • A) of a bounded operator, with generator A; every C₀-group whose generator is A on all of X is of this form.

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.

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

The domain D(A) of the generator of a C₀-group: the generator domain of its forward semigroup.

Equations

• U.domain = U.toSemigroup.domain

noncomputable def TauCeti.Semigroups.StronglyContinuousGroup.generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) : X →ₗ.[ℝ] X

The infinitesimal generator of a C₀-group, as an unbounded operator: the generator of its forward semigroup. The two-sided law makes the defining limit two-sided as well (TauCeti.Semigroups.StronglyContinuousGroup.hasDerivAt).

Equations

• U.generator = U.toSemigroup.generator

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

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

@[simp]

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

The defining limit

theorem TauCeti.Semigroups.StronglyContinuousGroup.mem_domain_iff_tendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (x : X) : x ∈ U.domain ↔ ∃ (y : X), Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((U t) x - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds y)

A vector lies in the generator domain iff its difference quotient (U t x - x)/t converges as t → 0⁺.

theorem TauCeti.Semigroups.StronglyContinuousGroup.generator_tendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (x : ↥U.domain) : Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((U t) ↑x - ↑x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (↑U.generator ⟨↑x, ⋯⟩))

Characteristic property of the generator: for x ∈ D(A) the difference quotient converges to A x as t → 0⁺.

theorem TauCeti.Semigroups.StronglyContinuousGroup.generator_eq_of_tendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) {x : X} (hx : x ∈ U.domain) {y : X} (h : Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((U t) x - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds y)) : ↑U.generator ⟨x, ⋯⟩ = y

Eliminator for the generator: if the difference quotient of an x ∈ D(A) converges to y, then A x = y.

theorem TauCeti.Semigroups.StronglyContinuousGroup.map_mem_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (x : ↥U.domain) (t : ℝ) : (U t) ↑x ∈ U.domain

The generator domain is invariant under the whole group, at negative times as well as positive ones.

theorem TauCeti.Semigroups.StronglyContinuousGroup.generator_map {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (x : ↥U.domain) (t : ℝ) : ↑U.generator ⟨(U t) ↑x, ⋯⟩ = (U t) (↑U.generator ⟨↑x, ⋯⟩)

The generator commutes with the group.

theorem TauCeti.Semigroups.StronglyContinuousGroup.tendsto_of_hasDerivAt_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) {y c : X} (h : HasDerivAt (fun (s : ℝ) => (U s) y) c 0) : Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((U t) y - y)) (nhdsWithin 0 (Set.Ioi 0)) (nhds c)

The positive-time difference quotient at 0 extracted from a two-sided derivative of an orbit.

theorem TauCeti.Semigroups.StronglyContinuousGroup.mem_domain_of_hasDerivAt_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) {x y : X} (h : HasDerivAt (fun (t : ℝ) => (U t) x) y 0) : x ∈ U.domain

A vector whose orbit is differentiable at 0 belongs to the generator domain.

theorem TauCeti.Semigroups.StronglyContinuousGroup.generator_eq_of_hasDerivAt_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) {x y : X} (h : HasDerivAt (fun (t : ℝ) => (U t) x) y 0) : ↑U.generator ⟨x, ⋯⟩ = y

The generator value is the derivative at 0 of the orbit.

Time reversal

@[simp]

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

The generator domain is invariant under time reversal.

@[simp]

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

The generator of the time-reversed group is the negative of the generator, on the same domain. This is the two-sided statement that makes the backward half of a C₀-group accessible to the semigroup API.

Two-sided differentiability of the orbits

theorem TauCeti.Semigroups.StronglyContinuousGroup.generator_tendsto_nhdsLT {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (U : StronglyContinuousGroup X) (x : ↥U.domain) : Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((U t) ↑x - ↑x)) (nhdsWithin 0 (Set.Iio 0)) (nhds (↑U.generator ⟨↑x, ⋯⟩))

For a domain vector the difference quotient converges from the left as well, to the same limit: the left quotient is minus the reversed group's right quotient, which converges to -A x.

theorem TauCeti.Semigroups.StronglyContinuousGroup.hasDerivAt_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (U : StronglyContinuousGroup X) (x : ↥U.domain) : HasDerivAt (fun (t : ℝ) => (U t) ↑x) (↑U.generator ⟨↑x, ⋯⟩) 0

The orbit of a domain vector is two-sidedly differentiable at 0.

theorem TauCeti.Semigroups.StronglyContinuousGroup.hasDerivAt {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (U : StronglyContinuousGroup X) (x : ↥U.domain) (t : ℝ) : HasDerivAt (fun (s : ℝ) => (U s) ↑x) ((U t) (↑U.generator ⟨↑x, ⋯⟩)) t

The abstract Cauchy problem on the whole line. For x ∈ D(A) the orbit t ↦ U t x is differentiable at every real time, with derivative U t (A x).

Uniqueness

theorem TauCeti.Semigroups.StronglyContinuousGroup.eq_of_generator_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {U V : StronglyContinuousGroup X} (h : U.generator = V.generator) : U = V

A C₀-group is determined by its generator. The generator fixes the forward semigroup by uniqueness for semigroups, and it fixes the backward half through the reversed group, whose generator is -A.

theorem TauCeti.Semigroups.StronglyContinuousGroup.generator_injective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] : Function.Injective generator

Injectivity form of TauCeti.Semigroups.StronglyContinuousGroup.eq_of_generator_eq.

The group generated by a bounded operator

noncomputable def TauCeti.Semigroups.StronglyContinuousGroup.ofBounded {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) : StronglyContinuousGroup X

The uniformly continuous C₀-group U(t) = exp (t • A) of a bounded operator A. Unlike the semigroup TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded, this runs in both time directions: exp (-t • A) inverts exp (t • A).

Equations

• TauCeti.Semigroups.StronglyContinuousGroup.ofBounded A = { toFun := fun (t : ℝ) => NormedSpace.exp (t • A), map_zero' := ⋯, map_add' := ⋯, continuousAt_zero' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.ofBounded_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) (t : ℝ) : (ofBounded A) t = NormedSpace.exp (t • A)

The operator of ofBounded A at time t is exp (t • A).

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.ofBounded_toSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) : (ofBounded A).toSemigroup = StronglyContinuousSemigroup.ofBounded A

The forward semigroup of ofBounded A is the bounded-generator semigroup of A.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.ofBounded_reflect {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) : (ofBounded A).reflect = ofBounded (-A)

Time reversal of ofBounded A is the group of -A.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.ofBounded_domain_eq_top {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) : (ofBounded A).domain = ⊤

The generator domain of ofBounded A is the whole space.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.ofBounded_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) : (ofBounded A).generator = (↑A).toPMap ⊤

The generator of ofBounded A is A itself, viewed as a total unbounded operator.

theorem TauCeti.Semigroups.StronglyContinuousGroup.ofBounded_hasGrowthBound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) : (ofBounded A).HasGrowthBound ‖A‖ 1

ofBounded A has the two-sided growth bound (‖A‖, 1): ‖exp (t • A)‖ ≤ e^{‖A‖ |t|}.

theorem TauCeti.Semigroups.StronglyContinuousGroup.eq_ofBounded_of_generator_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {U : StronglyContinuousGroup X} (A : X →L[ℝ] X) (h : U.generator = (↑A).toPMap ⊤) : U = ofBounded A

A C₀-group whose generator is the bounded operator A, defined on all of X, is the operator exponential t ↦ exp (t • A).