Documentation

Mathlib.Dynamics.Flow

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 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 α) :

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

Equations
Instances For
    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 α) :

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

    Equations
    Instances For
      theorem IsInvariant.isFwInvariant {τ : Type u_1} {α : Type u_2} [Preorder τ] [Zero τ] {ϕ : ταα} {s : Set α} (h : IsInvariant ϕ s) :
      theorem IsFwInvariant.isInvariant {τ : Type u_1} {α : Type u_2} [CanonicallyOrderedAddCommMonoid τ] {ϕ : ταα} {s : Set α} (h : IsFwInvariant ϕ s) :

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

      theorem isFwInvariant_iff_isInvariant {τ : Type u_1} {α : Type u_2} [CanonicallyOrderedAddCommMonoid τ] {ϕ : ταα} {s : Set α} :

      If τ is a CanonicallyOrderedAddCommMonoid (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)

      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
      Instances For
        theorem Flow.cont' {τ : Type u_1} [TopologicalSpace τ] [AddMonoid τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (self : Flow τ α) :
        theorem Flow.map_add' {τ : Type u_1} [TopologicalSpace τ] [AddMonoid τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (self : Flow τ α) (t₁ : τ) (t₂ : τ) (x : α) :
        self.toFun (t₁ + t₂) x = self.toFun t₁ (self.toFun t₂ x)
        theorem Flow.map_zero' {τ : Type u_1} [TopologicalSpace τ] [AddMonoid τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] (self : Flow τ α) (x : α) :
        self.toFun 0 x = x
        instance Flow.instInhabited {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] :
        Inhabited (Flow τ α)
        Equations
        • Flow.instInhabited = { default := { toFun := fun (x : τ) (x : α) => x, cont' := , map_add' := , map_zero' := } }
        instance Flow.instCoeFunForallForall {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] :
        CoeFun (Flow τ α) fun (x : Flow τ α) => ταα
        Equations
        • Flow.instCoeFunForallForall = { coe := Flow.toFun }
        theorem Flow.ext {τ : Type u_1} [AddMonoid τ] [TopologicalSpace τ] [ContinuousAdd τ] {α : Type u_2} [TopologicalSpace α] {ϕ₁ : Flow τ α} {ϕ₂ : 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) :

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

        Equations
        • Flow.fromIter h = { toFun := fun (n : ) (x : α) => g^[n] x, cont' := , map_add' := , map_zero' := }
        Instances For
          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.

          Equations
          • ϕ.restrict h = { toFun := fun (t : τ) => Set.MapsTo.restrict (ϕ.toFun t) s s , cont' := , map_add' := , map_zero' := }
          Instances For
            theorem Flow.isInvariant_iff_image_eq {τ : Type u_1} [AddCommGroup τ] [TopologicalSpace τ] [TopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (s : Set α) :
            IsInvariant ϕ.toFun s ∀ (t : τ), ϕ.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.

            Equations
            • ϕ.reverse = { toFun := fun (t : τ) => ϕ.toFun (-t), cont' := , map_add' := , map_zero' := }
            Instances For
              theorem Flow.continuous_toFun {τ : Type u_1} [AddCommGroup τ] [TopologicalSpace τ] [TopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (t : τ) :
              Continuous (ϕ.toFun t)
              def Flow.toHomeomorph {τ : Type u_1} [AddCommGroup τ] [TopologicalSpace τ] [TopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (t : τ) :
              α ≃ₜ α

              The map ϕ t as a homeomorphism.

              Equations
              • ϕ.toHomeomorph t = { toFun := ϕ.toFun t, invFun := ϕ.toFun (-t), left_inv := , right_inv := , continuous_toFun := , continuous_invFun := }
              Instances For
                theorem Flow.image_eq_preimage {τ : Type u_1} [AddCommGroup τ] [TopologicalSpace τ] [TopologicalAddGroup τ] {α : Type u_2} [TopologicalSpace α] (ϕ : Flow τ α) (t : τ) (s : Set α) :
                ϕ.toFun t '' s = ϕ.toFun (-t) ⁻¹' s