Theory 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