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

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 IsFwInvariant {τ : 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.

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

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

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

theorem isFwInvariant_iff_isInvariant {τ : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid τ] {ϕ : τ → α → α} {s : Set α} : IsFwInvariant ϕ s ↔ IsInvariant ϕ s

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

Flows

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

• 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 α.

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

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

theorem Flow.ext {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] {ϕ₁ : Flow τ α} {ϕ₂ : Flow τ α} : (∀ (t : τ) (x : α), Flow.toFun ϕ₁ t x = Flow.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 => Flow.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 => Flow.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 : α) : Flow.toFun ϕ (t₁ + t₂) x = Flow.toFun ϕ t₁ (Flow.toFun ϕ t₂ x)

@[simp]

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

theorem Flow.map_zero_apply {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (x : α) : Flow.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.

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

def Flow.reverse {τ : Type u_1} [AddCommGroup τ] [TopologicalSpace τ] [TopologicalAddGroup τ] {α : 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 τ] [TopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (t : τ) : Continuous (Flow.toFun ϕ t)

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

The map ϕ t as a homeomorphism.

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