LaSalle's invariance principle

TheoremOmega-limit set lies in every closed set containing the orbit#✓fully proved

The ω-limit set of a point under a semiflow is contained in every closed set that contains the forward orbit.

theorem omegaLimit_singleton_subset_of_isClosed (ϕ : Flow ℝ≥0 X) {x : X} {K : Set X}
    (hK : IsClosed K) (hxK : ∀ t, ϕ t x ∈ K) : ω⁺ ϕ {x} ⊆ K

Used by 1

Used byLaSalle's invariance principle

TheoremV is constant on the ω-limit set#✓fully proved

If the forward orbit of x lies in a compact set K and the continuous function V is nonincreasing along it, then there is a constant c (the limit of V(ϕ t x)) such that V(ϕ t y) = c for every y ∈ ω⁺(x) and every t ≥ 0.

theorem exists_forall_eq_of_mem_omegaLimit (ϕ : Flow ℝ≥0 X) {V : X → ℝ}
    (hV : Continuous V) {x : X} {K : Set X} (hK : IsCompact K) (hxK : ∀ t, ϕ t x ∈ K)
    (hanti : Antitone fun t => V (ϕ t x)) :
    ∃ c : ℝ, ∀ y ∈ ω⁺ ϕ {x}, ∀ t, V (ϕ t y) = c

Used by 1

Used byLaSalle's invariance principle

TheoremLaSalle's invariance principle#✓fully proved

LaSalle's invariance principle (LaSalle 1960; Khalil 2002, Theorem 4.4). Let the forward orbit of x under the semiflow ϕ lie in a compact set K, let V be continuous and nonincreasing along that orbit, and let E contain every y ∈ K whose orbit keeps V constant. Then the ω-limit set ω⁺(x) is nonempty and contained in the largest forward-invariant subset M = {y | ∀ t, ϕ t y ∈ E} of E, and the orbit of x eventually enters every open set containing M.

theorem lasalle [T2Space X] (ϕ : Flow ℝ≥0 X) {V : X → ℝ} (hV : Continuous V) {x : X}
    {K E : Set X} (hK : IsCompact K) (hxK : ∀ t, ϕ t x ∈ K)
    (hanti : Antitone fun t => V (ϕ t x))
    (hE : ∀ y ∈ K, (∀ t, V (ϕ t y) = V y) → y ∈ E) :
    (ω⁺ ϕ {x}).Nonempty ∧ ω⁺ ϕ {x} ⊆ {y | ∀ t, ϕ t y ∈ E} ∧
      ∀ U : Set X, IsOpen U → {y | ∀ t, ϕ t y ∈ E} ⊆ U → ∀ᶠ t in atTop, ϕ t x ∈ U

Uses 2

Proof usesV is constant on the ω-limit set · Omega-limit set lies in every closed set containing the orbit

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.