Theory Poincare_Bendixson.Limit_Set
section ‹Limit Sets›
theory Limit_Set
imports Invariance
begin
context auto_ll_on_open begin
text ‹Positive limit point, assuming ‹{0..} ⊆ existence_ivl0 x››
definition "ω_limit_point x p ⟷
{0..} ⊆ existence_ivl0 x ∧
(∃s. s ⇢⇘⇙ ∞ ∧ (flow0 x ∘ s) ⇢ p)"
text ‹ Also called the ‹ω›-limit set of x ›
definition "ω_limit_set x = {p. ω_limit_point x p}"
definition "α_limit_point x p ⟷
{..0} ⊆ existence_ivl0 x ∧
(∃s. s ⇢⇘⇙ -∞ ∧ (flow0 x ∘ s) ⇢ p)"
text ‹ Also called the ‹α›-limit set of x ›
definition "α_limit_set x =
{p. α_limit_point x p}"
end context auto_ll_on_open begin
lemma α_limit_point_eq_rev: "α_limit_point x p = rev.ω_limit_point x p"
unfolding α_limit_point_def rev.ω_limit_point_def
apply (auto simp: rev_eq_flow[abs_def] o_def filterlim_uminus_at_bot rev_existence_ivl_eq0 subset_iff
intro: exI[where x="uminus o s" for s])
using neg_0_le_iff_le by fastforce
lemma α_limit_set_eq_rev: "α_limit_set x = rev.ω_limit_set x"
unfolding α_limit_set_def rev.ω_limit_set_def α_limit_point_eq_rev ..
lemma ω_limit_pointE:
assumes "ω_limit_point x p"
obtains s where
"filterlim s at_top sequentially"
"(flow0 x ∘ s) ⇢ p"
"∀n. b ≤ s n"
using assms filterlim_at_top_choose_lower ω_limit_point_def by blast
lemma ω_limit_set_eq:
assumes "{0..} ⊆ existence_ivl0 x"
shows "ω_limit_set x = (INF τ ∈ {0..}. closure (flow0 x ` {τ..}))"
unfolding ω_limit_set_def
proof safe
fix p t
assume pt: "0 ≤ (t::real)" "ω_limit_point x p"
from ω_limit_pointE[OF pt(2)]
obtain s where
"filterlim s at_top sequentially"
"(flow0 x ∘ s) ⇢ p"
"∀n. t ≤ s n" by blast
thus "p ∈ closure (flow0 x ` {t..})" unfolding closure_sequential
by (metis atLeast_iff comp_apply imageI)
next
fix p
assume "p ∈ (⋂τ∈{0..}. closure (flow0 x ` {τ..}))"
then have "⋀t. t ≥0 ⟹ p ∈ closure (flow0 x ` {t..})" by blast
then have "⋀t e. t ≥0 ⟹ e > 0 ⟹ (∃tt ≥ t. dist (flow0 x tt) p < e)"
unfolding closure_approachable
by fastforce
from approachable_sequenceE[OF this]
obtain s where "filterlim s at_top sequentially" "(flow0 x ∘ s) ⇢ p" by auto
thus "ω_limit_point x p" unfolding ω_limit_point_def using assms by auto
qed
lemma ω_limit_set_empty:
assumes "¬ ({0..} ⊆ existence_ivl0 x)"
shows "ω_limit_set x = {}"
unfolding ω_limit_set_def ω_limit_point_def
by (simp add: assms)
lemma ω_limit_set_closed: "closed (ω_limit_set x)"
using ω_limit_set_eq
by (metis ω_limit_set_empty closed_INT closed_closure closed_empty)
lemma ω_limit_set_positively_invariant:
shows "positively_invariant (ω_limit_set x)"
unfolding positively_invariant_def trapped_forward_def
proof safe
fix dummy p t
assume xa: "p ∈ ω_limit_set x"
"t ∈ existence_ivl0 p"
"0 ≤ t"
have "p ∈ X" using mem_existence_ivl_iv_defined(2) xa(2) by blast
have exist: "{0..} ⊆ existence_ivl0 x" using xa(1)
unfolding ω_limit_set_def ω_limit_point_def by auto
from xa(1)
obtain s where s:
"filterlim s at_top sequentially"
"(flow0 x ∘ s) ⇢ p"
"∀n. 0 ≤ s n"
unfolding ω_limit_set_def by (auto elim!:ω_limit_pointE)
define r where "r = (λn. t + s n)"
have rlim: "filterlim r at_top sequentially" unfolding r_def
by (auto intro: filterlim_tendsto_add_at_top[OF _ s(1)])
define dom where "dom = image (flow0 x) {0..} ∪ {p} "
have domin: "∀n. (flow0 x ∘ s) n ∈ dom" "p ∈ dom" unfolding dom_def o_def
using exist by(auto simp add: s(3))
have xt: "⋀x. x ∈ dom ⟹ t ∈ existence_ivl0 x" unfolding dom_def using xa(2)
apply auto
apply (rule existence_ivl_trans')
using exist xa(3) apply auto[1]
using exist by auto
have cont: "continuous_on dom (λx. flow0 x t)"
apply (rule flow_continuous_on_compose)
apply auto
using ‹p ∈ X› exist local.dom_def local.flow_in_domain apply auto[1]
using xt .
then have f1: "((λx. flow0 x t) ∘ (flow0 x ∘ s)) ⇢ flow0 p t" using domin s(2)
unfolding continuous_on_sequentially
by blast
have ff:"⋀n. (flow0 x ∘ r) n = ((λx. flow0 x t) ∘ (flow0 x ∘ s)) n"
unfolding o_def r_def
proof -
fix n
have s:"s n ∈ existence_ivl0 x"
using s(3) exist by auto
then have t:"t ∈ existence_ivl0 (flow0 x (s n))"
using domin(1) xt by auto
from flow_trans[OF s t]
show "flow0 x (t + s n) = flow0 (flow0 x (s n)) t"
by (simp add: add.commute)
qed
have f2: "(flow0 x ∘ r) ⇢ flow0 p t" using f1 unfolding ff .
show "flow0 p t ∈ ω_limit_set x" using exist f2 rlim
unfolding ω_limit_set_def ω_limit_point_def
using flow_in_domain r_def s(3) xa(2) xa(3) by auto
qed
lemma ω_limit_set_invariant:
shows "invariant (ω_limit_set x)"
unfolding invariant_iff_pos_invariant_and_compl_pos_invariant
proof safe
show "positively_invariant (ω_limit_set x)"
using ω_limit_set_positively_invariant .
next
show "positively_invariant (X - ω_limit_set x)"
unfolding positively_invariant_def trapped_forward_def
apply safe
using local.flow_in_domain apply blast
proof -
fix dummy p t
assume xa: "p ∈ X" "p ∉ ω_limit_set x"
"t ∈ existence_ivl0 p" "0 ≤ t"
and f: "flow0 p t ∈ ω_limit_set x"
have exist: "{0..} ⊆ existence_ivl0 x" using f
unfolding ω_limit_set_def ω_limit_point_def by auto
from f
obtain s where s:
"filterlim s at_top sequentially"
"(flow0 x ∘ s) ⇢ flow0 p t"
"∀n. t ≤ s n"
unfolding ω_limit_set_def by (auto elim!:ω_limit_pointE)
define r where "r = (λn. (-t) + s n)"
have "(λx. -t) ⇢ -t" by simp
from filterlim_tendsto_add_at_top[OF this s(1)]
have rlim: "filterlim r at_top sequentially" unfolding r_def by simp
define dom where "dom = image (flow0 x) {t..} ∪ {flow0 p t} "
have domin: "∀n. (flow0 x ∘ s) n ∈ dom" "flow0 p t ∈ dom" unfolding dom_def o_def
using exist by(auto simp add: s(3))
have xt: "⋀x. x ∈ dom ⟹ -t ∈ existence_ivl0 x" unfolding dom_def using xa(2)
apply auto
using local.existence_ivl_reverse xa(3) apply auto[1]
by (metis exist atLeast_iff diff_conv_add_uminus diff_ge_0_iff_ge linordered_ab_group_add_class.zero_le_double_add_iff_zero_le_single_add local.existence_ivl_trans' order_trans subset_iff xa(4))
have cont: "continuous_on dom (λx. flow0 x (-t))"
apply (rule flow_continuous_on_compose)
apply auto
using local.mem_existence_ivl_iv_defined(2) xt apply blast
by (simp add: xt)
then have f1: "((λx. flow0 x (-t)) ∘ (flow0 x ∘ s)) ⇢ flow0 (flow0 p t) (-t)" using domin s(2)
unfolding continuous_on_sequentially
by blast
have ff:"⋀n. (flow0 x ∘ r) n = ((λx. flow0 x (-t)) ∘ (flow0 x ∘ s)) n"
unfolding o_def r_def
proof -
fix n
have s:"s n ∈ existence_ivl0 x"
using s(3) exist ‹0≤ t› by (meson atLeast_iff order_trans subset_eq)
then have t:"-t ∈ existence_ivl0 (flow0 x (s n))"
using domin(1) xt by auto
from flow_trans[OF s t]
show "flow0 x (-t + s n) = flow0 (flow0 x (s n)) (-t)"
by (simp add: add.commute)
qed
have "(flow0 x ∘ r) ⇢ flow0 (flow0 p t) (-t)" using f1 unfolding ff .
then have f2: "(flow0 x ∘ r) ⇢ p" using flows_reverse xa(3) by auto
then have "p ∈ ω_limit_set x" unfolding ω_limit_set_def ω_limit_point_def
using rlim exist by auto
thus False using xa(2) by auto
qed
qed
end context auto_ll_on_open begin
lemma α_limit_set_eq:
assumes "{..0} ⊆ existence_ivl0 x"
shows "α_limit_set x = (INF τ ∈ {..0}. closure (flow0 x ` {..τ}))"
using rev.ω_limit_set_eq[of x, OF assms[folded infinite_rev_existence_ivl0_rewrites]]
unfolding α_limit_set_eq_rev rev_flow_image_eq image_uminus_atLeast
by (smt INT_extend_simps(10) Sup.SUP_cong image_uminus_atMost)
lemma α_limit_set_closed:
shows "closed (α_limit_set x)"
unfolding α_limit_set_eq_rev by (rule rev.ω_limit_set_closed)
lemma α_limit_set_positively_invariant:
shows "negatively_invariant (α_limit_set x)"
unfolding negatively_invariant_eq_rev α_limit_set_eq_rev
by (simp add: rev.ω_limit_set_positively_invariant)
lemma α_limit_set_invariant:
shows "invariant (α_limit_set x)"
unfolding invariant_eq_rev α_limit_set_eq_rev
by (simp add: rev.ω_limit_set_invariant)
text ‹ Fundamental properties of the positive limit set ›
context
fixes x K
assumes K: "compact K" "K ⊆ X"
assumes x: "x ∈ X" "trapped_forward x K"
begin
text ‹Bunch of facts for what's to come›
private lemma props:
shows "{0..} ⊆ existence_ivl0 x" "seq_compact K"
apply (rule trapped_sol_right)
using x K by (auto simp add: compact_imp_seq_compact)
private lemma flowimg:
shows "flow0 x ` (existence_ivl0 x ∩ {0..}) = flow0 x ` {0..}"
using props(1) by auto
lemma ω_limit_set_in_compact_subset:
shows "ω_limit_set x ⊆ K"
unfolding ω_limit_set_def
proof safe
fix p s
assume "ω_limit_point x p"
from ω_limit_pointE[OF this]
obtain s where s:
"filterlim s at_top sequentially"
"(flow0 x ∘ s) ⇢ p"
"∀n. 0 ≤ s n" by blast
then have fin: "∀n. (flow0 x ∘ s) n ∈ K" using s(3) x K props(1)
unfolding trapped_forward_def
by (simp add: subset_eq)
from seq_compactE[OF props(2) fin]
show "p ∈ K" using s(2)
by (metis LIMSEQ_subseq_LIMSEQ LIMSEQ_unique)
qed
lemma ω_limit_set_in_compact_compact:
shows "compact (ω_limit_set x)"
proof -
from ω_limit_set_in_compact_subset
have "bounded (ω_limit_set x)"
using bounded_subset compact_imp_bounded
using K(1) by auto
thus ?thesis using ω_limit_set_closed
by (simp add: compact_eq_bounded_closed)
qed
lemma ω_limit_set_in_compact_nonempty:
shows "ω_limit_set x ≠ {}"
proof -
have fin: "∀n. (flow0 x ∘ real) n ∈ K" using x K props(1)
by (simp add: flowimg image_subset_iff trapped_forward_def)
from seq_compactE[OF props(2) this]
obtain r l where "l ∈ K" "strict_mono r" "(flow0 x ∘ real ∘ r) ⇢ l" by blast
then have "ω_limit_point x l" unfolding ω_limit_point_def using props(1)
by (smt comp_def filterlim_sequentially_iff_filterlim_real filterlim_subseq tendsto_at_top_eq_left)
thus ?thesis unfolding ω_limit_set_def by auto
qed
lemma ω_limit_set_in_compact_existence:
shows "⋀y. y ∈ ω_limit_set x ⟹ existence_ivl0 y = UNIV"
proof -
fix y
assume y: "y ∈ ω_limit_set x"
then have "y ∈ X" using ω_limit_set_in_compact_subset K by blast
from ω_limit_set_invariant
have "⋀t. t ∈ existence_ivl0 y ⟹ flow0 y t ∈ ω_limit_set x"
unfolding invariant_def trapped_iff_on_existence_ivl0 using y by blast
then have t: "⋀t. t ∈ existence_ivl0 y ⟹ flow0 y t ∈ K"
using ω_limit_set_in_compact_subset by blast
thus "existence_ivl0 y = UNIV"
by (meson ‹y ∈ X› existence_ivl_zero existence_ivl_initial_time_iff existence_ivl_subset mem_compact_implies_subset_existence_interval subset_antisym K)
qed
lemma ω_limit_set_in_compact_tendsto:
shows "((λt. infdist (flow0 x t) (ω_limit_set x)) ⤏ 0) at_top"
proof (rule ccontr)
assume "¬ ((λt. infdist (flow0 x t) (ω_limit_set x)) ⤏ 0) at_top"
from not_tendsto_frequentlyE[OF this]
obtain S where S: "open S" "0 ∈ S"
"∃⇩F t in at_top. infdist (flow0 x t) (ω_limit_set x) ∉ S" .
then obtain e where "e > 0" "ball 0 e ⊆ S" using openE by blast
then have "⋀x. x ≥0 ⟹ x ∉ S ⟹ x ≥ e" by force
then have "∀xa. infdist (flow0 x xa) (ω_limit_set x) ∉ S ⟶
infdist (flow0 x xa) (ω_limit_set x) ≥ e" using infdist_nonneg by blast
from frequently_mono[OF this S(3)]
have "∃⇩F t in at_top. infdist (flow0 x t) (ω_limit_set x) ≥ e" by blast
then have "∀n. ∃⇩F t in at_top. infdist (flow0 x t) (ω_limit_set x) ≥ e ∧ real n ≤ t"
by (auto intro!: eventually_frequently_conj)
from frequently_at_topE[OF this]
obtain s where s: "⋀i. e ≤ infdist (flow0 x (s i)) (ω_limit_set x)"
"⋀i. real i ≤ s i" "strict_mono s" by force
then have sf: "filterlim s at_top sequentially"
using filterlim_at_top_mono filterlim_real_sequentially not_eventuallyD by blast
have fin: "∀n. (flow0 x ∘ s) n ∈ K" using x K props(1) s unfolding flowimg trapped_forward_def
by (metis atLeast_iff comp_apply image_subset_iff of_nat_0_le_iff order_trans)
from seq_compactE[OF props(2) this]
obtain r l where r:"strict_mono r" and l: "l ∈ K" "(flow0 x ∘ s ∘ r) ⇢ l" by blast
moreover from filterlim_at_top_strict_mono[OF s(3) r(1) sf]
have "filterlim (s ∘ r) at_top sequentially" .
moreover have "ω_limit_point x l" unfolding ω_limit_point_def using props(1) calculation
by (metis comp_assoc)
ultimately have "infdist l (ω_limit_set x) = 0" by (simp add: ω_limit_set_def)
then have c1:"((λy. infdist y (ω_limit_set x)) ∘ (flow0 x ∘ s ∘ r)) ⇢ 0"
by (auto intro!: tendsto_compose_at[OF l(2)] tendsto_eq_intros)
have c2: "⋀i. e ≤ infdist (flow0 x ((s ∘ r) i)) (ω_limit_set x)" using s(1) by simp
show False using c1 c2 ‹e > 0› unfolding o_def
using Lim_bounded2
by (metis (no_types, lifting) ball_eq_empty centre_in_ball empty_iff)
qed
lemma ω_limit_set_in_compact_connected:
shows "connected (ω_limit_set x)"
unfolding connected_closed_set[OF ω_limit_set_closed]
proof clarsimp
fix Apre Bpre
assume pre: "closed Apre" "Apre ∪ Bpre = ω_limit_set x" "closed Bpre"
"Apre ≠ {}" "Bpre ≠ {}" "Apre ∩ Bpre = {}"
then obtain A B where "Apre ⊆ A" "Bpre ⊆ B" "open A" "open B" and disj:"A ∩ B = {}"
by (meson t4_space)
then have "ω_limit_set x ⊆ A ∪ B"
"ω_limit_set x ∩ A ≠ {}" "ω_limit_set x ∩ B ≠ {}" using pre by auto
then obtain p q where
p: "ω_limit_point x p" "p ∈ A"
and q: "ω_limit_point x q" "q ∈ B"
using ω_limit_set_def by auto
from ω_limit_pointE[OF p(1)]
obtain ps where ps: "filterlim ps at_top sequentially"
"(flow0 x ∘ ps) ⇢ p" "∀n. 0 ≤ ps n" by blast
from ω_limit_pointE[OF q(1)]
obtain qs where qs: "filterlim qs at_top sequentially"
"(flow0 x ∘ qs) ⇢ q" "∀n. 0 ≤ qs n" by blast
have "∀n. ∃⇩F t in at_top. flow0 x t ∉ A ∧ flow0 x t ∉ B" unfolding frequently_at_top
proof safe
fix dummy mpre
obtain m where "m ≥ (0::real)" "m > mpre"
by (meson approximation_preproc_push_neg(1) gt_ex le_cases order_trans)
from ps obtain a where a:"a > m" "(flow0 x a) ∈ A"
using ‹open A› p unfolding tendsto_def filterlim_at_top eventually_sequentially
by (metis approximation_preproc_push_neg(1) comp_apply gt_ex le_cases order_trans)
from qs obtain b where b:"b > a" "(flow0 x b) ∈ B"
using ‹open B› q unfolding tendsto_def filterlim_at_top eventually_sequentially
by (metis approximation_preproc_push_neg(1) comp_apply gt_ex le_cases order_trans)
have "continuous_on {a..b} (flow0 x)"
by (metis Icc_subset_Ici_iff ‹0 ≤ m› ‹m < a› approximation_preproc_push_neg(2) atMost_iff atMost_subset_iff continuous_on_subset le_cases local.flow_continuous_on props(1) subset_eq)
from connected_continuous_image[OF this connected_Icc]
have c:"connected (flow0 x ` {a..b})" .
have "∃t∈ {a..b}. flow0 x t ∉ A ∧ flow0 x t ∉ B"
proof (rule ccontr)
assume "¬ (∃t∈{a..b}. flow0 x t ∉ A ∧ flow0 x t ∉ B)"
then have "flow0 x ` {a..b} ⊆ A ∪ B" by blast
from topological_space_class.connectedD[OF c ‹open A› ‹open B› _ this]
show False using a b disj by force
qed
thus "∃n>mpre. flow0 x n ∉ A ∧ flow0 x n ∉ B"
by (smt ‹mpre < m› a(1) atLeastAtMost_iff)
qed
from frequently_at_topE'[OF this filterlim_real_sequentially]
obtain s where s: "∀i. flow0 x (s i) ∉ A ∧ flow0 x (s i) ∉ B"
"strict_mono s" "⋀n. real n ≤ s n" by blast
then have "∀n. (flow0 x ∘ s) n ∈ K"
by (smt atLeast_iff comp_apply flowimg image_subset_iff of_nat_0_le_iff trapped_forward_def x(2))
from seq_compactE[OF props(2) this]
obtain r l where r: "l ∈ K" "strict_mono r" "(flow0 x ∘ s ∘ r) ⇢ l" by blast
have "filterlim s at_top sequentially"
using s filterlim_at_top_mono filterlim_real_sequentially not_eventuallyD by blast
from filterlim_at_top_strict_mono[OF s(2) r(2) this]
have "filterlim (s ∘ r) at_top sequentially" .
then have "ω_limit_point x l" unfolding ω_limit_point_def using props(1) r
by (metis comp_assoc)
moreover have "l ∉ A" using s(1) r(3) ‹open A› unfolding tendsto_def by auto
moreover have "l ∉ B" using s(1) r(3) ‹open B› unfolding tendsto_def by auto
ultimately show False using ‹ω_limit_set x ⊆ A ∪ B› unfolding ω_limit_set_def
by auto
qed
lemma ω_limit_set_in_compact_ω_limit_set_contained:
shows "∀y ∈ ω_limit_set x. ω_limit_set y ⊆ ω_limit_set x"
proof safe
fix y z
assume "y ∈ ω_limit_set x" "z ∈ ω_limit_set y"
then have "ω_limit_point y z" unfolding ω_limit_set_def by auto
from ω_limit_pointE[OF this]
obtain s where s: "(flow0 y ∘ s) ⇢ z" .
have "∀n. (flow0 y ∘ s) n ∈ ω_limit_set x"
using ‹y ∈ ω_limit_set x› invariant_def
ω_limit_set_in_compact_existence ω_limit_set_invariant trapped_iff_on_existence_ivl0
by force
thus "z ∈ ω_limit_set x" using closed_sequential_limits s ω_limit_set_closed
by blast
qed
lemma ω_limit_set_in_compact_α_limit_set_contained:
assumes zpx: "z ∈ ω_limit_set x"
shows "α_limit_set z ⊆ ω_limit_set x"
proof
fix w assume "w ∈ α_limit_set z"
then obtain s where s: "(flow0 z ∘ s) ⇢ w"
unfolding α_limit_set_def α_limit_point_def
by auto
from ω_limit_set_invariant have "invariant (ω_limit_set x)" .
then have "∀n. (flow0 z ∘ s) n ∈ ω_limit_set x"
using ω_limit_set_in_compact_existence[OF zpx] zpx
using invariant_def trapped_iff_on_existence_ivl0 by fastforce
from closed_sequentially[OF ω_limit_set_closed] this s
show "w ∈ ω_limit_set x"
by blast
qed
end
text ‹ Fundamental properties of the negative limit set ›
end context auto_ll_on_open begin
context
fixes x K
assumes x: "x ∈ X" "trapped_backward x K"
assumes K: "compact K" "K ⊆ X"
begin
private lemma xrev: "x ∈ X" "rev.trapped_forward x K"
using trapped_backward_iff_rev_trapped_forward x(2)
by (auto simp: rev_existence_ivl_eq0 rev_eq_flow x(1))
lemma α_limit_set_in_compact_subset: "α_limit_set x ⊆ K"
and α_limit_set_in_compact_compact: "compact (α_limit_set x)"
and α_limit_set_in_compact_nonempty: "α_limit_set x ≠ {}"
and α_limit_set_in_compact_connected: "connected (α_limit_set x)"
and α_limit_set_in_compact_α_limit_set_contained:
"∀y ∈ α_limit_set x. α_limit_set y ⊆ α_limit_set x"
and α_limit_set_in_compact_tendsto: "((λt. infdist (flow0 x t) (α_limit_set x)) ⤏ 0) at_bot"
using rev.ω_limit_set_in_compact_subset[OF K xrev]
using rev.ω_limit_set_in_compact_compact[OF K xrev]
using rev.ω_limit_set_in_compact_nonempty[OF K xrev]
using rev.ω_limit_set_in_compact_connected[OF K xrev]
using rev.ω_limit_set_in_compact_ω_limit_set_contained[OF K xrev]
using rev.ω_limit_set_in_compact_tendsto[OF K xrev]
unfolding invariant_eq_rev α_limit_set_eq_rev existence_ivl_eq_rev flow_eq_rev0 filterlim_at_bot_mirror
minus_minus
.
lemma α_limit_set_in_compact_existence:
shows "⋀y. y ∈ α_limit_set x ⟹ existence_ivl0 y = UNIV"
using rev.ω_limit_set_in_compact_existence[OF K xrev]
unfolding α_limit_set_eq_rev existence_ivl_eq_rev0
by auto
end
end
end