Theory Missing_Topology

(*
    Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section ‹Some useful lemmas in topology›

theory Missing_Topology imports "HOL-Analysis.Multivariate_Analysis"
begin

subsection ‹Misc›    
 
lemma open_times_image:
  fixes S::"'a::real_normed_field set"
  assumes "open S" "c0"
  shows "open (((*) c) ` S)" 
proof -
  let ?f = "λx. x/c" and ?g="((*) c)"
  have "continuous_on UNIV ?f" using c0 by (auto intro:continuous_intros)
  then have "open (?f -` S)" using open S by (auto elim:open_vimage)
  moreover have "?g ` S = ?f -` S" using c0
    using image_iff by fastforce
  ultimately show ?thesis by auto
qed   
 
lemma image_linear_greaterThan:
  fixes x::"'a::linordered_field"
  assumes "c0"
  shows "((λx. c*x+b) ` {x<..}) = (if c>0 then {c*x+b <..} else {..< c*x+b})"
using c0
  apply (auto simp add:image_iff field_simps)    
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
done

lemma image_linear_lessThan:
  fixes x::"'a::linordered_field"
  assumes "c0"
  shows "((λx. c*x+b) ` {..<x}) = (if c>0 then {..<c*x+b} else {c*x+b<..})"
using c0
  apply (auto simp add:image_iff field_simps)    
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
  subgoal for y by (rule bexI[where x="(y-b)/c"],auto simp add:field_simps)
done    
 
lemma continuous_on_neq_split:
  fixes f :: "'a::linear_continuum_topology  'b::linorder_topology"
  assumes "xs. f xy" "continuous_on s f" "connected s"
  shows "(xs. f x>y)  (xs. f x<y)"
  by (smt (verit) assms connectedD_interval connected_continuous_image imageE image_eqI leI) 

lemma
  fixes f::"'a::linorder_topology  'b::topological_space"
  assumes "continuous_on {a..b} f" "a<b"
  shows continuous_on_at_left:"continuous (at_left b) f" 
    and continuous_on_at_right:"continuous (at_right a) f"
  using assms continuous_on_Icc_at_leftD continuous_within apply blast
  using assms continuous_on_Icc_at_rightD continuous_within by blast
 
subsection ‹More about @{term eventually}    
    
lemma eventually_comp_filtermap:
    "eventually (P o f) F  eventually P (filtermap f F)"
  unfolding comp_def using eventually_filtermap by auto
 
lemma eventually_at_infinityI:
  fixes P::"'a::real_normed_vector  bool"
  assumes "x. c  norm x  P x"
  shows "eventually P at_infinity"  
unfolding eventually_at_infinity using assms by auto
   
lemma eventually_at_bot_linorderI:
  fixes c::"'a::linorder"
  assumes "x. x  c  P x"
  shows "eventually P at_bot"
  using assms by (auto simp: eventually_at_bot_linorder)     

subsection ‹More about @{term filtermap} 

lemma filtermap_linear_at_within:
  assumes "bij f" and cont: "isCont f a" and open_map: "S. open S  open (f`S)"
  shows "filtermap f (at a within S) = at (f a) within f`S"
  unfolding filter_eq_iff
proof safe
  fix P
  assume "eventually P (filtermap f (at a within S))"
  then obtain T where "open T" "a  T" and impP:"xT. xa  xS P (f x)"
    by (auto simp: eventually_filtermap eventually_at_topological)
  then show "eventually P (at (f a) within f ` S)"
    unfolding eventually_at_topological
    apply (intro exI[of _ "f`T"])
    using bij f open_map by (metis bij_pointE imageE imageI)  
next
  fix P
  assume "eventually P (at (f a) within f ` S)"
  then obtain T1 where "open T1" "f a  T1" and impP:"xT1. xf a  xf`S P (x)"
    unfolding eventually_at_topological by auto
  then obtain T2 where "open T2" "a  T2" "(x'T2. f x'  T1)" 
    using cont[unfolded continuous_at_open,rule_format,of T1] by blast 
  then have "xT2. xa  xS P (f x)"
    using impP by (metis assms(1) bij_pointE imageI)
  then show "eventually P (filtermap f (at a within S))" 
    unfolding eventually_filtermap eventually_at_topological 
    apply (intro exI[of _ T2])
    using open T2 a  T2 by auto
qed
  
lemma filtermap_at_bot_linear_eq:
  fixes c::"'a::linordered_field"
  assumes "c0"
  shows "filtermap (λx. x * c + b) at_bot = (if c>0 then at_bot else at_top)"
proof (cases "c>0")
  case True
  then have "filtermap (λx. x * c + b) at_bot = at_bot" 
    apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"])
    subgoal unfolding eventually_at_bot_linorder filterlim_at_bot
      by (auto simp add: field_simps)
    subgoal unfolding eventually_at_bot_linorder filterlim_at_bot
      by (metis mult.commute real_affinity_le)
    by auto
  then show ?thesis using c>0 by auto
next
  case False
  then have "c<0" using c0 by auto
  then have "filtermap (λx. x * c + b) at_bot = at_top"
    apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"])
    subgoal unfolding eventually_at_top_linorder filterlim_at_bot
      by (meson le_diff_eq neg_divide_le_eq)
    subgoal unfolding eventually_at_bot_linorder filterlim_at_top
      using c < 0 by (meson False diff_le_eq le_divide_eq)
    by auto
  then show ?thesis using c<0 by auto
qed  
  
lemma filtermap_linear_at_left:
  fixes c::"'a::{linordered_field,linorder_topology,real_normed_field}"
  assumes "c0"
  shows "filtermap (λx. c*x+b) (at_left x) = (if c>0 then at_left (c*x+b) else at_right (c*x+b))"
proof -
  let ?f = "λx. c*x+b"
  have "filtermap (λx. c*x+b) (at_left x) = (at (?f x) within ?f ` {..<x})"
  proof (subst filtermap_linear_at_within)
    show "bij ?f" using c0 
      by (auto intro!: o_bij[of "λx. (x-b)/c"])
    show "isCont ?f x" by auto
    show "S. open S  open (?f ` S)" 
      using open_times_image[OF _ c0,THEN open_translation,of _ b]  
      by (simp add:image_image add.commute)
    show "at (?f x) within ?f ` {..<x} = at (?f x) within ?f ` {..<x}" by simp
  qed
  moreover have "?f ` {..<x} =  {..<?f x}" when "c>0" 
    using image_linear_lessThan[OF c0,of b x] that by auto
  moreover have "?f ` {..<x} =  {?f x<..}" when "¬ c>0" 
    using image_linear_lessThan[OF c0,of b x] that by auto
  ultimately show ?thesis by auto
qed
    
lemma filtermap_linear_at_right:
  fixes c::"'a::{linordered_field,linorder_topology,real_normed_field}"
  assumes "c0"
  shows "filtermap (λx. c*x+b) (at_right x) = (if c>0 then at_right (c*x+b) else at_left (c*x+b))" 
proof -
  let ?f = "λx. c*x+b"
  have "filtermap ?f (at_right x) = (at (?f x) within ?f ` {x<..})"
  proof (subst filtermap_linear_at_within)
    show "bij ?f" using c0 
      by (auto intro!: o_bij[of "λx. (x-b)/c"])
    show "isCont ?f x" by auto
    show "S. open S  open (?f ` S)" 
      using open_times_image[OF _ c0,THEN open_translation,of _ b]  
      by (simp add:image_image add.commute)
    show "at (?f x) within ?f ` {x<..} = at (?f x) within ?f ` {x<..}" by simp
  qed
  moreover have "?f ` {x<..} =  {?f x<..}" when "c>0" 
    using image_linear_greaterThan[OF c0,of b x] that by auto
  moreover have "?f ` {x<..} =  {..<?f x}" when "¬ c>0" 
    using image_linear_greaterThan[OF c0,of b x] that by auto
  ultimately show ?thesis by auto
qed
 
lemma filtermap_at_top_linear_eq:
  fixes c::"'a::linordered_field"
  assumes "c0"
  shows "filtermap (λx. x * c + b) at_top = (if c>0 then at_top else at_bot)"
proof (cases "c>0")
  case True
  then have "filtermap (λx. x * c + b) at_top = at_top" 
    apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"])
    subgoal unfolding eventually_at_top_linorder filterlim_at_top 
      by (meson le_diff_eq pos_le_divide_eq)
    subgoal unfolding eventually_at_top_linorder filterlim_at_top
      apply auto
      by (metis mult.commute real_le_affinity) 
    by auto
  then show ?thesis using c>0 by auto
next
  case False
  then have "c<0" using c0 by auto
  then have "filtermap (λx. x * c + b) at_top = at_bot"
    apply (intro filtermap_fun_inverse[of "λx. (x-b) / c"])
    subgoal unfolding eventually_at_bot_linorder filterlim_at_top
      by (auto simp add: field_simps)
    subgoal unfolding eventually_at_top_linorder filterlim_at_bot
      by (meson le_diff_eq neg_divide_le_eq)
    by auto
  then show ?thesis using c<0 by auto
qed

subsection ‹More about @{term filterlim}
  
lemma filterlim_at_top_linear_iff:
  fixes f::"'a::linordered_field  'b"
  assumes "c0"
  shows "(LIM x at_top. f (x * c + b) :> F2)  (if c>0 then (LIM x at_top. f x :> F2) 
            else (LIM x at_bot. f x :> F2))"
  unfolding filterlim_def
  apply (subst filtermap_filtermap[of f "λx. x * c + b",symmetric])
  using assms by (auto simp add:filtermap_at_top_linear_eq)
    
