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›

(* TODO: Perhaps a more intrinsic definition would be better here *)
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)

(* TODO: Walter gives a more direct proof *)
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 = {}"
    (* TODO: this move is very strange *)
  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