Continuity of the Generated Semigroup Orbit

This is the continuity statement for the orbit generated by a closed densely defined operator.

Let $H_0,H_1$ be complete real Hilbert spaces, let $T:H_0\to H_1$ be a linear partial map, let hT assert that $T$ is closed, and let hd assert that its domain is dense in $H_0$. For every $f\in H_0$, the generated orbit $t\mapsto P_t f$, represented by Generated.apply T hT hd t f, is continuous on the nonnegative half-line:

This is a semigroup regularity statement for nonnegative times.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Semigroup.Generated. Shown in its original module context. Proof omitted.

theorem continuousOn (T : H₀ →ₗ.[ℝ] H₁) (hT : T.IsClosed)
    (hd : Dense (T.domain : Set H₀)) (f : H₀) :
    ContinuousOn (fun t : ℝ => Generated.apply T hT hd t f) (Set.Ici 0)

Module navigation

Module: Analysis/Semigroup/Generated/Laws.

Definition modules: Analysis/Semigroup/Generated/Basic.

Source excerpt, lines 399–401 · Frozen source 408915f.