lemma filterlim_at_bot_linear_iff:
  fixes f::"'a::linordered_field  'b"
  assumes "c0"
  shows "(LIM x at_bot. f (x * c + b) :> F2)  (if c>0 then (LIM x at_bot. f x :> F2) 
            else (LIM x at_top. f x :> F2)) "
  unfolding filterlim_def 
  apply (subst filtermap_filtermap[of f "λx. x * c + b",symmetric])
  using assms by (auto simp add:filtermap_at_bot_linear_eq)      
  
  
lemma filterlim_tendsto_add_at_top_iff:
  assumes f: "(f  c) F"
  shows "(LIM x F. (f x + g x :: real) :> at_top)  (LIM x F. g x :> at_top)"
proof     
  assume "LIM x F. f x + g x :> at_top" 
  moreover have "((λx. - f x)  - c) F"
    using f by (intro tendsto_intros,simp)
  ultimately show "filterlim g at_top F" using filterlim_tendsto_add_at_top 
    by fastforce
qed (auto simp add:filterlim_tendsto_add_at_top[OF f])    
    
  
lemma filterlim_tendsto_add_at_bot_iff:
  fixes c::real
  assumes f: "(f  c) F"
  shows "(LIM x F. f x + g x :> at_bot)  (LIM x F. g x :> at_bot)" 
