Linear flows from strongly continuous groups

A strongly continuous one-parameter group of bounded linear operators acts continuously on its underlying normed space, and hence determines a Flow. This file supplies that bridge between the operator-valued semigroup API and the point-valued dynamical API.

The construction forgets only linear structure: its time maps are the operators of the group. Consequently it commutes with time reversal, and its orbits are definitionally the group orbits.

Main declarations

• TauCeti.Semigroups.StronglyContinuousGroup.toFlow: the flow underlying a strongly continuous group.
• TauCeti.Semigroups.StronglyContinuousGroup.toFlow_reflect: time reversal commutes with passage to the underlying flow.

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

The continuous flow on X underlying a strongly continuous one-parameter group of bounded linear operators.

Equations

• U.toFlow = { toFun := fun (t : ℝ) (x : X) => (U t) x, cont' := ⋯, map_add' := ⋯, map_zero' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.toFlow_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (U : StronglyContinuousGroup X) (t : ℝ) (x : X) : U.toFlow.toFun t x = (U t) x

@[simp]

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

Passing to the underlying flow commutes with reversing time.