The uniformly continuous semigroup generated by a bounded operator

For a bounded operator A : X →L[ℝ] X on a Banach space, the operator exponential t ↦ exp (t • A) is a strongly (indeed uniformly, norm-) continuous one-parameter semigroup. This file records that construction, ofBounded A, and its basic API:

• ofBounded A is a StronglyContinuousSemigroup, with exp (t • A) at time t;
• it satisfies the growth bound (‖A‖, 1), from ‖exp x‖ ≤ Real.exp ‖x‖;
• its infinitesimal generator is A itself, on the whole space (ofBounded_domain_eq_top, ofBounded_generator);
• conversely, uniqueness of the semigroup generated by an operator identifies every C₀-semigroup whose generator is A on the whole space with ofBounded A (eq_ofBounded_of_generator_eq).

This is the general bounded-generator acceptance example for the one-parameter-semigroups roadmap; the zero-operator case is the identity semigroup (TauCeti/Analysis/Semigroups/Identity.lean), and here A is an arbitrary bounded operator. The endomorphism algebra X →L[ℝ] X is a Banach algebra, so Mathlib's NormedSpace.exp and its derivative hasDerivAt_exp_smul_const apply directly.

References

The uniformly continuous semigroup S(t) = exp (tA) and the identification of its generator with A are standard; see Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Ch. I, and Pazy, Semigroups of Linear Operators, Ch. 1.

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

The uniformly continuous C₀-semigroup S(t) = exp (t • A) generated by a bounded operator A : X →L[ℝ] X.

Equations

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

@[simp]

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

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

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_apply_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) (t : NNReal) (x : X) : ((ofBounded A) t) x = (NormedSpace.exp (↑t • A)) x

The operator of ofBounded A at nonnegative time t, applied to x, is exp (t • A) x.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_realOperator_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) {t : ℝ} (ht : 0 ≤ t) : (ofBounded A).realOperator t = NormedSpace.exp (t • A)

The real-time operator of ofBounded A at t ≥ 0 is exp (t • A).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_realOperator_apply_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) {t : ℝ} (ht : 0 ≤ t) (x : X) : ((ofBounded A).realOperator t) x = (NormedSpace.exp (t • A)) x

The real-time operator of ofBounded A at t ≥ 0, applied to x, is exp (t • A) x.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_continuous {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) : Continuous fun (t : NNReal) => (ofBounded A) t

The bounded-generator semigroup is norm-continuous in nonnegative time.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_realOperator_continuousOn_Ici {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) : ContinuousOn (fun (t : ℝ) => (ofBounded A).realOperator t) (Set.Ici 0)

The real-time operator of ofBounded A is norm-continuous on the nonnegative half-line.

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

The semigroup ofBounded A has the growth bound (‖A‖, 1): ‖exp (t • A)‖ ≤ e^{‖A‖ t}.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_ofBounded_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) (x : X) : x ∈ (ofBounded A).domain

Every vector lies in the generator domain of ofBounded A: its generator is bounded.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.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.StronglyContinuousSemigroup.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.StronglyContinuousSemigroup.eq_ofBounded_of_generator_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S : StronglyContinuousSemigroup X} (A : X →L[ℝ] X) (h : S.generator = (↑A).toPMap ⊤) : S = ofBounded A

A strongly continuous semigroup whose generator is the bounded operator A, defined on all of X, is the operator exponential t ↦ exp (t • A).