Flows and invariant sets

This file defines a flow on a topological space α by a topological monoid τ as a continuous monoid-action 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 (forward) orbit, a semiconjugacy between flows, a factor of a flow, the restriction of a flow onto an invariant subset, and the time-reversal of a flow by a group.

Invariant sets

def IsInvariant {τ : Type u_1} {α : Type u_2} (ϕ : τ → α → α) (s : Set α) : Prop

A set s ⊆ α is invariant under ϕ : τ → α → α if ϕ t s ⊆ s for all t in τ.

theorem isInvariant_iff_image {τ : Type u_1} {α : Type u_2} (ϕ : τ → α → α) (s : Set α) : IsInvariant ϕ s ↔ ∀ (t : τ), ϕ t '' s ⊆ s

def IsForwardInvariant {τ : Type u_1} {α : Type u_2} [Preorder τ] [Zero τ] (ϕ : τ → α → α) (s : Set α) : Prop

A set s ⊆ α is forward-invariant under ϕ : τ → α → α if ϕ t s ⊆ s for all t ≥ 0.

@[deprecated IsForwardInvariant (since := "2025-09-25")]

def IsFwInvariant {τ : Type u_1} {α : Type u_2} [Preorder τ] [Zero τ] (ϕ : τ → α → α) (s : Set α) : Prop

Alias of IsForwardInvariant.

---

A set s ⊆ α is forward-invariant under ϕ : τ → α → α if ϕ t s ⊆ s for all t ≥ 0.

theorem IsInvariant.isForwardInvariant {τ : Type u_1} {α : Type u_2} [Preorder τ] [Zero τ] {ϕ : τ → α → α} {s : Set α} (h : IsInvariant ϕ s) : IsForwardInvariant ϕ s

@[deprecated IsInvariant.isForwardInvariant (since := "2025-09-25")]

theorem IsInvariant.isFwInvariant {τ : Type u_1} {α : Type u_2} [Preorder τ] [Zero τ] {ϕ : τ → α → α} {s : Set α} (h : IsInvariant ϕ s) : IsForwardInvariant ϕ s

Alias of IsInvariant.isForwardInvariant.

theorem IsForwardInvariant.isInvariant {τ : Type u_1} {α : Type u_2} [AddMonoid τ] [PartialOrder τ] [CanonicallyOrderedAdd τ] {ϕ : τ → α → α} {s : Set α} (h : IsForwardInvariant ϕ s) : IsInvariant ϕ s

If τ is a CanonicallyOrderedAdd monoid (e.g., ℕ or ℝ≥0), then the notions IsForwardInvariant and IsInvariant are equivalent.

@[deprecated IsForwardInvariant.isInvariant (since := "2025-09-25")]

theorem IsFwInvariant.isInvariant {τ : Type u_1} {α : Type u_2} [AddMonoid τ] [PartialOrder τ] [CanonicallyOrderedAdd τ] {ϕ : τ → α → α} {s : Set α} (h : IsForwardInvariant ϕ s) : IsInvariant ϕ s

Alias of IsForwardInvariant.isInvariant.

---

If τ is a CanonicallyOrderedAdd monoid (e.g., ℕ or ℝ≥0), then the notions IsForwardInvariant and IsInvariant are equivalent.

theorem isForwardInvariant_iff_isInvariant {τ : Type u_1} {α : Type u_2} [AddMonoid τ] [PartialOrder τ] [CanonicallyOrderedAdd τ] {ϕ : τ → α → α} {s : Set α} : IsForwardInvariant ϕ s ↔ IsInvariant ϕ s

If τ is a CanonicallyOrderedAdd monoid (e.g., ℕ or ℝ≥0), then the notions IsForwardInvariant and IsInvariant are equivalent.

@[deprecated isForwardInvariant_iff_isInvariant (since := "2025-09-25")]

theorem isFwInvariant_iff_isInvariant {τ : Type u_1} {α : Type u_2} [AddMonoid τ] [PartialOrder τ] [CanonicallyOrderedAdd τ] {ϕ : τ → α → α} {s : Set α} : IsForwardInvariant ϕ s ↔ IsInvariant ϕ s

Alias of isForwardInvariant_iff_isInvariant.

---

If τ is a CanonicallyOrderedAdd monoid (e.g., ℕ or ℝ≥0), then the notions IsForwardInvariant and IsInvariant are equivalent.

Flows

structure Flow (τ : Type u_1) [TopologicalSpace τ] [AddMonoid τ] [ContinuousAdd τ] (α : Type u_2) [TopologicalSpace α] : Type (max u_1 u_2)

A flow on a topological space α by an additive topological monoid τ is a continuous monoid action of τ on α.

• toFun : τ → α → α

  The map τ → α → α underlying a flow of τ on α.

