Flows and invariant sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines a flow on a topological space
α by a topological
τ as a continuous monoid-act of
α. Anticipating the
τ is one of
ℝ, we use additive
notation for the monoids, though the definition does not require
α is invariant under a family of maps
ϕₜ : α → α
ϕₜ s ⊆ s for all
t. In many cases
ϕ will be a flow on
α. For the cases where
ϕ is a flow by an ordered (additive,
commutative) monoid, we additionally define forward invariance, where
t ranges over those elements which are nonnegative.
Additionally, we define such constructions as the restriction of a flow onto an invariant subset, and the time-reveral of a flow by a group.
Invariant sets #
- to_fun : τ → α → α
- cont' : continuous (function.uncurry self.to_fun)
- map_add' : ∀ (t₁ t₂ : τ) (x : α), self.to_fun (t₁ + t₂) x = self.to_fun t₁ (self.to_fun t₂ x)
- map_zero' : ∀ (x : α), self.to_fun 0 x = x
A flow on a topological space
α by an a additive topological
τ is a continuous monoid action of
Iterations of a continuous function from a topological space
to itself defines a semiflow by
Restriction of a flow onto an invariant set.
The time-reversal of a flow
ϕ by a (commutative, additive) group
ϕ.reverse t x = ϕ (-t) x.
ϕ t as a homeomorphism.