Flows and invariant sets #
This file defines a flow on a topological space α
by a topological
monoid τ
as a continuous monoid-act of τ
on α
. Anticipating the
cases where τ
is one of ℕ
, ℤ
, ℝ⁺
, or ℝ
, we use additive
notation for the monoids, though the definition does not require
commutativity.
A subset s
of α
is invariant under a family of maps ϕₜ : α → α
if ϕₜ 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-reversal of a flow by a group.
Invariant sets #
If τ
is a CanonicallyOrderedAddMonoid
(e.g., ℕ
or ℝ≥0
), then the notions
IsFwInvariant
and IsInvariant
are equivalent.
If τ
is a CanonicallyOrderedAddMonoid
(e.g., ℕ
or ℝ≥0
), then the notions
IsFwInvariant
and IsInvariant
are equivalent.
Flows #
- toFun : τ → α → α
- cont' : Continuous (Function.uncurry s.toFun)
- map_add' : ∀ (t₁ t₂ : τ) (x : α), Flow.toFun s (t₁ + t₂) x = Flow.toFun s t₁ (Flow.toFun s t₂ x)
- map_zero' : ∀ (x : α), Flow.toFun s 0 x = x
A flow on a topological space α
by an additive topological
monoid τ
is a continuous monoid action of τ
on α
.
Instances For
Alias of Flow.continuous
.
Iterations of a continuous function from a topological space α
to itself defines a semiflow by ℕ
on α
.
Instances For
Restriction of a flow onto an invariant set.
Instances For
The time-reversal of a flow ϕ
by a (commutative, additive) group
is defined ϕ.reverse t x = ϕ (-t) x
.
Instances For
The map ϕ t
as a homeomorphism.