• cont' : Continuous (Function.uncurry self.toFun)
• map_add' (t₁ t₂ : τ) (x : α) : self.toFun (t₁ + t₂) x = self.toFun t₁ (self.toFun t₂ x)
• map_zero' (x : α) : self.toFun 0 x = x

instance Flow.instInhabited {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] : Inhabited (Flow τ α)

instance Flow.instCoeFunForallForall {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] : CoeFun (Flow τ α) fun (x : Flow τ α) => τ → α → α

theorem Flow.ext {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] {ϕ₁ ϕ₂ : Flow τ α} : (∀ (t : τ) (x : α), ϕ₁.toFun t x = ϕ₂.toFun t x) → ϕ₁ = ϕ₂

theorem Flow.ext_iff {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] {ϕ₁ ϕ₂ : Flow τ α} : ϕ₁ = ϕ₂ ↔ ∀ (t : τ) (x : α), ϕ₁.toFun t x = ϕ₂.toFun t x

theorem Flow.continuous {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) {β : Type u_3} [TopologicalSpace β] {t : β → τ} (ht : Continuous t) {f : β → α} (hf : Continuous f) : Continuous fun (x : β) => ϕ.toFun (t x) (f x)

theorem Continuous.flow {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) {β : Type u_3} [TopologicalSpace β] {t : β → τ} (ht : Continuous t) {f : β → α} (hf : Continuous f) : Continuous fun (x : β) => ϕ.toFun (t x) (f x)

Alias of Flow.continuous.

