mathlib3 documentation

dynamics.flow

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 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-reveral of a flow by a group.

Invariant sets #

source
def is_invariant {τ : Type u_1} {α : Type u_2} (ϕ : τ → α → α) (s : set α) :
Prop

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

Equations
source
theorem is_invariant_iff_image {τ : Type u_1} {α : Type u_2} (ϕ : τ → α → α) (s : set α) :
is_invariant ϕ s ↔ ∀ (t : τ), ϕ t '' s ⊆ s
source
def is_fw_invariant {τ : Type u_1} {α : Type u_2} [preorder τ] [has_zero τ] (ϕ : τ → α → α) (s : set α) :
Prop

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

Equations
source
theorem is_invariant.is_fw_invariant {τ : Type u_1} {α : Type u_2} [preorder τ] [has_zero τ] {ϕ : τ → α → α} {s : set α} (h : is_invariant ϕ s) :
is_fw_invariant ϕ s
source
theorem is_fw_invariant.is_invariant {τ : Type u_1} {α : Type u_2} [canonically_ordered_add_monoid τ] {ϕ : τ → α → α} {s : set α} (h : is_fw_invariant ϕ s) :
is_invariant ϕ s

If τ is a canonically_ordered_add_monoid (e.g., ℕ or ℝ≥0), then the notions is_fw_invariant and is_invariant are equivalent.

source
theorem is_fw_invariant_iff_is_invariant {τ : Type u_1} {α : Type u_2} [canonically_ordered_add_monoid τ] {ϕ : τ → α → α} {s : set α} :
is_fw_invariant ϕ s ↔ is_invariant ϕ s

If τ is a canonically_ordered_add_monoid (e.g., ℕ or ℝ≥0), then the notions is_fw_invariant and is_invariant are equivalent.

Flows #

source
structure flow (τ : Type u_1) [topological_space τ] [add_monoid τ] [has_continuous_add τ] (α : Type u_2) [topological_space α] :
Type (max u_1 u_2)

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

Instances for flow
source
@[protected, instance]
def flow.inhabited {τ : Type u_1} [add_monoid τ] [topological_space τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] :
inhabited (flow τ α)
Equations
source
@[protected, instance]
def flow.has_coe_to_fun {τ : Type u_1} [add_monoid τ] [topological_space τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] :
has_coe_to_fun (flow τ α) (λ (_x : flow τ α), τ → α → α)
Equations
source
@[ext]
theorem flow.ext {τ : Type u_1} [add_monoid τ] [topological_space τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] {ϕ₁ ϕ₂ : flow τ α} :
(∀ (t : τ) (x : α), ⇑ϕ₁ t x = ⇑ϕ₂ t x) → ϕ₁ = ϕ₂
source
@[protected, continuity]
theorem flow.continuous {τ : Type u_1} [add_monoid τ] [topological_space τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] (ϕ : flow τ α) {β : Type u_3} [topological_space β] {t : β → τ} (ht : continuous t) {f : β → α} (hf : continuous f) :
continuous (λ (x : β), ⇑ϕ (t x) (f x))
source
theorem continuous.flow {τ : Type u_1} [add_monoid τ] [topological_space τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] (ϕ : flow τ α) {β : Type u_3} [topological_space β] {t : β → τ} (ht : continuous t) {f : β → α} (hf : continuous f) :
continuous (λ (x : β), ⇑ϕ (t x) (f x))

Alias of flow.continuous.

source
theorem flow.map_add {τ : Type u_1} [add_monoid τ] [topological_space τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] (ϕ : flow τ α) (t₁ t₂ : τ) (x : α) :
⇑ϕ (t₁ + t₂) x = ⇑ϕ t₁ (⇑ϕ t₂ x)
source
@[simp]
theorem flow.map_zero {τ : Type u_1} [add_monoid τ] [topological_space τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] (ϕ : flow τ α) :
⇑ϕ 0 = id
source
theorem flow.map_zero_apply {τ : Type u_1} [add_monoid τ] [topological_space τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] (ϕ : flow τ α) (x : α) :
⇑ϕ 0 x = x
source
def flow.from_iter {α : Type u_2} [topological_space α] {g : α → α} (h : continuous g) :
flow ℕ α

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

Equations
source
def flow.restrict {τ : Type u_1} [add_monoid τ] [topological_space τ] [has_continuous_add τ] {α : Type u_2} [topological_space α] (ϕ : flow τ α) {s : set α} (h : is_invariant ⇑ϕ s) :
flow τ ↥s

Restriction of a flow onto an invariant set.

Equations
source
theorem flow.is_invariant_iff_image_eq {τ : Type u_1} [add_comm_group τ] [topological_space τ] [topological_add_group τ] {α : Type u_2} [topological_space α] (ϕ : flow τ α) (s : set α) :
is_invariant ⇑ϕ s ↔ ∀ (t : τ), ⇑ϕ t '' s = s
source
def flow.reverse {τ : Type u_1} [add_comm_group τ] [topological_space τ] [topological_add_group τ] {α : Type u_2} [topological_space α] (ϕ : flow τ α) :
flow τ α

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

Equations
source
def flow.to_homeomorph {τ : Type u_1} [add_comm_group τ] [topological_space τ] [topological_add_group τ] {α : Type u_2} [topological_space α] (ϕ : flow τ α) (t : τ) :
α ≃ₜ α

The map ϕ t as a homeomorphism.

Equations
source
theorem flow.image_eq_preimage {τ : Type u_1} [add_comm_group τ] [topological_space τ] [topological_add_group τ] {α : Type u_2} [topological_space α] (ϕ : flow τ α) (t : τ) (s : set α) :
⇑ϕ t '' s = ⇑ϕ (-t) ⁻¹' s