proof -
  have "(LIM x F. f x + g x :> at_bot) 
          (LIM x F. - f x + (- g x)  :> at_top)"
    apply (subst filterlim_uminus_at_top)
    by (rule filterlim_cong,auto)
  also have "... = (LIM x F. - g x  :> at_top)"
    apply (subst filterlim_tendsto_add_at_top_iff[of _ "-c"])
    by (auto intro:tendsto_intros simp add:f)
  also have "... = (LIM x F. g x  :> at_bot)"
    apply (subst filterlim_uminus_at_top)
    by (rule filterlim_cong,auto)
  finally show ?thesis .
qed
  
lemma tendsto_inverse_0_at_infinity: 
    "LIM x F. f x :> at_infinity  ((λx. inverse (f x) :: real)  0) F"
  by (metis filterlim_at filterlim_inverse_at_iff)

(*
lemma filterlim_at_top_tendsto[elim]:
  fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
  assumes top:"filterlim f at_top F" and tendsto: "(f ⤏ c) F" 
          and "F≠bot"
  shows False
proof -
  obtain cc where "cc>c" using gt_ex by blast
  have "∀F x in F. cc < f x" 
    using top unfolding filterlim_at_top_dense by auto
  moreover have "∀F x in F. f x < cc" 
    using tendsto order_tendstoD(2)[OF _ ‹cc>c›] by auto
  ultimately have "∀F x in F. cc < f x ∧ f x < cc" 
    using eventually_conj by auto
  then have "∀F x in F. False" by (auto elim:eventually_mono)
  then show False using ‹F≠bot› by auto
qed

lemma filterlim_at_bot_tendsto[elim]:
  fixes f::"'a ⇒ 'b::{unbounded_dense_linorder,order_topology}" and F::"'a filter"
  assumes top:"filterlim f at_bot F" and tendsto: "(f ⤏ c) F" 
          and "F≠bot"
  shows False
proof -
  obtain cc where "cc<c" using lt_ex by blast
  have "∀F x in F. cc > f x" 
    using top unfolding filterlim_at_bot_dense by auto
  moreover have "∀F x in F. f x > cc" 
    using tendsto order_tendstoD(1)[OF _ ‹cc<c›] by auto
  ultimately have "∀F x in F. cc < f x ∧ f x < cc" 
    using eventually_conj by auto
  then have "∀F x in F. False" by (auto elim:eventually_mono)
  then show False using ‹F≠bot› by auto
qed
*)
  
end