theorem Flow.map_add {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (t₁ t₂ : τ) (x : α) : ϕ.toFun (t₁ + t₂) x = ϕ.toFun t₁ (ϕ.toFun t₂ x)

@[simp]

theorem Flow.map_zero {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) : ϕ.toFun 0 = id

theorem Flow.map_zero_apply {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (x : α) : ϕ.toFun 0 x = x

def Flow.fromIter {α : Type u_2} [TopologicalSpace α] {g : α → α} (h : Continuous g) : Flow ℕ α

Iterations of a continuous function from a topological space α to itself defines a semiflow by ℕ on α.

def Flow.restrict {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) {s : Set α} (h : IsInvariant ϕ.toFun s) : Flow τ ↑s

Restriction of a flow onto an invariant set.

@[simp]

theorem Flow.coe_restrict_apply {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) {s : Set α} (h : IsInvariant ϕ.toFun s) (t : τ) (x : ↑s) : ↑((ϕ.restrict h).toFun t x) = ϕ.toFun t ↑x

def Flow.toAddAction {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) : AddAction τ α

Convert a flow to an additive monoid action.

def Flow.restrictAddSubmonoid {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (S : AddSubmonoid τ) : Flow (↥S) α

Restrict a flow by τ to a flow by an additive submonoid of τ.

theorem Flow.restrictAddSubmonoid_apply {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (S : AddSubmonoid τ) (t : ↥S) (x : α) : (ϕ.restrictAddSubmonoid S).toFun t x = ϕ.toFun (↑t) x

def Flow.orbit {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (x : α) : Set α

The orbit of a point under a flow.

theorem Flow.orbit_eq_range {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (x : α) : ϕ.orbit x = Set.range fun (t : τ) => ϕ.toFun t x

theorem Flow.mem_orbit_iff {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) {x₁ x₂ : α} : x₂ ∈ ϕ.orbit x₁ ↔ ∃ (t : τ), ϕ.toFun t x₁ = x₂

theorem Flow.mem_orbit {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (x : α) (t : τ) : ϕ.toFun t x ∈ ϕ.orbit x

theorem Flow.mem_orbit_self {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (x : α) : x ∈ ϕ.orbit x

theorem Flow.nonempty_orbit {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (x : α) : (ϕ.orbit x).Nonempty

theorem Flow.mem_orbit_of_mem_orbit {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) {x₁ x₂ : α} (t : τ) (h : x₂ ∈ ϕ.orbit x₁) : ϕ.toFun t x₂ ∈ ϕ.orbit x₁

theorem Flow.isInvariant_orbit {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (x : α) : IsInvariant ϕ.toFun (ϕ.orbit x)

The orbit of a point under a flow ϕ is invariant under ϕ.

theorem Flow.orbit_restrict {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (s : Set α) (hs : IsInvariant ϕ.toFun s) (x : ↑s) : (ϕ.restrict hs).orbit x = Subtype.val ⁻¹' ϕ.orbit ↑x

def Flow.restrictNonneg {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) [Preorder τ] [AddLeftMono τ] : Flow (↥(AddSubmonoid.nonneg τ)) α

Restrict a flow by τ to a flow by the additive submonoid of nonnegative elements of τ.

def Flow.forwardOrbit {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) [Preorder τ] [AddLeftMono τ] (x : α) : Set α

The forward orbit of a point under a flow.

theorem Flow.forwardOrbit_eq_range_nonneg {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) [Preorder τ] [AddLeftMono τ] (x : α) : ϕ.forwardOrbit x = Set.range fun (t : { t : τ // 0 ≤ t }) => ϕ.toFun (↑t) x

theorem Flow.isForwardInvariant_forwardOrbit {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) [Preorder τ] [AddLeftMono τ] (x : α) : IsForwardInvariant ϕ.toFun (ϕ.forwardOrbit x)

The forward orbit of a point under a flow ϕ is forward-invariant under ϕ.

theorem Flow.forwardOrbit_subset_orbit {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) [Preorder τ] [AddLeftMono τ] (x : α) : ϕ.forwardOrbit x ⊆ ϕ.orbit x

The forward orbit of a point x is contained in the orbit of x.

theorem Flow.mem_orbit_of_mem_forwardOrbit {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) [Preorder τ] [AddLeftMono τ] {x₁ x₂ : α} (h : x₁ ∈ ϕ.forwardOrbit x₂) : x₁ ∈ ϕ.orbit x₂

structure Flow.IsSemiconjugacy {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] (π : α → β) (ϕ : Flow τ α) (ψ : Flow τ β) : Prop

Given flows ϕ by τ on α and ψ by τ on β, a function π : α → β is called a semiconjugacy from ϕ to ψ if π is continuous and surjective, and π ∘ (ϕ t) = (ψ t) ∘ π for all t : τ.

• cont : Continuous π
• surj : Function.Surjective π
• semiconj (t : τ) : Function.Semiconj π (ϕ.toFun t) (ψ.toFun t)

theorem Flow.IsSemiconjugacy.comp {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) {β : Type u_3} {γ : Type u_4} [TopologicalSpace β] [TopologicalSpace γ] (ψ : Flow τ β) (χ : Flow τ γ) {π : α → β} {ρ : β → γ} (h₁ : IsSemiconjugacy π ϕ ψ) (h₂ : IsSemiconjugacy ρ ψ χ) : IsSemiconjugacy (ρ ∘ π) ϕ χ

The composition of semiconjugacies is a semiconjugacy.

theorem Flow.isSemiconjugacy_id_iff_eq {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ ψ : Flow τ α) : IsSemiconjugacy id ϕ ψ ↔ ϕ = ψ

The identity is a semiconjugacy from ϕ to ψ if and only if ϕ and ψ are equal.

def Flow.IsFactorOf {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] {β : Type u_3} [TopologicalSpace β] (ψ : Flow τ β) (ϕ : Flow τ α) : Prop

A flow ψ is called a factor of ϕ if there exists a semiconjugacy from ϕ to ψ.

theorem Flow.IsSemiconjugacy.isFactorOf {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) {β : Type u_3} [TopologicalSpace β] (ψ : Flow τ β) {π : α → β} (h : IsSemiconjugacy π ϕ ψ) : ψ.IsFactorOf ϕ

theorem Flow.IsFactorOf.trans {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) {β : Type u_3} {γ : Type u_4} [TopologicalSpace β] [TopologicalSpace γ] (ψ : Flow τ β) (χ : Flow τ γ) (h₁ : ϕ.IsFactorOf ψ) (h₂ : ψ.IsFactorOf χ) : ϕ.IsFactorOf χ

Transitivity of factors of flows.

theorem Flow.IsFactorOf.self {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) : ϕ.IsFactorOf ϕ

Every flow is a factor of itself.

theorem Flow.isInvariant_iff_image_eq {τ : Type u_1} [AddCommGroup τ] [TopologicalSpace τ] [IsTopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (s : Set α) : IsInvariant ϕ.toFun s ↔ ∀ (t : τ), ϕ.toFun t '' s = s

def Flow.reverse {τ : Type u_1} [AddCommGroup τ] [TopologicalSpace τ] [IsTopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) : Flow τ α

The time-reversal of a flow ϕ by a (commutative, additive) group is defined ϕ.reverse t x = ϕ (-t) x.

theorem Flow.continuous_toFun {τ : Type u_1} [AddCommGroup τ] [TopologicalSpace τ] [IsTopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (t : τ) : Continuous (ϕ.toFun t)

def Flow.toHomeomorph {τ : Type u_1} [AddCommGroup τ] [TopologicalSpace τ] [IsTopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (t : τ) : α ≃ₜ α

The map ϕ t as a homeomorphism.

theorem Flow.image_eq_preimage_symm {τ : Type u_1} [AddCommGroup τ] [TopologicalSpace τ] [IsTopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (t : τ) (s : Set α) : ϕ.toFun t '' s = ϕ.toFun (-t) ⁻¹' s