Various lemmas for HOL-Analysis
authorManuel Eberl <eberlm@in.tum.de>
Sun Aug 20 03:35:20 2017 +0200 (23 months ago)
changeset 66456621897f47fab
parent 66455 158c513a39f5
child 66465 86223a532d8e
child 66466 aec5d9c88d69
Various lemmas for HOL-Analysis
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Extended_Real_Limits.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Set_Integral.thy
src/HOL/Analysis/Summation_Tests.thy
src/HOL/Limits.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Fri Aug 18 22:55:54 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Sun Aug 20 03:35:20 2017 +0200
     1.3 @@ -278,6 +278,21 @@
     1.4      by (metis open_ball \<open>\<xi> islimpt T\<close> centre_in_ball fT0 insertE insert_Diff islimptE)
     1.5  qed
     1.6  
     1.7 +corollary analytic_continuation_open:
     1.8 +  assumes "open s" "open s'" "s \<noteq> {}" "connected s'" "s \<subseteq> s'"
     1.9 +  assumes "f holomorphic_on s'" "g holomorphic_on s'" "\<And>z. z \<in> s \<Longrightarrow> f z = g z"
    1.10 +  assumes "z \<in> s'"
    1.11 +  shows   "f z = g z"
    1.12 +proof -
    1.13 +  from \<open>s \<noteq> {}\<close> obtain \<xi> where "\<xi> \<in> s" by auto
    1.14 +  with \<open>open s\<close> have \<xi>: "\<xi> islimpt s" 
    1.15 +    by (intro interior_limit_point) (auto simp: interior_open)
    1.16 +  have "f z - g z = 0"
    1.17 +    by (rule analytic_continuation[of "\<lambda>z. f z - g z" s' s \<xi>])
    1.18 +       (insert assms \<open>\<xi> \<in> s\<close> \<xi>, auto intro: holomorphic_intros)
    1.19 +  thus ?thesis by simp
    1.20 +qed
    1.21 +
    1.22  
    1.23  subsection\<open>Open mapping theorem\<close>
    1.24  
    1.25 @@ -3910,4 +3925,291 @@
    1.26    then show ?thesis unfolding c_def using w_def by auto
    1.27  qed
    1.28  
    1.29 +
    1.30 +subsection \<open>More facts about poles and residues\<close>
    1.31 +
    1.32 +lemma lhopital_complex_simple:
    1.33 +  assumes "(f has_field_derivative f') (at z)" 
    1.34 +  assumes "(g has_field_derivative g') (at z)"
    1.35 +  assumes "f z = 0" "g z = 0" "g' \<noteq> 0" "f' / g' = c"
    1.36 +  shows   "((\<lambda>w. f w / g w) \<longlongrightarrow> c) (at z)"
    1.37 +proof -
    1.38 +  have "eventually (\<lambda>w. w \<noteq> z) (at z)"
    1.39 +    by (auto simp: eventually_at_filter)
    1.40 +  hence "eventually (\<lambda>w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z)) = f w / g w) (at z)"
    1.41 +    by eventually_elim (simp add: assms divide_simps)
    1.42 +  moreover have "((\<lambda>w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z))) \<longlongrightarrow> f' / g') (at z)"
    1.43 +    by (intro tendsto_divide has_field_derivativeD assms)
    1.44 +  ultimately have "((\<lambda>w. f w / g w) \<longlongrightarrow> f' / g') (at z)"
    1.45 +    by (rule Lim_transform_eventually)
    1.46 +  with assms show ?thesis by simp
    1.47 +qed
    1.48 +
    1.49 +lemma porder_eqI:
    1.50 +  assumes "open s" "z \<in> s" "g holomorphic_on s" "g z \<noteq> 0" "n > 0"
    1.51 +  assumes "\<And>w. w \<in> s - {z} \<Longrightarrow> f w = g w / (w - z) ^ n"
    1.52 +  shows   "porder f z = n"
    1.53 +proof -
    1.54 +  define f' where "f' = (\<lambda>x. if x = z then 0 else inverse (f x))"
    1.55 +  define g' where "g' = (\<lambda>x. inverse (g x))"
    1.56 +  define s' where "s' = (g -` (-{0}) \<inter> s)"
    1.57 +  have "continuous_on s g"
    1.58 +    by (intro holomorphic_on_imp_continuous_on) fact
    1.59 +  hence "open s'"
    1.60 +    unfolding s'_def using assms by (subst (asm) continuous_on_open_vimage) blast+
    1.61 +  have s': "z \<in> s'" "g' holomorphic_on s'" "g' z \<noteq> 0" using assms 
    1.62 +    by (auto simp: s'_def g'_def intro!: holomorphic_intros)
    1.63 +  have f'_g': "f' w = g' w * (w - z) ^ n" if "w \<in> s'" for w
    1.64 +    unfolding f'_def g'_def using that \<open>n > 0\<close>
    1.65 +    by (auto simp: assms(6) field_simps s'_def)
    1.66 +  have "porder f z = zorder f' z"
    1.67 +    by (simp add: porder_def f'_def)
    1.68 +  also have "\<dots> = n" using assms f'_g' 
    1.69 +    by (intro zorder_eqI[OF \<open>open s'\<close> s']) (auto simp: f'_def g'_def field_simps s'_def)
    1.70 +  finally show ?thesis .
    1.71 +qed
    1.72 +
    1.73 +lemma simple_poleI':
    1.74 +  assumes "open s" "connected s" "z \<in> s"
    1.75 +  assumes "\<And>w. w \<in> s - {z} \<Longrightarrow> 
    1.76 +             ((\<lambda>w. inverse (f w)) has_field_derivative f' w) (at w)"
    1.77 +  assumes "f holomorphic_on s - {z}" "f' holomorphic_on s" "is_pole f z" "f' z \<noteq> 0"
    1.78 +  shows   "porder f z = 1"
    1.79 +proof -
    1.80 +  define g where "g = (\<lambda>w. if w = z then 0 else inverse (f w))"
    1.81 +  from \<open>is_pole f z\<close> have "eventually (\<lambda>w. f w \<noteq> 0) (at z)"
    1.82 +    unfolding is_pole_def using filterlim_at_infinity_imp_eventually_ne by blast
    1.83 +  then obtain s'' where s'': "open s''" "z \<in> s''" "\<forall>w\<in>s''-{z}. f w \<noteq> 0"
    1.84 +    by (auto simp: eventually_at_topological)
    1.85 +  from assms(1) and s''(1) have "open (s \<inter> s'')" by auto
    1.86 +  then obtain r where r: "r > 0" "ball z r \<subseteq> s \<inter> s''"
    1.87 +    using assms(3) s''(2) by (subst (asm) open_contains_ball) blast
    1.88 +  define s' where "s' = ball z r"
    1.89 +  hence s': "open s'" "connected s'" "z \<in> s'" "s' \<subseteq> s" "\<forall>w\<in>s'-{z}. f w \<noteq> 0"
    1.90 +    using r s'' by (auto simp: s'_def)
    1.91 +  have s'_ne: "s' - {z} \<noteq> {}"
    1.92 +    using r unfolding s'_def by (intro ball_minus_countable_nonempty) auto
    1.93 +
    1.94 +  have "porder f z = zorder g z"
    1.95 +    by (simp add: porder_def g_def)
    1.96 +  also have "\<dots> = 1"
    1.97 +  proof (rule simple_zeroI')
    1.98 +    fix w assume w: "w \<in> s'"
    1.99 +    have [holomorphic_intros]: "g holomorphic_on s'" unfolding g_def using assms s'
   1.100 +      by (intro is_pole_inverse_holomorphic holomorphic_on_subset[OF assms(5)]) auto
   1.101 +    hence "(g has_field_derivative deriv g w) (at w)"
   1.102 +      using w s' by (intro holomorphic_derivI)
   1.103 +    also have deriv_g: "deriv g w = f' w" if "w \<in> s' - {z}" for w
   1.104 +    proof -
   1.105 +      from that have ne: "eventually (\<lambda>w. w \<noteq> z) (nhds w)"
   1.106 +        by (intro t1_space_nhds) auto
   1.107 +      have "deriv g w = deriv (\<lambda>w. inverse (f w)) w"
   1.108 +        by (intro deriv_cong_ev refl eventually_mono [OF ne]) (auto simp: g_def)
   1.109 +      also from assms(4)[of w] that s' have "\<dots> = f' w"
   1.110 +        by (auto dest: DERIV_imp_deriv)
   1.111 +      finally show ?thesis .
   1.112 +    qed
   1.113 +    have "deriv g w = f' w"
   1.114 +      by (rule analytic_continuation_open[of "s' - {z}" s' "deriv g" f'])
   1.115 +         (insert s' assms s'_ne deriv_g w, 
   1.116 +          auto intro!: holomorphic_intros holomorphic_on_subset[OF assms(6)])
   1.117 +    finally show "(g has_field_derivative f' w) (at w)" .
   1.118 +  qed (insert assms s', auto simp: g_def)
   1.119 +  finally show ?thesis .
   1.120 +qed
   1.121 +
   1.122 +lemma residue_holomorphic_over_power:
   1.123 +  assumes "open A" "z0 \<in> A" "f holomorphic_on A"
   1.124 +  shows   "residue (\<lambda>z. f z / (z - z0) ^ Suc n) z0 = (deriv ^^ n) f z0 / fact n"
   1.125 +proof -
   1.126 +  let ?f = "\<lambda>z. f z / (z - z0) ^ Suc n"
   1.127 +  from assms(1,2) obtain r where r: "r > 0" "cball z0 r \<subseteq> A"
   1.128 +    by (auto simp: open_contains_cball)
   1.129 +  have "(?f has_contour_integral 2 * pi * \<i> * residue ?f z0) (circlepath z0 r)"
   1.130 +    using r assms by (intro base_residue[of A]) (auto intro!: holomorphic_intros)
   1.131 +  moreover have "(?f has_contour_integral 2 * pi * \<i> / fact n * (deriv ^^ n) f z0) (circlepath z0 r)"
   1.132 +    using assms r
   1.133 +    by (intro Cauchy_has_contour_integral_higher_derivative_circlepath)
   1.134 +       (auto intro!: holomorphic_on_subset[OF assms(3)] holomorphic_on_imp_continuous_on)
   1.135 +  ultimately have "2 * pi * \<i> * residue ?f z0 = 2 * pi * \<i> / fact n * (deriv ^^ n) f z0"  
   1.136 +    by (rule has_contour_integral_unique)
   1.137 +  thus ?thesis by (simp add: field_simps)
   1.138 +qed
   1.139 +
   1.140 +lemma residue_holomorphic_over_power':
   1.141 +  assumes "open A" "0 \<in> A" "f holomorphic_on A"
   1.142 +  shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
   1.143 +  using residue_holomorphic_over_power[OF assms] by simp
   1.144 +
   1.145 +lemma zer_poly_eqI:
   1.146 +  fixes f :: "complex \<Rightarrow> complex" and z0 :: complex
   1.147 +  defines "n \<equiv> zorder f z0"
   1.148 +  assumes "open A" "connected A" "z0 \<in> A" "f holomorphic_on A" "f z0 = 0" "\<exists>z\<in>A. f z \<noteq> 0"
   1.149 +  assumes lim: "((\<lambda>x. f (g x) / (g x - z0) ^ n) \<longlongrightarrow> c) F"
   1.150 +  assumes g: "filterlim g (at z0) F" and "F \<noteq> bot"
   1.151 +  shows   "zer_poly f z0 z0 = c"
   1.152 +proof -
   1.153 +  from zorder_exist[OF assms(2-7)] obtain r where
   1.154 +    r: "r > 0" "cball z0 r \<subseteq> A" "zer_poly f z0 holomorphic_on cball z0 r"
   1.155 +       "\<And>w. w \<in> cball z0 r \<Longrightarrow> f w = zer_poly f z0 w * (w - z0) ^ n"
   1.156 +    unfolding n_def by blast
   1.157 +  from r(1) have "eventually (\<lambda>w. w \<in> ball z0 r \<and> w \<noteq> z0) (at z0)"
   1.158 +    using eventually_at_ball'[of r z0 UNIV] by auto
   1.159 +  hence "eventually (\<lambda>w. zer_poly f z0 w = f w / (w - z0) ^ n) (at z0)"
   1.160 +    by eventually_elim (insert r, auto simp: field_simps)
   1.161 +  moreover have "continuous_on (ball z0 r) (zer_poly f z0)"
   1.162 +    using r by (intro holomorphic_on_imp_continuous_on) auto
   1.163 +  with r(1,2) have "isCont (zer_poly f z0) z0"
   1.164 +    by (auto simp: continuous_on_eq_continuous_at)
   1.165 +  hence "(zer_poly f z0 \<longlongrightarrow> zer_poly f z0 z0) (at z0)"
   1.166 +    unfolding isCont_def .
   1.167 +  ultimately have "((\<lambda>w. f w / (w - z0) ^ n) \<longlongrightarrow> zer_poly f z0 z0) (at z0)"
   1.168 +    by (rule Lim_transform_eventually)
   1.169 +  hence "((\<lambda>x. f (g x) / (g x - z0) ^ n) \<longlongrightarrow> zer_poly f z0 z0) F"
   1.170 +    by (rule filterlim_compose[OF _ g])
   1.171 +  from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
   1.172 +qed
   1.173 +
   1.174 +lemma pol_poly_eqI:
   1.175 +  fixes f :: "complex \<Rightarrow> complex" and z0 :: complex
   1.176 +  defines "n \<equiv> porder f z0"
   1.177 +  assumes "open A" "z0 \<in> A" "f holomorphic_on A-{z0}" "is_pole f z0"
   1.178 +  assumes lim: "((\<lambda>x. f (g x) * (g x - z0) ^ n) \<longlongrightarrow> c) F"
   1.179 +  assumes g: "filterlim g (at z0) F" and "F \<noteq> bot"
   1.180 +  shows   "pol_poly f z0 z0 = c"
   1.181 +proof -
   1.182 +  from porder_exist[OF assms(2-5)] obtain r where
   1.183 +    r: "r > 0" "cball z0 r \<subseteq> A" "pol_poly f z0 holomorphic_on cball z0 r"
   1.184 +       "\<And>w. w \<in> cball z0 r - {z0} \<Longrightarrow> f w = pol_poly f z0 w / (w - z0) ^ n"
   1.185 +    unfolding n_def by blast
   1.186 +  from r(1) have "eventually (\<lambda>w. w \<in> ball z0 r \<and> w \<noteq> z0) (at z0)"
   1.187 +    using eventually_at_ball'[of r z0 UNIV] by auto
   1.188 +  hence "eventually (\<lambda>w. pol_poly f z0 w = f w * (w - z0) ^ n) (at z0)"
   1.189 +    by eventually_elim (insert r, auto simp: field_simps)
   1.190 +  moreover have "continuous_on (ball z0 r) (pol_poly f z0)"
   1.191 +    using r by (intro holomorphic_on_imp_continuous_on) auto
   1.192 +  with r(1,2) have "isCont (pol_poly f z0) z0"
   1.193 +    by (auto simp: continuous_on_eq_continuous_at)
   1.194 +  hence "(pol_poly f z0 \<longlongrightarrow> pol_poly f z0 z0) (at z0)"
   1.195 +    unfolding isCont_def .
   1.196 +  ultimately have "((\<lambda>w. f w * (w - z0) ^ n) \<longlongrightarrow> pol_poly f z0 z0) (at z0)"
   1.197 +    by (rule Lim_transform_eventually)
   1.198 +  hence "((\<lambda>x. f (g x) * (g x - z0) ^ n) \<longlongrightarrow> pol_poly f z0 z0) F"
   1.199 +    by (rule filterlim_compose[OF _ g])
   1.200 +  from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
   1.201 +qed
   1.202 +
   1.203 +lemma residue_simple_pole:
   1.204 +  assumes "open A" "z0 \<in> A" "f holomorphic_on A - {z0}" 
   1.205 +  assumes "is_pole f z0" "porder f z0 = 1"
   1.206 +  shows   "residue f z0 = pol_poly f z0 z0"
   1.207 +  using assms by (subst residue_porder[of A]) simp_all
   1.208 +
   1.209 +lemma residue_simple_pole_limit:
   1.210 +  assumes "open A" "z0 \<in> A" "f holomorphic_on A - {z0}" 
   1.211 +  assumes "is_pole f z0" "porder f z0 = 1"
   1.212 +  assumes "((\<lambda>x. f (g x) * (g x - z0)) \<longlongrightarrow> c) F"
   1.213 +  assumes "filterlim g (at z0) F" "F \<noteq> bot"
   1.214 +  shows   "residue f z0 = c"
   1.215 +proof -
   1.216 +  have "residue f z0 = pol_poly f z0 z0"
   1.217 +    by (rule residue_simple_pole assms)+
   1.218 +  also have "\<dots> = c"
   1.219 +    using assms by (intro pol_poly_eqI[of A z0 f g c F]) auto
   1.220 +  finally show ?thesis .
   1.221 +qed
   1.222 +
   1.223 +(* TODO: This is a mess and could be done much more easily if we had
   1.224 +   a nice compositional theory of poles and zeros *)
   1.225 +lemma
   1.226 +  assumes "open s" "connected s" "z \<in> s" "f holomorphic_on s" "g holomorphic_on s"
   1.227 +  assumes "(g has_field_derivative g') (at z)"
   1.228 +  assumes "f z \<noteq> 0" "g z = 0" "g' \<noteq> 0"
   1.229 +  shows   porder_simple_pole_deriv: "porder (\<lambda>w. f w / g w) z = 1"
   1.230 +    and   residue_simple_pole_deriv: "residue (\<lambda>w. f w / g w) z = f z / g'"
   1.231 +proof -
   1.232 +  have "\<exists>w\<in>s. g w \<noteq> 0"
   1.233 +  proof (rule ccontr)
   1.234 +    assume *: "\<not>(\<exists>w\<in>s. g w \<noteq> 0)"
   1.235 +    have **: "eventually (\<lambda>w. w \<in> s) (nhds z)"
   1.236 +      by (intro eventually_nhds_in_open assms)
   1.237 +    from * have "deriv g z = deriv (\<lambda>_. 0) z"
   1.238 +      by (intro deriv_cong_ev eventually_mono [OF **]) auto
   1.239 +    also have "\<dots> = 0" by simp
   1.240 +    also from assms have "deriv g z = g'" by (auto dest: DERIV_imp_deriv)
   1.241 +    finally show False using \<open>g' \<noteq> 0\<close> by contradiction
   1.242 +  qed
   1.243 +  then obtain w where w: "w \<in> s" "g w \<noteq> 0" by blast
   1.244 +  from isolated_zeros[OF assms(5) assms(1-3,8) w]
   1.245 +  obtain r where r: "r > 0" "ball z r \<subseteq> s" "\<And>w. w \<in> ball z r - {z} \<Longrightarrow> g w \<noteq> 0"
   1.246 +    by blast
   1.247 +  from assms r have holo: "(\<lambda>w. f w / g w) holomorphic_on ball z r - {z}"
   1.248 +    by (auto intro!: holomorphic_intros)
   1.249 +
   1.250 +  have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
   1.251 +    using eventually_at_ball'[OF r(1), of z UNIV] by auto
   1.252 +  hence "eventually (\<lambda>w. g w \<noteq> 0) (at z)"
   1.253 +    by eventually_elim (use r in auto)
   1.254 +  moreover have "continuous_on s g" 
   1.255 +    by (intro holomorphic_on_imp_continuous_on) fact
   1.256 +  with assms have "isCont g z"
   1.257 +    by (auto simp: continuous_on_eq_continuous_at)
   1.258 +  ultimately have "filterlim g (at 0) (at z)"
   1.259 +    using \<open>g z = 0\<close> by (auto simp: filterlim_at isCont_def)
   1.260 +  moreover have "continuous_on s f" by (intro holomorphic_on_imp_continuous_on) fact
   1.261 +  with assms have "isCont f z"
   1.262 +    by (auto simp: continuous_on_eq_continuous_at)
   1.263 +  ultimately have pole: "is_pole (\<lambda>w. f w / g w) z" 
   1.264 +    unfolding is_pole_def using \<open>f z \<noteq> 0\<close>
   1.265 +    by (intro filterlim_divide_at_infinity[of _ "f z"]) (auto simp: isCont_def)
   1.266 +
   1.267 +  have "continuous_on s f" by (intro holomorphic_on_imp_continuous_on) fact
   1.268 +  moreover have "open (-{0::complex})" by auto
   1.269 +  ultimately have "open (f -` (-{0}) \<inter> s)" using \<open>open s\<close>
   1.270 +    by (subst (asm) continuous_on_open_vimage) blast+
   1.271 +  moreover have "z \<in> f -` (-{0}) \<inter> s" using assms by auto
   1.272 +  ultimately obtain r' where r': "r' > 0" "ball z r' \<subseteq> f -` (-{0}) \<inter> s"
   1.273 +    unfolding open_contains_ball by blast
   1.274 +
   1.275 +  let ?D = "\<lambda>w. (f w * deriv g w - g w * deriv f w) / f w ^ 2"
   1.276 +  show "porder (\<lambda>w. f w / g w) z = 1"
   1.277 +  proof (rule simple_poleI')
   1.278 +    show "open (ball z (min r r'))" "connected (ball z (min r r'))" "z \<in> ball z (min r r')"
   1.279 +      using r'(1) r(1) by auto
   1.280 +  next
   1.281 +    fix w assume "w \<in> ball z (min r r') - {z}"
   1.282 +    with r' have "w \<in> s" "f w \<noteq> 0" by auto
   1.283 +    have "((\<lambda>w. g w / f w) has_field_derivative ?D w) (at w)"
   1.284 +      by (rule derivative_eq_intros holomorphic_derivI[OF assms(4)] 
   1.285 +            holomorphic_derivI[OF assms(5)] | fact)+ 
   1.286 +         (simp_all add: algebra_simps power2_eq_square)
   1.287 +    thus "((\<lambda>w. inverse (f w / g w)) has_field_derivative ?D w) (at w)"
   1.288 +      by (simp add: divide_simps)
   1.289 +  next
   1.290 +    from r' show "?D holomorphic_on ball z (min r r')"
   1.291 +      by (intro holomorphic_intros holomorphic_on_subset[OF assms(4)]
   1.292 +                holomorphic_on_subset[OF assms(5)]) auto
   1.293 +  next
   1.294 +    from assms have "deriv g z = g'"
   1.295 +      by (auto dest: DERIV_imp_deriv)
   1.296 +    with assms r' show "(f z * deriv g z - g z * deriv f z) / (f z)\<^sup>2 \<noteq> 0"
   1.297 +      by simp
   1.298 +  qed (insert pole holo, auto)
   1.299 +
   1.300 +  show "residue (\<lambda>w. f w / g w) z = f z / g'"
   1.301 +  proof (rule residue_simple_pole_limit)
   1.302 +    show "porder (\<lambda>w. f w / g w) z = 1" by fact
   1.303 +    from r show "open (ball z r)" "z \<in> ball z r" by auto
   1.304 +    
   1.305 +    have "((\<lambda>w. (f w * (w - z)) / g w) \<longlongrightarrow> f z / g') (at z)"
   1.306 +    proof (rule lhopital_complex_simple)
   1.307 +      show "((\<lambda>w. f w * (w - z)) has_field_derivative f z) (at z)"
   1.308 +        using assms by (auto intro!: derivative_eq_intros holomorphic_derivI[OF assms(4)])
   1.309 +      show "(g has_field_derivative g') (at z)" by fact
   1.310 +    qed (insert assms, auto)
   1.311 +    thus "((\<lambda>w. (f w / g w) * (w - z)) \<longlongrightarrow> f z / g') (at z)"
   1.312 +      by (simp add: divide_simps)
   1.313 +  qed (insert holo pole, auto simp: filterlim_ident)
   1.314 +qed
   1.315 +
   1.316  end
     2.1 --- a/src/HOL/Analysis/Extended_Real_Limits.thy	Fri Aug 18 22:55:54 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Sun Aug 20 03:35:20 2017 +0200
     2.3 @@ -358,6 +358,739 @@
     2.4    apply (metis INF_absorb centre_in_ball)
     2.5    done
     2.6  
     2.7 +subsection \<open>Fun.thy\<close>
     2.8 +
     2.9 +lemma inj_fn:
    2.10 +  fixes f::"'a \<Rightarrow> 'a"
    2.11 +  assumes "inj f"
    2.12 +  shows "inj (f^^n)"
    2.13 +proof (induction n)
    2.14 +  case (Suc n)
    2.15 +  have "inj (f o (f^^n))"
    2.16 +    using inj_comp[OF assms Suc.IH] by simp
    2.17 +  then show "inj (f^^(Suc n))"
    2.18 +    by auto
    2.19 +qed (auto)
    2.20 +
    2.21 +lemma surj_fn:
    2.22 +  fixes f::"'a \<Rightarrow> 'a"
    2.23 +  assumes "surj f"
    2.24 +  shows "surj (f^^n)"
    2.25 +proof (induction n)
    2.26 +  case (Suc n)
    2.27 +  have "surj (f o (f^^n))"
    2.28 +    using assms Suc.IH by (simp add: comp_surj)
    2.29 +  then show "surj (f^^(Suc n))"
    2.30 +    by auto
    2.31 +qed (auto)
    2.32 +
    2.33 +lemma bij_fn:
    2.34 +  fixes f::"'a \<Rightarrow> 'a"
    2.35 +  assumes "bij f"
    2.36 +  shows "bij (f^^n)"
    2.37 +by (rule bijI[OF inj_fn[OF bij_is_inj[OF assms]] surj_fn[OF bij_is_surj[OF assms]]])
    2.38 +
    2.39 +lemma inv_fn_o_fn_is_id:
    2.40 +  fixes f::"'a \<Rightarrow> 'a"
    2.41 +  assumes "bij f"
    2.42 +  shows "((inv f)^^n) o (f^^n) = (\<lambda>x. x)"
    2.43 +proof -
    2.44 +  have "((inv f)^^n)((f^^n) x) = x" for x n
    2.45 +  proof (induction n)
    2.46 +    case (Suc n)
    2.47 +    have *: "(inv f) (f y) = y" for y
    2.48 +      by (simp add: assms bij_is_inj)
    2.49 +    have "(inv f ^^ Suc n) ((f ^^ Suc n) x) = (inv f^^n) (inv f (f ((f^^n) x)))"
    2.50 +      by (simp add: funpow_swap1)
    2.51 +    also have "... = (inv f^^n) ((f^^n) x)"
    2.52 +      using * by auto
    2.53 +    also have "... = x" using Suc.IH by auto
    2.54 +    finally show ?case by simp
    2.55 +  qed (auto)
    2.56 +  then show ?thesis unfolding o_def by blast
    2.57 +qed
    2.58 +
    2.59 +lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y" (* COPIED FROM Permutations *)
    2.60 +  using surj_f_inv_f[of p] by (auto simp add: bij_def)
    2.61 +
    2.62 +lemma fn_o_inv_fn_is_id:
    2.63 +  fixes f::"'a \<Rightarrow> 'a"
    2.64 +  assumes "bij f"
    2.65 +  shows "(f^^n) o ((inv f)^^n) = (\<lambda>x. x)"
    2.66 +proof -
    2.67 +  have "(f^^n) (((inv f)^^n) x) = x" for x n
    2.68 +  proof (induction n)
    2.69 +    case (Suc n)
    2.70 +    have *: "f(inv f y) = y" for y
    2.71 +      using assms by (meson bij_inv_eq_iff)
    2.72 +    have "(f ^^ Suc n) ((inv f ^^ Suc n) x) = (f^^n) (f (inv f ((inv f^^n) x)))"
    2.73 +      by (simp add: funpow_swap1)
    2.74 +    also have "... = (f^^n) ((inv f^^n) x)"
    2.75 +      using * by auto
    2.76 +    also have "... = x" using Suc.IH by auto
    2.77 +    finally show ?case by simp
    2.78 +  qed (auto)
    2.79 +  then show ?thesis unfolding o_def by blast
    2.80 +qed
    2.81 +
    2.82 +lemma inv_fn:
    2.83 +  fixes f::"'a \<Rightarrow> 'a"
    2.84 +  assumes "bij f"
    2.85 +  shows "inv (f^^n) = ((inv f)^^n)"
    2.86 +proof -
    2.87 +  have "inv (f^^n) x = ((inv f)^^n) x" for x
    2.88 +  apply (rule inv_into_f_eq, auto simp add: inj_fn[OF bij_is_inj[OF assms]])
    2.89 +  using fn_o_inv_fn_is_id[OF assms, of n] by (metis comp_apply)
    2.90 +  then show ?thesis by auto
    2.91 +qed
    2.92 +
    2.93 +lemma mono_inv:
    2.94 +  fixes f::"'a::linorder \<Rightarrow> 'b::linorder"
    2.95 +  assumes "mono f" "bij f"
    2.96 +  shows "mono (inv f)"
    2.97 +proof
    2.98 +  fix x y::'b assume "x \<le> y"
    2.99 +  then show "inv f x \<le> inv f y"
   2.100 +    by (metis (no_types, lifting) assms bij_is_surj eq_iff le_cases mono_def surj_f_inv_f)
   2.101 +qed
   2.102 +
   2.103 +lemma mono_bij_Inf:
   2.104 +  fixes f :: "'a::complete_linorder \<Rightarrow> 'b::complete_linorder"
   2.105 +  assumes "mono f" "bij f"
   2.106 +  shows "f (Inf A) = Inf (f`A)"
   2.107 +proof -
   2.108 +  have "(inv f) (Inf (f`A)) \<le> Inf ((inv f)`(f`A))"
   2.109 +    using mono_Inf[OF mono_inv[OF assms], of "f`A"] by simp
   2.110 +  then have "Inf (f`A) \<le> f (Inf ((inv f)`(f`A)))"
   2.111 +    by (metis (no_types, lifting) assms mono_def bij_inv_eq_iff)
   2.112 +  also have "... = f(Inf A)"
   2.113 +    using assms by (simp add: bij_is_inj)
   2.114 +  finally show ?thesis using mono_Inf[OF assms(1), of A] by auto
   2.115 +qed
   2.116 +
   2.117 +
   2.118 +lemma Inf_nat_def1:
   2.119 +  fixes K::"nat set"
   2.120 +  assumes "K \<noteq> {}"
   2.121 +  shows "Inf K \<in> K"
   2.122 +by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI)
   2.123 +
   2.124 +
   2.125 +subsection \<open>Extended-Real.thy\<close>
   2.126 +
   2.127 +text\<open>The proof of this one is copied from \verb+ereal_add_mono+.\<close>
   2.128 +lemma ereal_add_strict_mono2:
   2.129 +  fixes a b c d :: ereal
   2.130 +  assumes "a < b"
   2.131 +    and "c < d"
   2.132 +  shows "a + c < b + d"
   2.133 +using assms
   2.134 +apply (cases a)
   2.135 +apply (cases rule: ereal3_cases[of b c d], auto)
   2.136 +apply (cases rule: ereal3_cases[of b c d], auto)
   2.137 +done
   2.138 +
   2.139 +text \<open>The next ones are analogues of \verb+mult_mono+ and \verb+mult_mono'+ in ereal.\<close>
   2.140 +
   2.141 +lemma ereal_mult_mono:
   2.142 +  fixes a b c d::ereal
   2.143 +  assumes "b \<ge> 0" "c \<ge> 0" "a \<le> b" "c \<le> d"
   2.144 +  shows "a * c \<le> b * d"
   2.145 +by (metis ereal_mult_right_mono mult.commute order_trans assms)
   2.146 +
   2.147 +lemma ereal_mult_mono':
   2.148 +  fixes a b c d::ereal
   2.149 +  assumes "a \<ge> 0" "c \<ge> 0" "a \<le> b" "c \<le> d"
   2.150 +  shows "a * c \<le> b * d"
   2.151 +by (metis ereal_mult_right_mono mult.commute order_trans assms)
   2.152 +
   2.153 +lemma ereal_mult_mono_strict:
   2.154 +  fixes a b c d::ereal
   2.155 +  assumes "b > 0" "c > 0" "a < b" "c < d"
   2.156 +  shows "a * c < b * d"
   2.157 +proof -
   2.158 +  have "c < \<infinity>" using \<open>c < d\<close> by auto
   2.159 +  then have "a * c < b * c" by (metis ereal_mult_strict_left_mono[OF assms(3) assms(2)] mult.commute)
   2.160 +  moreover have "b * c \<le> b * d" using assms(2) assms(4) by (simp add: assms(1) ereal_mult_left_mono less_imp_le)
   2.161 +  ultimately show ?thesis by simp
   2.162 +qed
   2.163 +
   2.164 +lemma ereal_mult_mono_strict':
   2.165 +  fixes a b c d::ereal
   2.166 +  assumes "a > 0" "c > 0" "a < b" "c < d"
   2.167 +  shows "a * c < b * d"
   2.168 +apply (rule ereal_mult_mono_strict, auto simp add: assms) using assms by auto
   2.169 +
   2.170 +lemma ereal_abs_add:
   2.171 +  fixes a b::ereal
   2.172 +  shows "abs(a+b) \<le> abs a + abs b"
   2.173 +by (cases rule: ereal2_cases[of a b]) (auto)
   2.174 +
   2.175 +lemma ereal_abs_diff:
   2.176 +  fixes a b::ereal
   2.177 +  shows "abs(a-b) \<le> abs a + abs b"
   2.178 +by (cases rule: ereal2_cases[of a b]) (auto)
   2.179 +
   2.180 +lemma sum_constant_ereal:
   2.181 +  fixes a::ereal
   2.182 +  shows "(\<Sum>i\<in>I. a) = a * card I"
   2.183 +apply (cases "finite I", induct set: finite, simp_all)
   2.184 +apply (cases a, auto, metis (no_types, hide_lams) add.commute mult.commute semiring_normalization_rules(3))
   2.185 +done
   2.186 +
   2.187 +lemma real_lim_then_eventually_real:
   2.188 +  assumes "(u \<longlongrightarrow> ereal l) F"
   2.189 +  shows "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) F"
   2.190 +proof -
   2.191 +  have "ereal l \<in> {-\<infinity><..<(\<infinity>::ereal)}" by simp
   2.192 +  moreover have "open {-\<infinity><..<(\<infinity>::ereal)}" by simp
   2.193 +  ultimately have "eventually (\<lambda>n. u n \<in> {-\<infinity><..<(\<infinity>::ereal)}) F" using assms tendsto_def by blast
   2.194 +  moreover have "\<And>x. x \<in> {-\<infinity><..<(\<infinity>::ereal)} \<Longrightarrow> x = ereal(real_of_ereal x)" using ereal_real by auto
   2.195 +  ultimately show ?thesis by (metis (mono_tags, lifting) eventually_mono)
   2.196 +qed
   2.197 +
   2.198 +lemma ereal_Inf_cmult:
   2.199 +  assumes "c>(0::real)"
   2.200 +  shows "Inf {ereal c * x |x. P x} = ereal c * Inf {x. P x}"
   2.201 +proof -
   2.202 +  have "(\<lambda>x::ereal. c * x) (Inf {x::ereal. P x}) = Inf ((\<lambda>x::ereal. c * x)`{x::ereal. P x})"
   2.203 +    apply (rule mono_bij_Inf)
   2.204 +    apply (simp add: assms ereal_mult_left_mono less_imp_le mono_def)
   2.205 +    apply (rule bij_betw_byWitness[of _ "\<lambda>x. (x::ereal) / c"], auto simp add: assms ereal_mult_divide)
   2.206 +    using assms ereal_divide_eq apply auto
   2.207 +    done
   2.208 +  then show ?thesis by (simp only: setcompr_eq_image[symmetric])
   2.209 +qed
   2.210 +
   2.211 +
   2.212 +subsubsection \<open>Continuity of addition\<close>
   2.213 +
   2.214 +text \<open>The next few lemmas remove an unnecessary assumption in \verb+tendsto_add_ereal+, culminating
   2.215 +in \verb+tendsto_add_ereal_general+ which essentially says that the addition
   2.216 +is continuous on ereal times ereal, except at $(-\infty, \infty)$ and $(\infty, -\infty)$.
   2.217 +It is much more convenient in many situations, see for instance the proof of
   2.218 +\verb+tendsto_sum_ereal+ below.\<close>
   2.219 +
   2.220 +lemma tendsto_add_ereal_PInf:
   2.221 +  fixes y :: ereal
   2.222 +  assumes y: "y \<noteq> -\<infinity>"
   2.223 +  assumes f: "(f \<longlongrightarrow> \<infinity>) F" and g: "(g \<longlongrightarrow> y) F"
   2.224 +  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> \<infinity>) F"
   2.225 +proof -
   2.226 +  have "\<exists>C. eventually (\<lambda>x. g x > ereal C) F"
   2.227 +  proof (cases y)
   2.228 +    case (real r)
   2.229 +    have "y > y-1" using y real by (simp add: ereal_between(1))
   2.230 +    then have "eventually (\<lambda>x. g x > y - 1) F" using g y order_tendsto_iff by auto
   2.231 +    moreover have "y-1 = ereal(real_of_ereal(y-1))"
   2.232 +      by (metis real ereal_eq_1(1) ereal_minus(1) real_of_ereal.simps(1))
   2.233 +    ultimately have "eventually (\<lambda>x. g x > ereal(real_of_ereal(y - 1))) F" by simp
   2.234 +    then show ?thesis by auto
   2.235 +  next
   2.236 +    case (PInf)
   2.237 +    have "eventually (\<lambda>x. g x > ereal 0) F" using g PInf by (simp add: tendsto_PInfty)
   2.238 +    then show ?thesis by auto
   2.239 +  qed (simp add: y)
   2.240 +  then obtain C::real where ge: "eventually (\<lambda>x. g x > ereal C) F" by auto
   2.241 +
   2.242 +  {
   2.243 +    fix M::real
   2.244 +    have "eventually (\<lambda>x. f x > ereal(M - C)) F" using f by (simp add: tendsto_PInfty)
   2.245 +    then have "eventually (\<lambda>x. (f x > ereal (M-C)) \<and> (g x > ereal C)) F"
   2.246 +      by (auto simp add: ge eventually_conj_iff)
   2.247 +    moreover have "\<And>x. ((f x > ereal (M-C)) \<and> (g x > ereal C)) \<Longrightarrow> (f x + g x > ereal M)"
   2.248 +      using ereal_add_strict_mono2 by fastforce
   2.249 +    ultimately have "eventually (\<lambda>x. f x + g x > ereal M) F" using eventually_mono by force
   2.250 +  }
   2.251 +  then show ?thesis by (simp add: tendsto_PInfty)
   2.252 +qed
   2.253 +
   2.254 +text\<open>One would like to deduce the next lemma from the previous one, but the fact
   2.255 +that $-(x+y)$ is in general different from $(-x) + (-y)$ in ereal creates difficulties,
   2.256 +so it is more efficient to copy the previous proof.\<close>
   2.257 +
   2.258 +lemma tendsto_add_ereal_MInf:
   2.259 +  fixes y :: ereal
   2.260 +  assumes y: "y \<noteq> \<infinity>"
   2.261 +  assumes f: "(f \<longlongrightarrow> -\<infinity>) F" and g: "(g \<longlongrightarrow> y) F"
   2.262 +  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> -\<infinity>) F"
   2.263 +proof -
   2.264 +  have "\<exists>C. eventually (\<lambda>x. g x < ereal C) F"
   2.265 +  proof (cases y)
   2.266 +    case (real r)
   2.267 +    have "y < y+1" using y real by (simp add: ereal_between(1))
   2.268 +    then have "eventually (\<lambda>x. g x < y + 1) F" using g y order_tendsto_iff by force
   2.269 +    moreover have "y+1 = ereal(real_of_ereal (y+1))" by (simp add: real)
   2.270 +    ultimately have "eventually (\<lambda>x. g x < ereal(real_of_ereal(y + 1))) F" by simp
   2.271 +    then show ?thesis by auto
   2.272 +  next
   2.273 +    case (MInf)
   2.274 +    have "eventually (\<lambda>x. g x < ereal 0) F" using g MInf by (simp add: tendsto_MInfty)
   2.275 +    then show ?thesis by auto
   2.276 +  qed (simp add: y)
   2.277 +  then obtain C::real where ge: "eventually (\<lambda>x. g x < ereal C) F" by auto
   2.278 +
   2.279 +  {
   2.280 +    fix M::real
   2.281 +    have "eventually (\<lambda>x. f x < ereal(M - C)) F" using f by (simp add: tendsto_MInfty)
   2.282 +    then have "eventually (\<lambda>x. (f x < ereal (M- C)) \<and> (g x < ereal C)) F"
   2.283 +      by (auto simp add: ge eventually_conj_iff)
   2.284 +    moreover have "\<And>x. ((f x < ereal (M-C)) \<and> (g x < ereal C)) \<Longrightarrow> (f x + g x < ereal M)"
   2.285 +      using ereal_add_strict_mono2 by fastforce
   2.286 +    ultimately have "eventually (\<lambda>x. f x + g x < ereal M) F" using eventually_mono by force
   2.287 +  }
   2.288 +  then show ?thesis by (simp add: tendsto_MInfty)
   2.289 +qed
   2.290 +
   2.291 +lemma tendsto_add_ereal_general1:
   2.292 +  fixes x y :: ereal
   2.293 +  assumes y: "\<bar>y\<bar> \<noteq> \<infinity>"
   2.294 +  assumes f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   2.295 +  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   2.296 +proof (cases x)
   2.297 +  case (real r)
   2.298 +  have a: "\<bar>x\<bar> \<noteq> \<infinity>" by (simp add: real)
   2.299 +  show ?thesis by (rule tendsto_add_ereal[OF a, OF y, OF f, OF g])
   2.300 +next
   2.301 +  case PInf
   2.302 +  then show ?thesis using tendsto_add_ereal_PInf assms by force
   2.303 +next
   2.304 +  case MInf
   2.305 +  then show ?thesis using tendsto_add_ereal_MInf assms
   2.306 +    by (metis abs_ereal.simps(3) ereal_MInfty_eq_plus)
   2.307 +qed
   2.308 +
   2.309 +lemma tendsto_add_ereal_general2:
   2.310 +  fixes x y :: ereal
   2.311 +  assumes x: "\<bar>x\<bar> \<noteq> \<infinity>"
   2.312 +      and f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   2.313 +  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   2.314 +proof -
   2.315 +  have "((\<lambda>x. g x + f x) \<longlongrightarrow> x + y) F"
   2.316 +    using tendsto_add_ereal_general1[OF x, OF g, OF f] add.commute[of "y", of "x"] by simp
   2.317 +  moreover have "\<And>x. g x + f x = f x + g x" using add.commute by auto
   2.318 +  ultimately show ?thesis by simp
   2.319 +qed
   2.320 +
   2.321 +text \<open>The next lemma says that the addition is continuous on ereal, except at
   2.322 +the pairs $(-\infty, \infty)$ and $(\infty, -\infty)$.\<close>
   2.323 +
   2.324 +lemma tendsto_add_ereal_general [tendsto_intros]:
   2.325 +  fixes x y :: ereal
   2.326 +  assumes "\<not>((x=\<infinity> \<and> y=-\<infinity>) \<or> (x=-\<infinity> \<and> y=\<infinity>))"
   2.327 +      and f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   2.328 +  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   2.329 +proof (cases x)
   2.330 +  case (real r)
   2.331 +  show ?thesis
   2.332 +    apply (rule tendsto_add_ereal_general2) using real assms by auto
   2.333 +next
   2.334 +  case (PInf)
   2.335 +  then have "y \<noteq> -\<infinity>" using assms by simp
   2.336 +  then show ?thesis using tendsto_add_ereal_PInf PInf assms by auto
   2.337 +next
   2.338 +  case (MInf)
   2.339 +  then have "y \<noteq> \<infinity>" using assms by simp
   2.340 +  then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
   2.341 +qed
   2.342 +
   2.343 +subsubsection \<open>Continuity of multiplication\<close>
   2.344 +
   2.345 +text \<open>In the same way as for addition, we prove that the multiplication is continuous on
   2.346 +ereal times ereal, except at $(\infty, 0)$ and $(-\infty, 0)$ and $(0, \infty)$ and $(0, -\infty)$,
   2.347 +starting with specific situations.\<close>
   2.348 +
   2.349 +lemma tendsto_mult_real_ereal:
   2.350 +  assumes "(u \<longlongrightarrow> ereal l) F" "(v \<longlongrightarrow> ereal m) F"
   2.351 +  shows "((\<lambda>n. u n * v n) \<longlongrightarrow> ereal l * ereal m) F"
   2.352 +proof -
   2.353 +  have ureal: "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) F" by (rule real_lim_then_eventually_real[OF assms(1)])
   2.354 +  then have "((\<lambda>n. ereal(real_of_ereal(u n))) \<longlongrightarrow> ereal l) F" using assms by auto
   2.355 +  then have limu: "((\<lambda>n. real_of_ereal(u n)) \<longlongrightarrow> l) F" by auto
   2.356 +  have vreal: "eventually (\<lambda>n. v n = ereal(real_of_ereal(v n))) F" by (rule real_lim_then_eventually_real[OF assms(2)])
   2.357 +  then have "((\<lambda>n. ereal(real_of_ereal(v n))) \<longlongrightarrow> ereal m) F" using assms by auto
   2.358 +  then have limv: "((\<lambda>n. real_of_ereal(v n)) \<longlongrightarrow> m) F" by auto
   2.359 +
   2.360 +  {
   2.361 +    fix n assume "u n = ereal(real_of_ereal(u n))" "v n = ereal(real_of_ereal(v n))"
   2.362 +    then have "ereal(real_of_ereal(u n) * real_of_ereal(v n)) = u n * v n" by (metis times_ereal.simps(1))
   2.363 +  }
   2.364 +  then have *: "eventually (\<lambda>n. ereal(real_of_ereal(u n) * real_of_ereal(v n)) = u n * v n) F"
   2.365 +    using eventually_elim2[OF ureal vreal] by auto
   2.366 +
   2.367 +  have "((\<lambda>n. real_of_ereal(u n) * real_of_ereal(v n)) \<longlongrightarrow> l * m) F" using tendsto_mult[OF limu limv] by auto
   2.368 +  then have "((\<lambda>n. ereal(real_of_ereal(u n)) * real_of_ereal(v n)) \<longlongrightarrow> ereal(l * m)) F" by auto
   2.369 +  then show ?thesis using * filterlim_cong by fastforce
   2.370 +qed
   2.371 +
   2.372 +lemma tendsto_mult_ereal_PInf:
   2.373 +  fixes f g::"_ \<Rightarrow> ereal"
   2.374 +  assumes "(f \<longlongrightarrow> l) F" "l>0" "(g \<longlongrightarrow> \<infinity>) F"
   2.375 +  shows "((\<lambda>x. f x * g x) \<longlongrightarrow> \<infinity>) F"
   2.376 +proof -
   2.377 +  obtain a::real where "0 < ereal a" "a < l" using assms(2) using ereal_dense2 by blast
   2.378 +  have *: "eventually (\<lambda>x. f x > a) F" using \<open>a < l\<close> assms(1) by (simp add: order_tendsto_iff)
   2.379 +  {
   2.380 +    fix K::real
   2.381 +    define M where "M = max K 1"
   2.382 +    then have "M > 0" by simp
   2.383 +    then have "ereal(M/a) > 0" using \<open>ereal a > 0\<close> by simp
   2.384 +    then have "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > ereal a * ereal(M/a))"
   2.385 +      using ereal_mult_mono_strict'[where ?c = "M/a", OF \<open>0 < ereal a\<close>] by auto
   2.386 +    moreover have "ereal a * ereal(M/a) = M" using \<open>ereal a > 0\<close> by simp
   2.387 +    ultimately have "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > M)" by simp
   2.388 +    moreover have "M \<ge> K" unfolding M_def by simp
   2.389 +    ultimately have Imp: "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > K)"
   2.390 +      using ereal_less_eq(3) le_less_trans by blast
   2.391 +
   2.392 +    have "eventually (\<lambda>x. g x > M/a) F" using assms(3) by (simp add: tendsto_PInfty)
   2.393 +    then have "eventually (\<lambda>x. (f x > a) \<and> (g x > M/a)) F"
   2.394 +      using * by (auto simp add: eventually_conj_iff)
   2.395 +    then have "eventually (\<lambda>x. f x * g x > K) F" using eventually_mono Imp by force
   2.396 +  }
   2.397 +  then show ?thesis by (auto simp add: tendsto_PInfty)
   2.398 +qed
   2.399 +
   2.400 +lemma tendsto_mult_ereal_pos:
   2.401 +  fixes f g::"_ \<Rightarrow> ereal"
   2.402 +  assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "l>0" "m>0"
   2.403 +  shows "((\<lambda>x. f x * g x) \<longlongrightarrow> l * m) F"
   2.404 +proof (cases)
   2.405 +  assume *: "l = \<infinity> \<or> m = \<infinity>"
   2.406 +  then show ?thesis
   2.407 +  proof (cases)
   2.408 +    assume "m = \<infinity>"
   2.409 +    then show ?thesis using tendsto_mult_ereal_PInf assms by auto
   2.410 +  next
   2.411 +    assume "\<not>(m = \<infinity>)"
   2.412 +    then have "l = \<infinity>" using * by simp
   2.413 +    then have "((\<lambda>x. g x * f x) \<longlongrightarrow> l * m) F" using tendsto_mult_ereal_PInf assms by auto
   2.414 +    moreover have "\<And>x. g x * f x = f x * g x" using mult.commute by auto
   2.415 +    ultimately show ?thesis by simp
   2.416 +  qed
   2.417 +next
   2.418 +  assume "\<not>(l = \<infinity> \<or> m = \<infinity>)"
   2.419 +  then have "l < \<infinity>" "m < \<infinity>" by auto
   2.420 +  then obtain lr mr where "l = ereal lr" "m = ereal mr"
   2.421 +    using \<open>l>0\<close> \<open>m>0\<close> by (metis ereal_cases ereal_less(6) not_less_iff_gr_or_eq)
   2.422 +  then show ?thesis using tendsto_mult_real_ereal assms by auto
   2.423 +qed
   2.424 +
   2.425 +text \<open>We reduce the general situation to the positive case by multiplying by suitable signs.
   2.426 +Unfortunately, as ereal is not a ring, all the neat sign lemmas are not available there. We
   2.427 +give the bare minimum we need.\<close>
   2.428 +
   2.429 +lemma ereal_sgn_abs:
   2.430 +  fixes l::ereal
   2.431 +  shows "sgn(l) * l = abs(l)"
   2.432 +apply (cases l) by (auto simp add: sgn_if ereal_less_uminus_reorder)
   2.433 +
   2.434 +lemma sgn_squared_ereal:
   2.435 +  assumes "l \<noteq> (0::ereal)"
   2.436 +  shows "sgn(l) * sgn(l) = 1"
   2.437 +apply (cases l) using assms by (auto simp add: one_ereal_def sgn_if)
   2.438 +
   2.439 +lemma tendsto_mult_ereal [tendsto_intros]:
   2.440 +  fixes f g::"_ \<Rightarrow> ereal"
   2.441 +  assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "\<not>((l=0 \<and> abs(m) = \<infinity>) \<or> (m=0 \<and> abs(l) = \<infinity>))"
   2.442 +  shows "((\<lambda>x. f x * g x) \<longlongrightarrow> l * m) F"
   2.443 +proof (cases)
   2.444 +  assume "l=0 \<or> m=0"
   2.445 +  then have "abs(l) \<noteq> \<infinity>" "abs(m) \<noteq> \<infinity>" using assms(3) by auto
   2.446 +  then obtain lr mr where "l = ereal lr" "m = ereal mr" by auto
   2.447 +  then show ?thesis using tendsto_mult_real_ereal assms by auto
   2.448 +next
   2.449 +  have sgn_finite: "\<And>a::ereal. abs(sgn a) \<noteq> \<infinity>"
   2.450 +    by (metis MInfty_neq_ereal(2) PInfty_neq_ereal(2) abs_eq_infinity_cases ereal_times(1) ereal_times(3) ereal_uminus_eq_reorder sgn_ereal.elims)
   2.451 +  then have sgn_finite2: "\<And>a b::ereal. abs(sgn a * sgn b) \<noteq> \<infinity>"
   2.452 +    by (metis abs_eq_infinity_cases abs_ereal.simps(2) abs_ereal.simps(3) ereal_mult_eq_MInfty ereal_mult_eq_PInfty)
   2.453 +  assume "\<not>(l=0 \<or> m=0)"
   2.454 +  then have "l \<noteq> 0" "m \<noteq> 0" by auto
   2.455 +  then have "abs(l) > 0" "abs(m) > 0"
   2.456 +    by (metis abs_ereal_ge0 abs_ereal_less0 abs_ereal_pos ereal_uminus_uminus ereal_uminus_zero less_le not_less)+
   2.457 +  then have "sgn(l) * l > 0" "sgn(m) * m > 0" using ereal_sgn_abs by auto
   2.458 +  moreover have "((\<lambda>x. sgn(l) * f x) \<longlongrightarrow> (sgn(l) * l)) F"
   2.459 +    by (rule tendsto_cmult_ereal, auto simp add: sgn_finite assms(1))
   2.460 +  moreover have "((\<lambda>x. sgn(m) * g x) \<longlongrightarrow> (sgn(m) * m)) F"
   2.461 +    by (rule tendsto_cmult_ereal, auto simp add: sgn_finite assms(2))
   2.462 +  ultimately have *: "((\<lambda>x. (sgn(l) * f x) * (sgn(m) * g x)) \<longlongrightarrow> (sgn(l) * l) * (sgn(m) * m)) F"
   2.463 +    using tendsto_mult_ereal_pos by force
   2.464 +  have "((\<lambda>x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x))) \<longlongrightarrow> (sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m))) F"
   2.465 +    by (rule tendsto_cmult_ereal, auto simp add: sgn_finite2 *)
   2.466 +  moreover have "\<And>x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x)) = f x * g x"
   2.467 +    by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
   2.468 +  moreover have "(sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m)) = l * m"
   2.469 +    by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
   2.470 +  ultimately show ?thesis by auto
   2.471 +qed
   2.472 +
   2.473 +lemma tendsto_cmult_ereal_general [tendsto_intros]:
   2.474 +  fixes f::"_ \<Rightarrow> ereal" and c::ereal
   2.475 +  assumes "(f \<longlongrightarrow> l) F" "\<not> (l=0 \<and> abs(c) = \<infinity>)"
   2.476 +  shows "((\<lambda>x. c * f x) \<longlongrightarrow> c * l) F"
   2.477 +by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
   2.478 +
   2.479 +
   2.480 +subsubsection \<open>Continuity of division\<close>
   2.481 +
   2.482 +lemma tendsto_inverse_ereal_PInf:
   2.483 +  fixes u::"_ \<Rightarrow> ereal"
   2.484 +  assumes "(u \<longlongrightarrow> \<infinity>) F"
   2.485 +  shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 0) F"
   2.486 +proof -
   2.487 +  {
   2.488 +    fix e::real assume "e>0"
   2.489 +    have "1/e < \<infinity>" by auto
   2.490 +    then have "eventually (\<lambda>n. u n > 1/e) F" using assms(1) by (simp add: tendsto_PInfty)
   2.491 +    moreover
   2.492 +    {
   2.493 +      fix z::ereal assume "z>1/e"
   2.494 +      then have "z>0" using \<open>e>0\<close> using less_le_trans not_le by fastforce
   2.495 +      then have "1/z \<ge> 0" by auto
   2.496 +      moreover have "1/z < e" using \<open>e>0\<close> \<open>z>1/e\<close>
   2.497 +        apply (cases z) apply auto
   2.498 +        by (metis (mono_tags, hide_lams) less_ereal.simps(2) less_ereal.simps(4) divide_less_eq ereal_divide_less_pos ereal_less(4)
   2.499 +            ereal_less_eq(4) less_le_trans mult_eq_0_iff not_le not_one_less_zero times_ereal.simps(1))
   2.500 +      ultimately have "1/z \<ge> 0" "1/z < e" by auto
   2.501 +    }
   2.502 +    ultimately have "eventually (\<lambda>n. 1/u n<e) F" "eventually (\<lambda>n. 1/u n\<ge>0) F" by (auto simp add: eventually_mono)
   2.503 +  } note * = this
   2.504 +  show ?thesis
   2.505 +  proof (subst order_tendsto_iff, auto)
   2.506 +    fix a::ereal assume "a<0"
   2.507 +    then show "eventually (\<lambda>n. 1/u n > a) F" using *(2) eventually_mono less_le_trans linordered_field_no_ub by fastforce
   2.508 +  next
   2.509 +    fix a::ereal assume "a>0"
   2.510 +    then obtain e::real where "e>0" "a>e" using ereal_dense2 ereal_less(2) by blast
   2.511 +    then have "eventually (\<lambda>n. 1/u n < e) F" using *(1) by auto
   2.512 +    then show "eventually (\<lambda>n. 1/u n < a) F" using \<open>a>e\<close> by (metis (mono_tags, lifting) eventually_mono less_trans)
   2.513 +  qed
   2.514 +qed
   2.515 +
   2.516 +text \<open>The next lemma deserves to exist by itself, as it is so common and useful.\<close>
   2.517 +
   2.518 +lemma tendsto_inverse_real [tendsto_intros]:
   2.519 +  fixes u::"_ \<Rightarrow> real"
   2.520 +  shows "(u \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. 1/ u x) \<longlongrightarrow> 1/l) F"
   2.521 +  using tendsto_inverse unfolding inverse_eq_divide .
   2.522 +
   2.523 +lemma tendsto_inverse_ereal [tendsto_intros]:
   2.524 +  fixes u::"_ \<Rightarrow> ereal"
   2.525 +  assumes "(u \<longlongrightarrow> l) F" "l \<noteq> 0"
   2.526 +  shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 1/l) F"
   2.527 +proof (cases l)
   2.528 +  case (real r)
   2.529 +  then have "r \<noteq> 0" using assms(2) by auto
   2.530 +  then have "1/l = ereal(1/r)" using real by (simp add: one_ereal_def)
   2.531 +  define v where "v = (\<lambda>n. real_of_ereal(u n))"
   2.532 +  have ureal: "eventually (\<lambda>n. u n = ereal(v n)) F" unfolding v_def using real_lim_then_eventually_real assms(1) real by auto
   2.533 +  then have "((\<lambda>n. ereal(v n)) \<longlongrightarrow> ereal r) F" using assms real v_def by auto
   2.534 +  then have *: "((\<lambda>n. v n) \<longlongrightarrow> r) F" by auto
   2.535 +  then have "((\<lambda>n. 1/v n) \<longlongrightarrow> 1/r) F" using \<open>r \<noteq> 0\<close> tendsto_inverse_real by auto
   2.536 +  then have lim: "((\<lambda>n. ereal(1/v n)) \<longlongrightarrow> 1/l) F" using \<open>1/l = ereal(1/r)\<close> by auto
   2.537 +
   2.538 +  have "r \<in> -{0}" "open (-{(0::real)})" using \<open>r \<noteq> 0\<close> by auto
   2.539 +  then have "eventually (\<lambda>n. v n \<in> -{0}) F" using * using topological_tendstoD by blast
   2.540 +  then have "eventually (\<lambda>n. v n \<noteq> 0) F" by auto
   2.541 +  moreover
   2.542 +  {
   2.543 +    fix n assume H: "v n \<noteq> 0" "u n = ereal(v n)"
   2.544 +    then have "ereal(1/v n) = 1/ereal(v n)" by (simp add: one_ereal_def)
   2.545 +    then have "ereal(1/v n) = 1/u n" using H(2) by simp
   2.546 +  }
   2.547 +  ultimately have "eventually (\<lambda>n. ereal(1/v n) = 1/u n) F" using ureal eventually_elim2 by force
   2.548 +  with Lim_transform_eventually[OF this lim] show ?thesis by simp
   2.549 +next
   2.550 +  case (PInf)
   2.551 +  then have "1/l = 0" by auto
   2.552 +  then show ?thesis using tendsto_inverse_ereal_PInf assms PInf by auto
   2.553 +next
   2.554 +  case (MInf)
   2.555 +  then have "1/l = 0" by auto
   2.556 +  have "1/z = -1/ -z" if "z < 0" for z::ereal
   2.557 +    apply (cases z) using divide_ereal_def \<open> z < 0 \<close> by auto
   2.558 +  moreover have "eventually (\<lambda>n. u n < 0) F" by (metis (no_types) MInf assms(1) tendsto_MInfty zero_ereal_def)
   2.559 +  ultimately have *: "eventually (\<lambda>n. -1/-u n = 1/u n) F" by (simp add: eventually_mono)
   2.560 +
   2.561 +  define v where "v = (\<lambda>n. - u n)"
   2.562 +  have "(v \<longlongrightarrow> \<infinity>) F" unfolding v_def using MInf assms(1) tendsto_uminus_ereal by fastforce
   2.563 +  then have "((\<lambda>n. 1/v n) \<longlongrightarrow> 0) F" using tendsto_inverse_ereal_PInf by auto
   2.564 +  then have "((\<lambda>n. -1/v n) \<longlongrightarrow> 0) F" using tendsto_uminus_ereal by fastforce
   2.565 +  then show ?thesis unfolding v_def using Lim_transform_eventually[OF *] \<open> 1/l = 0 \<close> by auto
   2.566 +qed
   2.567 +
   2.568 +lemma tendsto_divide_ereal [tendsto_intros]:
   2.569 +  fixes f g::"_ \<Rightarrow> ereal"
   2.570 +  assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "m \<noteq> 0" "\<not>(abs(l) = \<infinity> \<and> abs(m) = \<infinity>)"
   2.571 +  shows "((\<lambda>x. f x / g x) \<longlongrightarrow> l / m) F"
   2.572 +proof -
   2.573 +  define h where "h = (\<lambda>x. 1/ g x)"
   2.574 +  have *: "(h \<longlongrightarrow> 1/m) F" unfolding h_def using assms(2) assms(3) tendsto_inverse_ereal by auto
   2.575 +  have "((\<lambda>x. f x * h x) \<longlongrightarrow> l * (1/m)) F"
   2.576 +    apply (rule tendsto_mult_ereal[OF assms(1) *]) using assms(3) assms(4) by (auto simp add: divide_ereal_def)
   2.577 +  moreover have "f x * h x = f x / g x" for x unfolding h_def by (simp add: divide_ereal_def)
   2.578 +  moreover have "l * (1/m) = l/m" by (simp add: divide_ereal_def)
   2.579 +  ultimately show ?thesis unfolding h_def using Lim_transform_eventually by auto
   2.580 +qed
   2.581 +
   2.582 +
   2.583 +subsubsection \<open>Further limits\<close>
   2.584 +
   2.585 +lemma id_nat_ereal_tendsto_PInf [tendsto_intros]:
   2.586 +  "(\<lambda> n::nat. real n) \<longlonglongrightarrow> \<infinity>"
   2.587 +by (simp add: filterlim_real_sequentially tendsto_PInfty_eq_at_top)
   2.588 +
   2.589 +lemma tendsto_at_top_pseudo_inverse [tendsto_intros]:
   2.590 +  fixes u::"nat \<Rightarrow> nat"
   2.591 +  assumes "LIM n sequentially. u n :> at_top"
   2.592 +  shows "LIM n sequentially. Inf {N. u N \<ge> n} :> at_top"
   2.593 +proof -
   2.594 +  {
   2.595 +    fix C::nat
   2.596 +    define M where "M = Max {u n| n. n \<le> C}+1"
   2.597 +    {
   2.598 +      fix n assume "n \<ge> M"
   2.599 +      have "eventually (\<lambda>N. u N \<ge> n) sequentially" using assms
   2.600 +        by (simp add: filterlim_at_top)
   2.601 +      then have *: "{N. u N \<ge> n} \<noteq> {}" by force
   2.602 +
   2.603 +      have "N > C" if "u N \<ge> n" for N
   2.604 +      proof (rule ccontr)
   2.605 +        assume "\<not>(N > C)"
   2.606 +        have "u N \<le> Max {u n| n. n \<le> C}"
   2.607 +          apply (rule Max_ge) using \<open>\<not>(N > C)\<close> by auto
   2.608 +        then show False using \<open>u N \<ge> n\<close> \<open>n \<ge> M\<close> unfolding M_def by auto
   2.609 +      qed
   2.610 +      then have **: "{N. u N \<ge> n} \<subseteq> {C..}" by fastforce
   2.611 +      have "Inf {N. u N \<ge> n} \<ge> C"
   2.612 +        by (metis "*" "**" Inf_nat_def1 atLeast_iff subset_eq)
   2.613 +    }
   2.614 +    then have "eventually (\<lambda>n. Inf {N. u N \<ge> n} \<ge> C) sequentially"
   2.615 +      using eventually_sequentially by auto
   2.616 +  }
   2.617 +  then show ?thesis using filterlim_at_top by auto
   2.618 +qed
   2.619 +
   2.620 +lemma pseudo_inverse_finite_set:
   2.621 +  fixes u::"nat \<Rightarrow> nat"
   2.622 +  assumes "LIM n sequentially. u n :> at_top"
   2.623 +  shows "finite {N. u N \<le> n}"
   2.624 +proof -
   2.625 +  fix n
   2.626 +  have "eventually (\<lambda>N. u N \<ge> n+1) sequentially" using assms
   2.627 +    by (simp add: filterlim_at_top)
   2.628 +  then obtain N1 where N1: "\<And>N. N \<ge> N1 \<Longrightarrow> u N \<ge> n + 1"
   2.629 +    using eventually_sequentially by auto
   2.630 +  have "{N. u N \<le> n} \<subseteq> {..<N1}"
   2.631 +    apply auto using N1 by (metis Suc_eq_plus1 not_less not_less_eq_eq)
   2.632 +  then show "finite {N. u N \<le> n}" by (simp add: finite_subset)
   2.633 +qed
   2.634 +
   2.635 +lemma tendsto_at_top_pseudo_inverse2 [tendsto_intros]:
   2.636 +  fixes u::"nat \<Rightarrow> nat"
   2.637 +  assumes "LIM n sequentially. u n :> at_top"
   2.638 +  shows "LIM n sequentially. Max {N. u N \<le> n} :> at_top"
   2.639 +proof -
   2.640 +  {
   2.641 +    fix N0::nat
   2.642 +    have "N0 \<le> Max {N. u N \<le> n}" if "n \<ge> u N0" for n
   2.643 +      apply (rule Max.coboundedI) using pseudo_inverse_finite_set[OF assms] that by auto
   2.644 +    then have "eventually (\<lambda>n. N0 \<le> Max {N. u N \<le> n}) sequentially"
   2.645 +      using eventually_sequentially by blast
   2.646 +  }
   2.647 +  then show ?thesis using filterlim_at_top by auto
   2.648 +qed
   2.649 +
   2.650 +lemma ereal_truncation_top [tendsto_intros]:
   2.651 +  fixes x::ereal
   2.652 +  shows "(\<lambda>n::nat. min x n) \<longlonglongrightarrow> x"
   2.653 +proof (cases x)
   2.654 +  case (real r)
   2.655 +  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   2.656 +  then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   2.657 +  then have "eventually (\<lambda>n. min x n = x) sequentially" using eventually_at_top_linorder by blast
   2.658 +  then show ?thesis by (simp add: Lim_eventually)
   2.659 +next
   2.660 +  case (PInf)
   2.661 +  then have "min x n = n" for n::nat by (auto simp add: min_def)
   2.662 +  then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto
   2.663 +next
   2.664 +  case (MInf)
   2.665 +  then have "min x n = x" for n::nat by (auto simp add: min_def)
   2.666 +  then show ?thesis by auto
   2.667 +qed
   2.668 +
   2.669 +lemma ereal_truncation_real_top [tendsto_intros]:
   2.670 +  fixes x::ereal
   2.671 +  assumes "x \<noteq> - \<infinity>"
   2.672 +  shows "(\<lambda>n::nat. real_of_ereal(min x n)) \<longlonglongrightarrow> x"
   2.673 +proof (cases x)
   2.674 +  case (real r)
   2.675 +  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   2.676 +  then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   2.677 +  then have "real_of_ereal(min x n) = r" if "n \<ge> K" for n using real that by auto
   2.678 +  then have "eventually (\<lambda>n. real_of_ereal(min x n) = r) sequentially" using eventually_at_top_linorder by blast
   2.679 +  then have "(\<lambda>n. real_of_ereal(min x n)) \<longlonglongrightarrow> r" by (simp add: Lim_eventually)
   2.680 +  then show ?thesis using real by auto
   2.681 +next
   2.682 +  case (PInf)
   2.683 +  then have "real_of_ereal(min x n) = n" for n::nat by (auto simp add: min_def)
   2.684 +  then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto
   2.685 +qed (simp add: assms)
   2.686 +
   2.687 +lemma ereal_truncation_bottom [tendsto_intros]:
   2.688 +  fixes x::ereal
   2.689 +  shows "(\<lambda>n::nat. max x (- real n)) \<longlonglongrightarrow> x"
   2.690 +proof (cases x)
   2.691 +  case (real r)
   2.692 +  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   2.693 +  then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   2.694 +  then have "eventually (\<lambda>n. max x (-real n) = x) sequentially" using eventually_at_top_linorder by blast
   2.695 +  then show ?thesis by (simp add: Lim_eventually)
   2.696 +next
   2.697 +  case (MInf)
   2.698 +  then have "max x (-real n) = (-1)* ereal(real n)" for n::nat by (auto simp add: max_def)
   2.699 +  moreover have "(\<lambda>n. (-1)* ereal(real n)) \<longlonglongrightarrow> -\<infinity>"
   2.700 +    using tendsto_cmult_ereal[of "-1", OF _ id_nat_ereal_tendsto_PInf] by (simp add: one_ereal_def)
   2.701 +  ultimately show ?thesis using MInf by auto
   2.702 +next
   2.703 +  case (PInf)
   2.704 +  then have "max x (-real n) = x" for n::nat by (auto simp add: max_def)
   2.705 +  then show ?thesis by auto
   2.706 +qed
   2.707 +
   2.708 +lemma ereal_truncation_real_bottom [tendsto_intros]:
   2.709 +  fixes x::ereal
   2.710 +  assumes "x \<noteq> \<infinity>"
   2.711 +  shows "(\<lambda>n::nat. real_of_ereal(max x (- real n))) \<longlonglongrightarrow> x"
   2.712 +proof (cases x)
   2.713 +  case (real r)
   2.714 +  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   2.715 +  then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   2.716 +  then have "real_of_ereal(max x (-real n)) = r" if "n \<ge> K" for n using real that by auto
   2.717 +  then have "eventually (\<lambda>n. real_of_ereal(max x (-real n)) = r) sequentially" using eventually_at_top_linorder by blast
   2.718 +  then have "(\<lambda>n. real_of_ereal(max x (-real n))) \<longlonglongrightarrow> r" by (simp add: Lim_eventually)
   2.719 +  then show ?thesis using real by auto
   2.720 +next
   2.721 +  case (MInf)
   2.722 +  then have "real_of_ereal(max x (-real n)) = (-1)* ereal(real n)" for n::nat by (auto simp add: max_def)
   2.723 +  moreover have "(\<lambda>n. (-1)* ereal(real n)) \<longlonglongrightarrow> -\<infinity>"
   2.724 +    using tendsto_cmult_ereal[of "-1", OF _ id_nat_ereal_tendsto_PInf] by (simp add: one_ereal_def)
   2.725 +  ultimately show ?thesis using MInf by auto
   2.726 +qed (simp add: assms)
   2.727 +
   2.728 +text \<open>the next one is copied from \verb+tendsto_sum+.\<close>
   2.729 +lemma tendsto_sum_ereal [tendsto_intros]:
   2.730 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
   2.731 +  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
   2.732 +          "\<And>i. abs(a i) \<noteq> \<infinity>"
   2.733 +  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
   2.734 +proof (cases "finite S")
   2.735 +  assume "finite S" then show ?thesis using assms
   2.736 +    by (induct, simp, simp add: tendsto_add_ereal_general2 assms)
   2.737 +qed(simp)
   2.738 +
   2.739 +
   2.740  subsection \<open>monoset\<close>
   2.741  
   2.742  definition (in order) mono_set:
   2.743 @@ -530,6 +1263,606 @@
   2.744      by auto
   2.745  qed
   2.746  
   2.747 +lemma limsup_finite_then_bounded:
   2.748 +  fixes u::"nat \<Rightarrow> real"
   2.749 +  assumes "limsup u < \<infinity>"
   2.750 +  shows "\<exists>C. \<forall>n. u n \<le> C"
   2.751 +proof -
   2.752 +  obtain C where C: "limsup u < C" "C < \<infinity>" using assms ereal_dense2 by blast
   2.753 +  then have "C = ereal(real_of_ereal C)" using ereal_real by force
   2.754 +  have "eventually (\<lambda>n. u n < C) sequentially" using C(1) unfolding Limsup_def
   2.755 +    apply (auto simp add: INF_less_iff)
   2.756 +    using SUP_lessD eventually_mono by fastforce
   2.757 +  then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> u n < C" using eventually_sequentially by auto
   2.758 +  define D where "D = max (real_of_ereal C) (Max {u n |n. n \<le> N})"
   2.759 +  have "\<And>n. u n \<le> D"
   2.760 +  proof -
   2.761 +    fix n show "u n \<le> D"
   2.762 +    proof (cases)
   2.763 +      assume *: "n \<le> N"
   2.764 +      have "u n \<le> Max {u n |n. n \<le> N}" by (rule Max_ge, auto simp add: *)
   2.765 +      then show "u n \<le> D" unfolding D_def by linarith
   2.766 +    next
   2.767 +      assume "\<not>(n \<le> N)"
   2.768 +      then have "n \<ge> N" by simp
   2.769 +      then have "u n < C" using N by auto
   2.770 +      then have "u n < real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
   2.771 +      then show "u n \<le> D" unfolding D_def by linarith
   2.772 +    qed
   2.773 +  qed
   2.774 +  then show ?thesis by blast
   2.775 +qed
   2.776 +
   2.777 +lemma liminf_finite_then_bounded_below:
   2.778 +  fixes u::"nat \<Rightarrow> real"
   2.779 +  assumes "liminf u > -\<infinity>"
   2.780 +  shows "\<exists>C. \<forall>n. u n \<ge> C"
   2.781 +proof -
   2.782 +  obtain C where C: "liminf u > C" "C > -\<infinity>" using assms using ereal_dense2 by blast
   2.783 +  then have "C = ereal(real_of_ereal C)" using ereal_real by force
   2.784 +  have "eventually (\<lambda>n. u n > C) sequentially" using C(1) unfolding Liminf_def
   2.785 +    apply (auto simp add: less_SUP_iff)
   2.786 +    using eventually_elim2 less_INF_D by fastforce
   2.787 +  then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> u n > C" using eventually_sequentially by auto
   2.788 +  define D where "D = min (real_of_ereal C) (Min {u n |n. n \<le> N})"
   2.789 +  have "\<And>n. u n \<ge> D"
   2.790 +  proof -
   2.791 +    fix n show "u n \<ge> D"
   2.792 +    proof (cases)
   2.793 +      assume *: "n \<le> N"
   2.794 +      have "u n \<ge> Min {u n |n. n \<le> N}" by (rule Min_le, auto simp add: *)
   2.795 +      then show "u n \<ge> D" unfolding D_def by linarith
   2.796 +    next
   2.797 +      assume "\<not>(n \<le> N)"
   2.798 +      then have "n \<ge> N" by simp
   2.799 +      then have "u n > C" using N by auto
   2.800 +      then have "u n > real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
   2.801 +      then show "u n \<ge> D" unfolding D_def by linarith
   2.802 +    qed
   2.803 +  qed
   2.804 +  then show ?thesis by blast
   2.805 +qed
   2.806 +
   2.807 +lemma liminf_upper_bound:
   2.808 +  fixes u:: "nat \<Rightarrow> ereal"
   2.809 +  assumes "liminf u < l"
   2.810 +  shows "\<exists>N>k. u N < l"
   2.811 +by (metis assms gt_ex less_le_trans liminf_bounded_iff not_less)
   2.812 +
   2.813 +lemma limsup_shift:
   2.814 +  "limsup (\<lambda>n. u (n+1)) = limsup u"
   2.815 +proof -
   2.816 +  have "(SUP m:{n+1..}. u m) = (SUP m:{n..}. u (m + 1))" for n
   2.817 +    apply (rule SUP_eq) using Suc_le_D by auto
   2.818 +  then have a: "(INF n. SUP m:{n..}. u (m + 1)) = (INF n. (SUP m:{n+1..}. u m))" by auto
   2.819 +  have b: "(INF n. (SUP m:{n+1..}. u m)) = (INF n:{1..}. (SUP m:{n..}. u m))"
   2.820 +    apply (rule INF_eq) using Suc_le_D by auto
   2.821 +  have "(INF n:{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
   2.822 +    apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
   2.823 +  moreover have "decseq (\<lambda>n. (SUP m:{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
   2.824 +  ultimately have c: "(INF n:{1..}. (SUP m:{n..}. u m)) = (INF n. (SUP m:{n..}. u m))" by simp
   2.825 +  have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m:{n..}. u (m + 1))" using a b c by simp
   2.826 +  then show ?thesis by (auto cong: limsup_INF_SUP)
   2.827 +qed
   2.828 +
   2.829 +lemma limsup_shift_k:
   2.830 +  "limsup (\<lambda>n. u (n+k)) = limsup u"
   2.831 +proof (induction k)
   2.832 +  case (Suc k)
   2.833 +  have "limsup (\<lambda>n. u (n+k+1)) = limsup (\<lambda>n. u (n+k))" using limsup_shift[where ?u="\<lambda>n. u(n+k)"] by simp
   2.834 +  then show ?case using Suc.IH by simp
   2.835 +qed (auto)
   2.836 +
   2.837 +lemma liminf_shift:
   2.838 +  "liminf (\<lambda>n. u (n+1)) = liminf u"
   2.839 +proof -
   2.840 +  have "(INF m:{n+1..}. u m) = (INF m:{n..}. u (m + 1))" for n
   2.841 +    apply (rule INF_eq) using Suc_le_D by (auto)
   2.842 +  then have a: "(SUP n. INF m:{n..}. u (m + 1)) = (SUP n. (INF m:{n+1..}. u m))" by auto
   2.843 +  have b: "(SUP n. (INF m:{n+1..}. u m)) = (SUP n:{1..}. (INF m:{n..}. u m))"
   2.844 +    apply (rule SUP_eq) using Suc_le_D by (auto)
   2.845 +  have "(SUP n:{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
   2.846 +    apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
   2.847 +  moreover have "incseq (\<lambda>n. (INF m:{n..}. u m))" by (simp add: INF_superset_mono mono_def)
   2.848 +  ultimately have c: "(SUP n:{1..}. (INF m:{n..}. u m)) = (SUP n. (INF m:{n..}. u m))" by simp
   2.849 +  have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m:{n..}. u (m + 1))" using a b c by simp
   2.850 +  then show ?thesis by (auto cong: liminf_SUP_INF)
   2.851 +qed
   2.852 +
   2.853 +lemma liminf_shift_k:
   2.854 +  "liminf (\<lambda>n. u (n+k)) = liminf u"
   2.855 +proof (induction k)
   2.856 +  case (Suc k)
   2.857 +  have "liminf (\<lambda>n. u (n+k+1)) = liminf (\<lambda>n. u (n+k))" using liminf_shift[where ?u="\<lambda>n. u(n+k)"] by simp
   2.858 +  then show ?case using Suc.IH by simp
   2.859 +qed (auto)
   2.860 +
   2.861 +lemma Limsup_obtain:
   2.862 +  fixes u::"_ \<Rightarrow> 'a :: complete_linorder"
   2.863 +  assumes "Limsup F u > c"
   2.864 +  shows "\<exists>i. u i > c"
   2.865 +proof -
   2.866 +  have "(INF P:{P. eventually P F}. SUP x:{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
   2.867 +  then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff)
   2.868 +qed
   2.869 +
   2.870 +text \<open>The next lemma is extremely useful, as it often makes it possible to reduce statements
   2.871 +about limsups to statements about limits.\<close>
   2.872 +
   2.873 +lemma limsup_subseq_lim:
   2.874 +  fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   2.875 +  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> limsup u"
   2.876 +proof (cases)
   2.877 +  assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<le> u p"
   2.878 +  then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<le> u (r n)) \<and> r n < r (Suc n)"
   2.879 +    by (intro dependent_nat_choice) (auto simp: conj_commute)
   2.880 +  then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<le> u (r n)"
   2.881 +    by (auto simp: strict_mono_Suc_iff)
   2.882 +  define umax where "umax = (\<lambda>n. (SUP m:{n..}. u m))"
   2.883 +  have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
   2.884 +  then have "umax \<longlonglongrightarrow> limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
   2.885 +  then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
   2.886 +  have "\<And>n. umax(r n) = u(r n)" unfolding umax_def using mono
   2.887 +    by (metis SUP_le_iff antisym atLeast_def mem_Collect_eq order_refl)
   2.888 +  then have "umax o r = u o r" unfolding o_def by simp
   2.889 +  then have "(u o r) \<longlonglongrightarrow> limsup u" using * by simp
   2.890 +  then show ?thesis using \<open>strict_mono r\<close> by blast
   2.891 +next
   2.892 +  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<le> u p))"
   2.893 +  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p < u m" by (force simp: not_le le_less)
   2.894 +  have "\<exists>r. \<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<le> u (r (Suc n)))"
   2.895 +  proof (rule dependent_nat_choice)
   2.896 +    fix x assume "N < x"
   2.897 +    then have a: "finite {N<..x}" "{N<..x} \<noteq> {}" by simp_all
   2.898 +    have "Max {u i |i. i \<in> {N<..x}} \<in> {u i |i. i \<in> {N<..x}}" apply (rule Max_in) using a by (auto)
   2.899 +    then obtain p where "p \<in> {N<..x}" and upmax: "u p = Max{u i |i. i \<in> {N<..x}}" by auto
   2.900 +    define U where "U = {m. m > p \<and> u p < u m}"
   2.901 +    have "U \<noteq> {}" unfolding U_def using N[of p] \<open>p \<in> {N<..x}\<close> by auto
   2.902 +    define y where "y = Inf U"
   2.903 +    then have "y \<in> U" using \<open>U \<noteq> {}\<close> by (simp add: Inf_nat_def1)
   2.904 +    have a: "\<And>i. i \<in> {N<..x} \<Longrightarrow> u i \<le> u p"
   2.905 +    proof -
   2.906 +      fix i assume "i \<in> {N<..x}"
   2.907 +      then have "u i \<in> {u i |i. i \<in> {N<..x}}" by blast
   2.908 +      then show "u i \<le> u p" using upmax by simp
   2.909 +    qed
   2.910 +    moreover have "u p < u y" using \<open>y \<in> U\<close> U_def by auto
   2.911 +    ultimately have "y \<notin> {N<..x}" using not_le by blast
   2.912 +    moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
   2.913 +    ultimately have "y > x" by auto
   2.914 +
   2.915 +    have "\<And>i. i \<in> {N<..y} \<Longrightarrow> u i \<le> u y"
   2.916 +    proof -
   2.917 +      fix i assume "i \<in> {N<..y}" show "u i \<le> u y"
   2.918 +      proof (cases)
   2.919 +        assume "i = y"
   2.920 +        then show ?thesis by simp
   2.921 +      next
   2.922 +        assume "\<not>(i=y)"
   2.923 +        then have i:"i \<in> {N<..<y}" using \<open>i \<in> {N<..y}\<close> by simp
   2.924 +        have "u i \<le> u p"
   2.925 +        proof (cases)
   2.926 +          assume "i \<le> x"
   2.927 +          then have "i \<in> {N<..x}" using i by simp
   2.928 +          then show ?thesis using a by simp
   2.929 +        next
   2.930 +          assume "\<not>(i \<le> x)"
   2.931 +          then have "i > x" by simp
   2.932 +          then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
   2.933 +          have "i < Inf U" using i y_def by simp
   2.934 +          then have "i \<notin> U" using Inf_nat_def not_less_Least by auto
   2.935 +          then show ?thesis using U_def * by auto
   2.936 +        qed
   2.937 +        then show "u i \<le> u y" using \<open>u p < u y\<close> by auto
   2.938 +      qed
   2.939 +    qed
   2.940 +    then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
   2.941 +    then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" by auto
   2.942 +  qed (auto)
   2.943 +  then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<le> u (r (Suc n)))" by auto
   2.944 +  have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
   2.945 +  have "incseq (u o r)" unfolding o_def using r by (simp add: incseq_SucI order.strict_implies_order)
   2.946 +  then have "(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)" using LIMSEQ_SUP by blast
   2.947 +  then have "limsup (u o r) = (SUP n. (u o r) n)" by (simp add: lim_imp_Limsup)
   2.948 +  moreover have "limsup (u o r) \<le> limsup u" using \<open>strict_mono r\<close> by (simp add: limsup_subseq_mono)
   2.949 +  ultimately have "(SUP n. (u o r) n) \<le> limsup u" by simp
   2.950 +
   2.951 +  {
   2.952 +    fix i assume i: "i \<in> {N<..}"
   2.953 +    obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
   2.954 +    then have "i \<in> {N<..r(Suc n)}" using i by simp
   2.955 +    then have "u i \<le> u (r(Suc n))" using r by simp
   2.956 +    then have "u i \<le> (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
   2.957 +  }
   2.958 +  then have "(SUP i:{N<..}. u i) \<le> (SUP n. (u o r) n)" using SUP_least by blast
   2.959 +  then have "limsup u \<le> (SUP n. (u o r) n)" unfolding Limsup_def
   2.960 +    by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
   2.961 +  then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
   2.962 +  then have "(u o r) \<longlonglongrightarrow> limsup u" using \<open>(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)\<close> by simp
   2.963 +  then show ?thesis using \<open>strict_mono r\<close> by auto
   2.964 +qed
   2.965 +
   2.966 +lemma liminf_subseq_lim:
   2.967 +  fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   2.968 +  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> liminf u"
   2.969 +proof (cases)
   2.970 +  assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<ge> u p"
   2.971 +  then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<ge> u (r n)) \<and> r n < r (Suc n)"
   2.972 +    by (intro dependent_nat_choice) (auto simp: conj_commute)
   2.973 +  then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<ge> u (r n)"
   2.974 +    by (auto simp: strict_mono_Suc_iff)
   2.975 +  define umin where "umin = (\<lambda>n. (INF m:{n..}. u m))"
   2.976 +  have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
   2.977 +  then have "umin \<longlonglongrightarrow> liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
   2.978 +  then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
   2.979 +  have "\<And>n. umin(r n) = u(r n)" unfolding umin_def using mono
   2.980 +    by (metis le_INF_iff antisym atLeast_def mem_Collect_eq order_refl)
   2.981 +  then have "umin o r = u o r" unfolding o_def by simp
   2.982 +  then have "(u o r) \<longlonglongrightarrow> liminf u" using * by simp
   2.983 +  then show ?thesis using \<open>strict_mono r\<close> by blast
   2.984 +next
   2.985 +  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<ge> u p))"
   2.986 +  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p > u m" by (force simp: not_le le_less)
   2.987 +  have "\<exists>r. \<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))"
   2.988 +  proof (rule dependent_nat_choice)
   2.989 +    fix x assume "N < x"
   2.990 +    then have a: "finite {N<..x}" "{N<..x} \<noteq> {}" by simp_all
   2.991 +    have "Min {u i |i. i \<in> {N<..x}} \<in> {u i |i. i \<in> {N<..x}}" apply (rule Min_in) using a by (auto)
   2.992 +    then obtain p where "p \<in> {N<..x}" and upmin: "u p = Min{u i |i. i \<in> {N<..x}}" by auto
   2.993 +    define U where "U = {m. m > p \<and> u p > u m}"
   2.994 +    have "U \<noteq> {}" unfolding U_def using N[of p] \<open>p \<in> {N<..x}\<close> by auto
   2.995 +    define y where "y = Inf U"
   2.996 +    then have "y \<in> U" using \<open>U \<noteq> {}\<close> by (simp add: Inf_nat_def1)
   2.997 +    have a: "\<And>i. i \<in> {N<..x} \<Longrightarrow> u i \<ge> u p"
   2.998 +    proof -
   2.999 +      fix i assume "i \<in> {N<..x}"
  2.1000 +      then have "u i \<in> {u i |i. i \<in> {N<..x}}" by blast
  2.1001 +      then show "u i \<ge> u p" using upmin by simp
  2.1002 +    qed
  2.1003 +    moreover have "u p > u y" using \<open>y \<in> U\<close> U_def by auto
  2.1004 +    ultimately have "y \<notin> {N<..x}" using not_le by blast
  2.1005 +    moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
  2.1006 +    ultimately have "y > x" by auto
  2.1007 +
  2.1008 +    have "\<And>i. i \<in> {N<..y} \<Longrightarrow> u i \<ge> u y"
  2.1009 +    proof -
  2.1010 +      fix i assume "i \<in> {N<..y}" show "u i \<ge> u y"
  2.1011 +      proof (cases)
  2.1012 +        assume "i = y"
  2.1013 +        then show ?thesis by simp
  2.1014 +      next
  2.1015 +        assume "\<not>(i=y)"
  2.1016 +        then have i:"i \<in> {N<..<y}" using \<open>i \<in> {N<..y}\<close> by simp
  2.1017 +        have "u i \<ge> u p"
  2.1018 +        proof (cases)
  2.1019 +          assume "i \<le> x"
  2.1020 +          then have "i \<in> {N<..x}" using i by simp
  2.1021 +          then show ?thesis using a by simp
  2.1022 +        next
  2.1023 +          assume "\<not>(i \<le> x)"
  2.1024 +          then have "i > x" by simp
  2.1025 +          then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
  2.1026 +          have "i < Inf U" using i y_def by simp
  2.1027 +          then have "i \<notin> U" using Inf_nat_def not_less_Least by auto
  2.1028 +          then show ?thesis using U_def * by auto
  2.1029 +        qed
  2.1030 +        then show "u i \<ge> u y" using \<open>u p > u y\<close> by auto
  2.1031 +      qed
  2.1032 +    qed
  2.1033 +    then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
  2.1034 +    then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" by auto
  2.1035 +  qed (auto)
  2.1036 +  then obtain r :: "nat \<Rightarrow> nat" 
  2.1037 +    where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))" by auto
  2.1038 +  have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
  2.1039 +  have "decseq (u o r)" unfolding o_def using r by (simp add: decseq_SucI order.strict_implies_order)
  2.1040 +  then have "(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)" using LIMSEQ_INF by blast
  2.1041 +  then have "liminf (u o r) = (INF n. (u o r) n)" by (simp add: lim_imp_Liminf)
  2.1042 +  moreover have "liminf (u o r) \<ge> liminf u" using \<open>strict_mono r\<close> by (simp add: liminf_subseq_mono)
  2.1043 +  ultimately have "(INF n. (u o r) n) \<ge> liminf u" by simp
  2.1044 +
  2.1045 +  {
  2.1046 +    fix i assume i: "i \<in> {N<..}"
  2.1047 +    obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
  2.1048 +    then have "i \<in> {N<..r(Suc n)}" using i by simp
  2.1049 +    then have "u i \<ge> u (r(Suc n))" using r by simp
  2.1050 +    then have "u i \<ge> (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
  2.1051 +  }
  2.1052 +  then have "(INF i:{N<..}. u i) \<ge> (INF n. (u o r) n)" using INF_greatest by blast
  2.1053 +  then have "liminf u \<ge> (INF n. (u o r) n)" unfolding Liminf_def
  2.1054 +    by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
  2.1055 +  then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
  2.1056 +  then have "(u o r) \<longlonglongrightarrow> liminf u" using \<open>(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)\<close> by simp
  2.1057 +  then show ?thesis using \<open>strict_mono r\<close> by auto
  2.1058 +qed
  2.1059 +
  2.1060 +text \<open>The following statement about limsups is reduced to a statement about limits using
  2.1061 +subsequences thanks to \verb+limsup_subseq_lim+. The statement for limits follows for instance from
  2.1062 +\verb+tendsto_add_ereal_general+.\<close>
  2.1063 +
  2.1064 +lemma ereal_limsup_add_mono:
  2.1065 +  fixes u v::"nat \<Rightarrow> ereal"
  2.1066 +  shows "limsup (\<lambda>n. u n + v n) \<le> limsup u + limsup v"
  2.1067 +proof (cases)
  2.1068 +  assume "(limsup u = \<infinity>) \<or> (limsup v = \<infinity>)"
  2.1069 +  then have "limsup u + limsup v = \<infinity>" by simp
  2.1070 +  then show ?thesis by auto
  2.1071 +next
  2.1072 +  assume "\<not>((limsup u = \<infinity>) \<or> (limsup v = \<infinity>))"
  2.1073 +  then have "limsup u < \<infinity>" "limsup v < \<infinity>" by auto
  2.1074 +
  2.1075 +  define w where "w = (\<lambda>n. u n + v n)"
  2.1076 +  obtain r where r: "strict_mono r" "(w o r) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
  2.1077 +  obtain s where s: "strict_mono s" "(u o r o s) \<longlonglongrightarrow> limsup (u o r)" using limsup_subseq_lim by auto
  2.1078 +  obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
  2.1079 +
  2.1080 +  define a where "a = r o s o t"
  2.1081 +  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
  2.1082 +  have l:"(w o a) \<longlonglongrightarrow> limsup w"
  2.1083 +         "(u o a) \<longlonglongrightarrow> limsup (u o r)"
  2.1084 +         "(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
  2.1085 +  apply (metis (no_types, lifting) r(2) s(1) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  2.1086 +  apply (metis (no_types, lifting) s(2) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  2.1087 +  apply (metis (no_types, lifting) t(2) a_def comp_assoc)
  2.1088 +  done
  2.1089 +
  2.1090 +  have "limsup (u o r) \<le> limsup u" by (simp add: limsup_subseq_mono r(1))
  2.1091 +  then have a: "limsup (u o r) \<noteq> \<infinity>" using \<open>limsup u < \<infinity>\<close> by auto
  2.1092 +  have "limsup (v o r o s) \<le> limsup v" 
  2.1093 +    by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) strict_mono_o)
  2.1094 +  then have b: "limsup (v o r o s) \<noteq> \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
  2.1095 +
  2.1096 +  have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)"
  2.1097 +    using l tendsto_add_ereal_general a b by fastforce
  2.1098 +  moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
  2.1099 +  ultimately have "(w o a) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)" by simp
  2.1100 +  then have "limsup w = limsup (u o r) + limsup (v o r o s)" using l(1) LIMSEQ_unique by blast
  2.1101 +  then have "limsup w \<le> limsup u + limsup v"
  2.1102 +    using \<open>limsup (u o r) \<le> limsup u\<close> \<open>limsup (v o r o s) \<le> limsup v\<close> ereal_add_mono by simp
  2.1103 +  then show ?thesis unfolding w_def by simp
  2.1104 +qed
  2.1105 +
  2.1106 +text \<open>There is an asymmetry between liminfs and limsups in ereal, as $\infty + (-\infty) = \infty$.
  2.1107 +This explains why there are more assumptions in the next lemma dealing with liminfs that in the
  2.1108 +previous one about limsups.\<close>
  2.1109 +
  2.1110 +lemma ereal_liminf_add_mono:
  2.1111 +  fixes u v::"nat \<Rightarrow> ereal"
  2.1112 +  assumes "\<not>((liminf u = \<infinity> \<and> liminf v = -\<infinity>) \<or> (liminf u = -\<infinity> \<and> liminf v = \<infinity>))"
  2.1113 +  shows "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
  2.1114 +proof (cases)
  2.1115 +  assume "(liminf u = -\<infinity>) \<or> (liminf v = -\<infinity>)"
  2.1116 +  then have *: "liminf u + liminf v = -\<infinity>" using assms by auto
  2.1117 +  show ?thesis by (simp add: *)
  2.1118 +next
  2.1119 +  assume "\<not>((liminf u = -\<infinity>) \<or> (liminf v = -\<infinity>))"
  2.1120 +  then have "liminf u > -\<infinity>" "liminf v > -\<infinity>" by auto
  2.1121 +
  2.1122 +  define w where "w = (\<lambda>n. u n + v n)"
  2.1123 +  obtain r where r: "strict_mono r" "(w o r) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
  2.1124 +  obtain s where s: "strict_mono s" "(u o r o s) \<longlonglongrightarrow> liminf (u o r)" using liminf_subseq_lim by auto
  2.1125 +  obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> liminf (v o r o s)" using liminf_subseq_lim by auto
  2.1126 +
  2.1127 +  define a where "a = r o s o t"
  2.1128 +  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
  2.1129 +  have l:"(w o a) \<longlonglongrightarrow> liminf w"
  2.1130 +         "(u o a) \<longlonglongrightarrow> liminf (u o r)"
  2.1131 +         "(v o a) \<longlonglongrightarrow> liminf (v o r o s)"
  2.1132 +  apply (metis (no_types, lifting) r(2) s(1) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  2.1133 +  apply (metis (no_types, lifting) s(2) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  2.1134 +  apply (metis (no_types, lifting) t(2) a_def comp_assoc)
  2.1135 +  done
  2.1136 +
  2.1137 +  have "liminf (u o r) \<ge> liminf u" by (simp add: liminf_subseq_mono r(1))
  2.1138 +  then have a: "liminf (u o r) \<noteq> -\<infinity>" using \<open>liminf u > -\<infinity>\<close> by auto
  2.1139 +  have "liminf (v o r o s) \<ge> liminf v" 
  2.1140 +    by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) strict_mono_o)
  2.1141 +  then have b: "liminf (v o r o s) \<noteq> -\<infinity>" using \<open>liminf v > -\<infinity>\<close> by auto
  2.1142 +
  2.1143 +  have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)"
  2.1144 +    using l tendsto_add_ereal_general a b by fastforce
  2.1145 +  moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
  2.1146 +  ultimately have "(w o a) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)" by simp
  2.1147 +  then have "liminf w = liminf (u o r) + liminf (v o r o s)" using l(1) LIMSEQ_unique by blast
  2.1148 +  then have "liminf w \<ge> liminf u + liminf v"
  2.1149 +    using \<open>liminf (u o r) \<ge> liminf u\<close> \<open>liminf (v o r o s) \<ge> liminf v\<close> ereal_add_mono by simp
  2.1150 +  then show ?thesis unfolding w_def by simp
  2.1151 +qed
  2.1152 +
  2.1153 +lemma ereal_limsup_lim_add:
  2.1154 +  fixes u v::"nat \<Rightarrow> ereal"
  2.1155 +  assumes "u \<longlonglongrightarrow> a" "abs(a) \<noteq> \<infinity>"
  2.1156 +  shows "limsup (\<lambda>n. u n + v n) = a + limsup v"
  2.1157 +proof -
  2.1158 +  have "limsup u = a" using assms(1) using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  2.1159 +  have "(\<lambda>n. -u n) \<longlonglongrightarrow> -a" using assms(1) by auto
  2.1160 +  then have "limsup (\<lambda>n. -u n) = -a" using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  2.1161 +
  2.1162 +  have "limsup (\<lambda>n. u n + v n) \<le> limsup u + limsup v"
  2.1163 +    by (rule ereal_limsup_add_mono)
  2.1164 +  then have up: "limsup (\<lambda>n. u n + v n) \<le> a + limsup v" using \<open>limsup u = a\<close> by simp
  2.1165 +
  2.1166 +  have a: "limsup (\<lambda>n. (u n + v n) + (-u n)) \<le> limsup (\<lambda>n. u n + v n) + limsup (\<lambda>n. -u n)"
  2.1167 +    by (rule ereal_limsup_add_mono)
  2.1168 +  have "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) sequentially" using assms
  2.1169 +    real_lim_then_eventually_real by auto
  2.1170 +  moreover have "\<And>x. x = ereal(real_of_ereal(x)) \<Longrightarrow> x + (-x) = 0"
  2.1171 +    by (metis plus_ereal.simps(1) right_minus uminus_ereal.simps(1) zero_ereal_def)
  2.1172 +  ultimately have "eventually (\<lambda>n. u n + (-u n) = 0) sequentially"
  2.1173 +    by (metis (mono_tags, lifting) eventually_mono)
  2.1174 +  moreover have "\<And>n. u n + (-u n) = 0 \<Longrightarrow> u n + v n + (-u n) = v n"
  2.1175 +    by (metis add.commute add.left_commute add.left_neutral)
  2.1176 +  ultimately have "eventually (\<lambda>n. u n + v n + (-u n) = v n) sequentially"
  2.1177 +    using eventually_mono by force
  2.1178 +  then have "limsup v = limsup (\<lambda>n. u n + v n + (-u n))" using Limsup_eq by force
  2.1179 +  then have "limsup v \<le> limsup (\<lambda>n. u n + v n) -a" using a \<open>limsup (\<lambda>n. -u n) = -a\<close> by (simp add: minus_ereal_def)
  2.1180 +  then have "limsup (\<lambda>n. u n + v n) \<ge> a + limsup v" using assms(2) by (metis add.commute ereal_le_minus)
  2.1181 +  then show ?thesis using up by simp
  2.1182 +qed
  2.1183 +
  2.1184 +lemma ereal_limsup_lim_mult:
  2.1185 +  fixes u v::"nat \<Rightarrow> ereal"
  2.1186 +  assumes "u \<longlonglongrightarrow> a" "a>0" "a \<noteq> \<infinity>"
  2.1187 +  shows "limsup (\<lambda>n. u n * v n) = a * limsup v"
  2.1188 +proof -
  2.1189 +  define w where "w = (\<lambda>n. u n * v n)"
  2.1190 +  obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
  2.1191 +  have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
  2.1192 +  with tendsto_mult_ereal[OF this r(2)] have "(\<lambda>n. (u o r) n * (v o r) n) \<longlonglongrightarrow> a * limsup v" using assms(2) assms(3) by auto
  2.1193 +  moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
  2.1194 +  ultimately have "(w o r) \<longlonglongrightarrow> a * limsup v" unfolding w_def by presburger
  2.1195 +  then have "limsup (w o r) = a * limsup v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  2.1196 +  then have I: "limsup w \<ge> a * limsup v" by (metis limsup_subseq_mono r(1))
  2.1197 +
  2.1198 +  obtain s where s: "strict_mono s" "(w o s) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
  2.1199 +  have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
  2.1200 +  have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
  2.1201 +  moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
  2.1202 +  moreover have "(w o s) n / (u o s) n = (v o s) n" if "(u o s) n > 0" "(u o s) n < \<infinity>" for n
  2.1203 +    unfolding w_def using that by (auto simp add: ereal_divide_eq)
  2.1204 +  ultimately have "eventually (\<lambda>n. (w o s) n / (u o s) n = (v o s) n) sequentially" using eventually_elim2 by force
  2.1205 +  moreover have "(\<lambda>n. (w o s) n / (u o s) n) \<longlonglongrightarrow> (limsup w) / a"
  2.1206 +    apply (rule tendsto_divide_ereal[OF s(2) *]) using assms(2) assms(3) by auto
  2.1207 +  ultimately have "(v o s) \<longlonglongrightarrow> (limsup w) / a" using Lim_transform_eventually by fastforce
  2.1208 +  then have "limsup (v o s) = (limsup w) / a" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  2.1209 +  then have "limsup v \<ge> (limsup w) / a" by (metis limsup_subseq_mono s(1))
  2.1210 +  then have "a * limsup v \<ge> limsup w" using assms(2) assms(3) by (simp add: ereal_divide_le_pos)
  2.1211 +  then show ?thesis using I unfolding w_def by auto
  2.1212 +qed
  2.1213 +
  2.1214 +lemma ereal_liminf_lim_mult:
  2.1215 +  fixes u v::"nat \<Rightarrow> ereal"
  2.1216 +  assumes "u \<longlonglongrightarrow> a" "a>0" "a \<noteq> \<infinity>"
  2.1217 +  shows "liminf (\<lambda>n. u n * v n) = a * liminf v"
  2.1218 +proof -
  2.1219 +  define w where "w = (\<lambda>n. u n * v n)"
  2.1220 +  obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
  2.1221 +  have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
  2.1222 +  with tendsto_mult_ereal[OF this r(2)] have "(\<lambda>n. (u o r) n * (v o r) n) \<longlonglongrightarrow> a * liminf v" using assms(2) assms(3) by auto
  2.1223 +  moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
  2.1224 +  ultimately have "(w o r) \<longlonglongrightarrow> a * liminf v" unfolding w_def by presburger
  2.1225 +  then have "liminf (w o r) = a * liminf v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  2.1226 +  then have I: "liminf w \<le> a * liminf v" by (metis liminf_subseq_mono r(1))
  2.1227 +
  2.1228 +  obtain s where s: "strict_mono s" "(w o s) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
  2.1229 +  have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
  2.1230 +  have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
  2.1231 +  moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
  2.1232 +  moreover have "(w o s) n / (u o s) n = (v o s) n" if "(u o s) n > 0" "(u o s) n < \<infinity>" for n
  2.1233 +    unfolding w_def using that by (auto simp add: ereal_divide_eq)
  2.1234 +  ultimately have "eventually (\<lambda>n. (w o s) n / (u o s) n = (v o s) n) sequentially" using eventually_elim2 by force
  2.1235 +  moreover have "(\<lambda>n. (w o s) n / (u o s) n) \<longlonglongrightarrow> (liminf w) / a"
  2.1236 +    apply (rule tendsto_divide_ereal[OF s(2) *]) using assms(2) assms(3) by auto
  2.1237 +  ultimately have "(v o s) \<longlonglongrightarrow> (liminf w) / a" using Lim_transform_eventually by fastforce
  2.1238 +  then have "liminf (v o s) = (liminf w) / a" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  2.1239 +  then have "liminf v \<le> (liminf w) / a" by (metis liminf_subseq_mono s(1))
  2.1240 +  then have "a * liminf v \<le> liminf w" using assms(2) assms(3) by (simp add: ereal_le_divide_pos)
  2.1241 +  then show ?thesis using I unfolding w_def by auto
  2.1242 +qed
  2.1243 +
  2.1244 +lemma ereal_liminf_lim_add:
  2.1245 +  fixes u v::"nat \<Rightarrow> ereal"
  2.1246 +  assumes "u \<longlonglongrightarrow> a" "abs(a) \<noteq> \<infinity>"
  2.1247 +  shows "liminf (\<lambda>n. u n + v n) = a + liminf v"
  2.1248 +proof -
  2.1249 +  have "liminf u = a" using assms(1) tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  2.1250 +  then have *: "abs(liminf u) \<noteq> \<infinity>" using assms(2) by auto
  2.1251 +  have "(\<lambda>n. -u n) \<longlonglongrightarrow> -a" using assms(1) by auto
  2.1252 +  then have "liminf (\<lambda>n. -u n) = -a" using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  2.1253 +  then have **: "abs(liminf (\<lambda>n. -u n)) \<noteq> \<infinity>" using assms(2) by auto
  2.1254 +
  2.1255 +  have "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
  2.1256 +    apply (rule ereal_liminf_add_mono) using * by auto
  2.1257 +  then have up: "liminf (\<lambda>n. u n + v n) \<ge> a + liminf v" using \<open>liminf u = a\<close> by simp
  2.1258 +
  2.1259 +  have a: "liminf (\<lambda>n. (u n + v n) + (-u n)) \<ge> liminf (\<lambda>n. u n + v n) + liminf (\<lambda>n. -u n)"
  2.1260 +    apply (rule ereal_liminf_add_mono) using ** by auto
  2.1261 +  have "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) sequentially" using assms
  2.1262 +    real_lim_then_eventually_real by auto
  2.1263 +  moreover have "\<And>x. x = ereal(real_of_ereal(x)) \<Longrightarrow> x + (-x) = 0"
  2.1264 +    by (metis plus_ereal.simps(1) right_minus uminus_ereal.simps(1) zero_ereal_def)
  2.1265 +  ultimately have "eventually (\<lambda>n. u n + (-u n) = 0) sequentially"
  2.1266 +    by (metis (mono_tags, lifting) eventually_mono)
  2.1267 +  moreover have "\<And>n. u n + (-u n) = 0 \<Longrightarrow> u n + v n + (-u n) = v n"
  2.1268 +    by (metis add.commute add.left_commute add.left_neutral)
  2.1269 +  ultimately have "eventually (\<lambda>n. u n + v n + (-u n) = v n) sequentially"
  2.1270 +    using eventually_mono by force
  2.1271 +  then have "liminf v = liminf (\<lambda>n. u n + v n + (-u n))" using Liminf_eq by force
  2.1272 +  then have "liminf v \<ge> liminf (\<lambda>n. u n + v n) -a" using a \<open>liminf (\<lambda>n. -u n) = -a\<close> by (simp add: minus_ereal_def)
  2.1273 +  then have "liminf (\<lambda>n. u n + v n) \<le> a + liminf v" using assms(2) by (metis add.commute ereal_minus_le)
  2.1274 +  then show ?thesis using up by simp
  2.1275 +qed
  2.1276 +
  2.1277 +lemma ereal_liminf_limsup_add:
  2.1278 +  fixes u v::"nat \<Rightarrow> ereal"
  2.1279 +  shows "liminf (\<lambda>n. u n + v n) \<le> liminf u + limsup v"
  2.1280 +proof (cases)
  2.1281 +  assume "limsup v = \<infinity> \<or> liminf u = \<infinity>"
  2.1282 +  then show ?thesis by auto
  2.1283 +next
  2.1284 +  assume "\<not>(limsup v = \<infinity> \<or> liminf u = \<infinity>)"
  2.1285 +  then have "limsup v < \<infinity>" "liminf u < \<infinity>" by auto
  2.1286 +
  2.1287 +  define w where "w = (\<lambda>n. u n + v n)"
  2.1288 +  obtain r where r: "strict_mono r" "(u o r) \<longlonglongrightarrow> liminf u" using liminf_subseq_lim by auto
  2.1289 +  obtain s where s: "strict_mono s" "(w o r o s) \<longlonglongrightarrow> liminf (w o r)" using liminf_subseq_lim by auto
  2.1290 +  obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
  2.1291 +
  2.1292 +  define a where "a = r o s o t"
  2.1293 +  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
  2.1294 +  have l:"(u o a) \<longlonglongrightarrow> liminf u"
  2.1295 +         "(w o a) \<longlonglongrightarrow> liminf (w o r)"
  2.1296 +         "(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
  2.1297 +  apply (metis (no_types, lifting) r(2) s(1) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  2.1298 +  apply (metis (no_types, lifting) s(2) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  2.1299 +  apply (metis (no_types, lifting) t(2) a_def comp_assoc)
  2.1300 +  done
  2.1301 +
  2.1302 +  have "liminf (w o r) \<ge> liminf w" by (simp add: liminf_subseq_mono r(1))
  2.1303 +  have "limsup (v o r o s) \<le> limsup v" 
  2.1304 +    by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) strict_mono_o)
  2.1305 +  then have b: "limsup (v o r o s) < \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
  2.1306 +
  2.1307 +  have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf u + limsup (v o r o s)"
  2.1308 +    apply (rule tendsto_add_ereal_general) using b \<open>liminf u < \<infinity>\<close> l(1) l(3) by force+
  2.1309 +  moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
  2.1310 +  ultimately have "(w o a) \<longlonglongrightarrow> liminf u + limsup (v o r o s)" by simp
  2.1311 +  then have "liminf (w o r) = liminf u + limsup (v o r o s)" using l(2) using LIMSEQ_unique by blast
  2.1312 +  then have "liminf w \<le> liminf u + limsup v"
  2.1313 +    using \<open>liminf (w o r) \<ge> liminf w\<close> \<open>limsup (v o r o s) \<le> limsup v\<close>
  2.1314 +    by (metis add_mono_thms_linordered_semiring(2) le_less_trans not_less)
  2.1315 +  then show ?thesis unfolding w_def by simp
  2.1316 +qed
  2.1317 +
  2.1318 +lemma ereal_liminf_limsup_minus:
  2.1319 +  fixes u v::"nat \<Rightarrow> ereal"
  2.1320 +  shows "liminf (\<lambda>n. u n - v n) \<le> limsup u - limsup v"
  2.1321 +  unfolding minus_ereal_def
  2.1322 +  apply (subst add.commute)
  2.1323 +  apply (rule order_trans[OF ereal_liminf_limsup_add])
  2.1324 +  using ereal_Limsup_uminus[of sequentially "\<lambda>n. - v n"]
  2.1325 +  apply (simp add: add.commute)
  2.1326 +  done
  2.1327 +
  2.1328 +
  2.1329 +lemma liminf_minus_ennreal:
  2.1330 +  fixes u v::"nat \<Rightarrow> ennreal"
  2.1331 +  shows "(\<And>n. v n \<le> u n) \<Longrightarrow> liminf (\<lambda>n. u n - v n) \<le> limsup u - limsup v"
  2.1332 +  unfolding liminf_SUP_INF limsup_INF_SUP
  2.1333 +  including ennreal.lifting
  2.1334 +proof (transfer, clarsimp)
  2.1335 +  fix v u :: "nat \<Rightarrow> ereal" assume *: "\<forall>x. 0 \<le> v x" "\<forall>x. 0 \<le> u x" "\<And>n. v n \<le> u n"
  2.1336 +  moreover have "0 \<le> limsup u - limsup v"
  2.1337 +    using * by (intro ereal_diff_positive Limsup_mono always_eventually) simp
  2.1338 +  moreover have "0 \<le> (SUPREMUM {x..} v)" for x
  2.1339 +    using * by (intro SUP_upper2[of x]) auto
  2.1340 +  moreover have "0 \<le> (SUPREMUM {x..} u)" for x
  2.1341 +    using * by (intro SUP_upper2[of x]) auto
  2.1342 +  ultimately show "(SUP n. INF n:{n..}. max 0 (u n - v n))
  2.1343 +            \<le> max 0 ((INF x. max 0 (SUPREMUM {x..} u)) - (INF x. max 0 (SUPREMUM {x..} v)))"
  2.1344 +    by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
  2.1345 +qed
  2.1346 +
  2.1347  subsection "Relate extended reals and the indicator function"
  2.1348  
  2.1349  lemma ereal_indicator_le_0: "(indicator S x::ereal) \<le> 0 \<longleftrightarrow> x \<notin> S"
     3.1 --- a/src/HOL/Analysis/Path_Connected.thy	Fri Aug 18 22:55:54 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Sun Aug 20 03:35:20 2017 +0200
     3.3 @@ -6747,6 +6747,16 @@
     3.4      by (metis countable_subset)
     3.5  qed
     3.6  
     3.7 +lemma ball_minus_countable_nonempty:
     3.8 +  assumes "countable (A :: 'a :: euclidean_space set)" "r > 0"
     3.9 +  shows   "ball z r - A \<noteq> {}"
    3.10 +proof
    3.11 +  assume *: "ball z r - A = {}"
    3.12 +  have "uncountable (ball z r - A)"
    3.13 +    by (intro uncountable_minus_countable assms uncountable_ball)
    3.14 +  thus False by (subst (asm) *) auto
    3.15 +qed
    3.16 +
    3.17  lemma uncountable_cball:
    3.18    fixes a :: "'a::euclidean_space"
    3.19    assumes "r > 0"
     4.1 --- a/src/HOL/Analysis/Set_Integral.thy	Fri Aug 18 22:55:54 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Sun Aug 20 03:35:20 2017 +0200
     4.3 @@ -11,1343 +11,6 @@
     4.4    imports Radon_Nikodym
     4.5  begin
     4.6  
     4.7 -lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y" (* COPIED FROM Permutations *)
     4.8 -  using surj_f_inv_f[of p] by (auto simp add: bij_def)
     4.9 -
    4.10 -subsection \<open>Fun.thy\<close>
    4.11 -
    4.12 -lemma inj_fn:
    4.13 -  fixes f::"'a \<Rightarrow> 'a"
    4.14 -  assumes "inj f"
    4.15 -  shows "inj (f^^n)"
    4.16 -proof (induction n)
    4.17 -  case (Suc n)
    4.18 -  have "inj (f o (f^^n))"
    4.19 -    using inj_comp[OF assms Suc.IH] by simp
    4.20 -  then show "inj (f^^(Suc n))"
    4.21 -    by auto
    4.22 -qed (auto)
    4.23 -
    4.24 -lemma surj_fn:
    4.25 -  fixes f::"'a \<Rightarrow> 'a"
    4.26 -  assumes "surj f"
    4.27 -  shows "surj (f^^n)"
    4.28 -proof (induction n)
    4.29 -  case (Suc n)
    4.30 -  have "surj (f o (f^^n))"
    4.31 -    using assms Suc.IH by (simp add: comp_surj)
    4.32 -  then show "surj (f^^(Suc n))"
    4.33 -    by auto
    4.34 -qed (auto)
    4.35 -
    4.36 -lemma bij_fn:
    4.37 -  fixes f::"'a \<Rightarrow> 'a"
    4.38 -  assumes "bij f"
    4.39 -  shows "bij (f^^n)"
    4.40 -by (rule bijI[OF inj_fn[OF bij_is_inj[OF assms]] surj_fn[OF bij_is_surj[OF assms]]])
    4.41 -
    4.42 -lemma inv_fn_o_fn_is_id:
    4.43 -  fixes f::"'a \<Rightarrow> 'a"
    4.44 -  assumes "bij f"
    4.45 -  shows "((inv f)^^n) o (f^^n) = (\<lambda>x. x)"
    4.46 -proof -
    4.47 -  have "((inv f)^^n)((f^^n) x) = x" for x n
    4.48 -  proof (induction n)
    4.49 -    case (Suc n)
    4.50 -    have *: "(inv f) (f y) = y" for y
    4.51 -      by (simp add: assms bij_is_inj)
    4.52 -    have "(inv f ^^ Suc n) ((f ^^ Suc n) x) = (inv f^^n) (inv f (f ((f^^n) x)))"
    4.53 -      by (simp add: funpow_swap1)
    4.54 -    also have "... = (inv f^^n) ((f^^n) x)"
    4.55 -      using * by auto
    4.56 -    also have "... = x" using Suc.IH by auto
    4.57 -    finally show ?case by simp
    4.58 -  qed (auto)
    4.59 -  then show ?thesis unfolding o_def by blast
    4.60 -qed
    4.61 -
    4.62 -lemma fn_o_inv_fn_is_id:
    4.63 -  fixes f::"'a \<Rightarrow> 'a"
    4.64 -  assumes "bij f"
    4.65 -  shows "(f^^n) o ((inv f)^^n) = (\<lambda>x. x)"
    4.66 -proof -
    4.67 -  have "(f^^n) (((inv f)^^n) x) = x" for x n
    4.68 -  proof (induction n)
    4.69 -    case (Suc n)
    4.70 -    have *: "f(inv f y) = y" for y
    4.71 -      using assms by (meson bij_inv_eq_iff)
    4.72 -    have "(f ^^ Suc n) ((inv f ^^ Suc n) x) = (f^^n) (f (inv f ((inv f^^n) x)))"
    4.73 -      by (simp add: funpow_swap1)
    4.74 -    also have "... = (f^^n) ((inv f^^n) x)"
    4.75 -      using * by auto
    4.76 -    also have "... = x" using Suc.IH by auto
    4.77 -    finally show ?case by simp
    4.78 -  qed (auto)
    4.79 -  then show ?thesis unfolding o_def by blast
    4.80 -qed
    4.81 -
    4.82 -lemma inv_fn:
    4.83 -  fixes f::"'a \<Rightarrow> 'a"
    4.84 -  assumes "bij f"
    4.85 -  shows "inv (f^^n) = ((inv f)^^n)"
    4.86 -proof -
    4.87 -  have "inv (f^^n) x = ((inv f)^^n) x" for x
    4.88 -  apply (rule inv_into_f_eq, auto simp add: inj_fn[OF bij_is_inj[OF assms]])
    4.89 -  using fn_o_inv_fn_is_id[OF assms, of n] by (metis comp_apply)
    4.90 -  then show ?thesis by auto
    4.91 -qed
    4.92 -
    4.93 -
    4.94 -lemma mono_inv:
    4.95 -  fixes f::"'a::linorder \<Rightarrow> 'b::linorder"
    4.96 -  assumes "mono f" "bij f"
    4.97 -  shows "mono (inv f)"
    4.98 -proof
    4.99 -  fix x y::'b assume "x \<le> y"
   4.100 -  then show "inv f x \<le> inv f y"
   4.101 -    by (metis (no_types, lifting) assms bij_is_surj eq_iff le_cases mono_def surj_f_inv_f)
   4.102 -qed
   4.103 -
   4.104 -lemma mono_bij_Inf:
   4.105 -  fixes f :: "'a::complete_linorder \<Rightarrow> 'b::complete_linorder"
   4.106 -  assumes "mono f" "bij f"
   4.107 -  shows "f (Inf A) = Inf (f`A)"
   4.108 -proof -
   4.109 -  have "(inv f) (Inf (f`A)) \<le> Inf ((inv f)`(f`A))"
   4.110 -    using mono_Inf[OF mono_inv[OF assms], of "f`A"] by simp
   4.111 -  then have "Inf (f`A) \<le> f (Inf ((inv f)`(f`A)))"
   4.112 -    by (metis (no_types, lifting) assms mono_def bij_inv_eq_iff)
   4.113 -  also have "... = f(Inf A)"
   4.114 -    using assms by (simp add: bij_is_inj)
   4.115 -  finally show ?thesis using mono_Inf[OF assms(1), of A] by auto
   4.116 -qed
   4.117 -
   4.118 -
   4.119 -lemma Inf_nat_def1:
   4.120 -  fixes K::"nat set"
   4.121 -  assumes "K \<noteq> {}"
   4.122 -  shows "Inf K \<in> K"
   4.123 -by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI)
   4.124 -
   4.125 -subsection \<open>Liminf-Limsup.thy\<close>
   4.126 -
   4.127 -lemma limsup_shift:
   4.128 -  "limsup (\<lambda>n. u (n+1)) = limsup u"
   4.129 -proof -
   4.130 -  have "(SUP m:{n+1..}. u m) = (SUP m:{n..}. u (m + 1))" for n
   4.131 -    apply (rule SUP_eq) using Suc_le_D by auto
   4.132 -  then have a: "(INF n. SUP m:{n..}. u (m + 1)) = (INF n. (SUP m:{n+1..}. u m))" by auto
   4.133 -  have b: "(INF n. (SUP m:{n+1..}. u m)) = (INF n:{1..}. (SUP m:{n..}. u m))"
   4.134 -    apply (rule INF_eq) using Suc_le_D by auto
   4.135 -  have "(INF n:{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
   4.136 -    apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
   4.137 -  moreover have "decseq (\<lambda>n. (SUP m:{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
   4.138 -  ultimately have c: "(INF n:{1..}. (SUP m:{n..}. u m)) = (INF n. (SUP m:{n..}. u m))" by simp
   4.139 -  have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m:{n..}. u (m + 1))" using a b c by simp
   4.140 -  then show ?thesis by (auto cong: limsup_INF_SUP)
   4.141 -qed
   4.142 -
   4.143 -lemma limsup_shift_k:
   4.144 -  "limsup (\<lambda>n. u (n+k)) = limsup u"
   4.145 -proof (induction k)
   4.146 -  case (Suc k)
   4.147 -  have "limsup (\<lambda>n. u (n+k+1)) = limsup (\<lambda>n. u (n+k))" using limsup_shift[where ?u="\<lambda>n. u(n+k)"] by simp
   4.148 -  then show ?case using Suc.IH by simp
   4.149 -qed (auto)
   4.150 -
   4.151 -lemma liminf_shift:
   4.152 -  "liminf (\<lambda>n. u (n+1)) = liminf u"
   4.153 -proof -
   4.154 -  have "(INF m:{n+1..}. u m) = (INF m:{n..}. u (m + 1))" for n
   4.155 -    apply (rule INF_eq) using Suc_le_D by (auto)
   4.156 -  then have a: "(SUP n. INF m:{n..}. u (m + 1)) = (SUP n. (INF m:{n+1..}. u m))" by auto
   4.157 -  have b: "(SUP n. (INF m:{n+1..}. u m)) = (SUP n:{1..}. (INF m:{n..}. u m))"
   4.158 -    apply (rule SUP_eq) using Suc_le_D by (auto)
   4.159 -  have "(SUP n:{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
   4.160 -    apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
   4.161 -  moreover have "incseq (\<lambda>n. (INF m:{n..}. u m))" by (simp add: INF_superset_mono mono_def)
   4.162 -  ultimately have c: "(SUP n:{1..}. (INF m:{n..}. u m)) = (SUP n. (INF m:{n..}. u m))" by simp
   4.163 -  have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m:{n..}. u (m + 1))" using a b c by simp
   4.164 -  then show ?thesis by (auto cong: liminf_SUP_INF)
   4.165 -qed
   4.166 -
   4.167 -lemma liminf_shift_k:
   4.168 -  "liminf (\<lambda>n. u (n+k)) = liminf u"
   4.169 -proof (induction k)
   4.170 -  case (Suc k)
   4.171 -  have "liminf (\<lambda>n. u (n+k+1)) = liminf (\<lambda>n. u (n+k))" using liminf_shift[where ?u="\<lambda>n. u(n+k)"] by simp
   4.172 -  then show ?case using Suc.IH by simp
   4.173 -qed (auto)
   4.174 -
   4.175 -lemma Limsup_obtain:
   4.176 -  fixes u::"_ \<Rightarrow> 'a :: complete_linorder"
   4.177 -  assumes "Limsup F u > c"
   4.178 -  shows "\<exists>i. u i > c"
   4.179 -proof -
   4.180 -  have "(INF P:{P. eventually P F}. SUP x:{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
   4.181 -  then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff)
   4.182 -qed
   4.183 -
   4.184 -text \<open>The next lemma is extremely useful, as it often makes it possible to reduce statements
   4.185 -about limsups to statements about limits.\<close>
   4.186 -
   4.187 -lemma limsup_subseq_lim:
   4.188 -  fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   4.189 -  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> limsup u"
   4.190 -proof (cases)
   4.191 -  assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<le> u p"
   4.192 -  then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<le> u (r n)) \<and> r n < r (Suc n)"
   4.193 -    by (intro dependent_nat_choice) (auto simp: conj_commute)
   4.194 -  then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<le> u (r n)"
   4.195 -    by (auto simp: strict_mono_Suc_iff)
   4.196 -  define umax where "umax = (\<lambda>n. (SUP m:{n..}. u m))"
   4.197 -  have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
   4.198 -  then have "umax \<longlonglongrightarrow> limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
   4.199 -  then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
   4.200 -  have "\<And>n. umax(r n) = u(r n)" unfolding umax_def using mono
   4.201 -    by (metis SUP_le_iff antisym atLeast_def mem_Collect_eq order_refl)
   4.202 -  then have "umax o r = u o r" unfolding o_def by simp
   4.203 -  then have "(u o r) \<longlonglongrightarrow> limsup u" using * by simp
   4.204 -  then show ?thesis using \<open>strict_mono r\<close> by blast
   4.205 -next
   4.206 -  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<le> u p))"
   4.207 -  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p < u m" by (force simp: not_le le_less)
   4.208 -  have "\<exists>r. \<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<le> u (r (Suc n)))"
   4.209 -  proof (rule dependent_nat_choice)
   4.210 -    fix x assume "N < x"
   4.211 -    then have a: "finite {N<..x}" "{N<..x} \<noteq> {}" by simp_all
   4.212 -    have "Max {u i |i. i \<in> {N<..x}} \<in> {u i |i. i \<in> {N<..x}}" apply (rule Max_in) using a by (auto)
   4.213 -    then obtain p where "p \<in> {N<..x}" and upmax: "u p = Max{u i |i. i \<in> {N<..x}}" by auto
   4.214 -    define U where "U = {m. m > p \<and> u p < u m}"
   4.215 -    have "U \<noteq> {}" unfolding U_def using N[of p] \<open>p \<in> {N<..x}\<close> by auto
   4.216 -    define y where "y = Inf U"
   4.217 -    then have "y \<in> U" using \<open>U \<noteq> {}\<close> by (simp add: Inf_nat_def1)
   4.218 -    have a: "\<And>i. i \<in> {N<..x} \<Longrightarrow> u i \<le> u p"
   4.219 -    proof -
   4.220 -      fix i assume "i \<in> {N<..x}"
   4.221 -      then have "u i \<in> {u i |i. i \<in> {N<..x}}" by blast
   4.222 -      then show "u i \<le> u p" using upmax by simp
   4.223 -    qed
   4.224 -    moreover have "u p < u y" using \<open>y \<in> U\<close> U_def by auto
   4.225 -    ultimately have "y \<notin> {N<..x}" using not_le by blast
   4.226 -    moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
   4.227 -    ultimately have "y > x" by auto
   4.228 -
   4.229 -    have "\<And>i. i \<in> {N<..y} \<Longrightarrow> u i \<le> u y"
   4.230 -    proof -
   4.231 -      fix i assume "i \<in> {N<..y}" show "u i \<le> u y"
   4.232 -      proof (cases)
   4.233 -        assume "i = y"
   4.234 -        then show ?thesis by simp
   4.235 -      next
   4.236 -        assume "\<not>(i=y)"
   4.237 -        then have i:"i \<in> {N<..<y}" using \<open>i \<in> {N<..y}\<close> by simp
   4.238 -        have "u i \<le> u p"
   4.239 -        proof (cases)
   4.240 -          assume "i \<le> x"
   4.241 -          then have "i \<in> {N<..x}" using i by simp
   4.242 -          then show ?thesis using a by simp
   4.243 -        next
   4.244 -          assume "\<not>(i \<le> x)"
   4.245 -          then have "i > x" by simp
   4.246 -          then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
   4.247 -          have "i < Inf U" using i y_def by simp
   4.248 -          then have "i \<notin> U" using Inf_nat_def not_less_Least by auto
   4.249 -          then show ?thesis using U_def * by auto
   4.250 -        qed
   4.251 -        then show "u i \<le> u y" using \<open>u p < u y\<close> by auto
   4.252 -      qed
   4.253 -    qed
   4.254 -    then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
   4.255 -    then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" by auto
   4.256 -  qed (auto)
   4.257 -  then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<le> u (r (Suc n)))" by auto
   4.258 -  have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
   4.259 -  have "incseq (u o r)" unfolding o_def using r by (simp add: incseq_SucI order.strict_implies_order)
   4.260 -  then have "(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)" using LIMSEQ_SUP by blast
   4.261 -  then have "limsup (u o r) = (SUP n. (u o r) n)" by (simp add: lim_imp_Limsup)
   4.262 -  moreover have "limsup (u o r) \<le> limsup u" using \<open>strict_mono r\<close> by (simp add: limsup_subseq_mono)
   4.263 -  ultimately have "(SUP n. (u o r) n) \<le> limsup u" by simp
   4.264 -
   4.265 -  {
   4.266 -    fix i assume i: "i \<in> {N<..}"
   4.267 -    obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
   4.268 -    then have "i \<in> {N<..r(Suc n)}" using i by simp
   4.269 -    then have "u i \<le> u (r(Suc n))" using r by simp
   4.270 -    then have "u i \<le> (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
   4.271 -  }
   4.272 -  then have "(SUP i:{N<..}. u i) \<le> (SUP n. (u o r) n)" using SUP_least by blast
   4.273 -  then have "limsup u \<le> (SUP n. (u o r) n)" unfolding Limsup_def
   4.274 -    by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
   4.275 -  then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
   4.276 -  then have "(u o r) \<longlonglongrightarrow> limsup u" using \<open>(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)\<close> by simp
   4.277 -  then show ?thesis using \<open>strict_mono r\<close> by auto
   4.278 -qed
   4.279 -
   4.280 -lemma liminf_subseq_lim:
   4.281 -  fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   4.282 -  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> liminf u"
   4.283 -proof (cases)
   4.284 -  assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<ge> u p"
   4.285 -  then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<ge> u (r n)) \<and> r n < r (Suc n)"
   4.286 -    by (intro dependent_nat_choice) (auto simp: conj_commute)
   4.287 -  then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<ge> u (r n)"
   4.288 -    by (auto simp: strict_mono_Suc_iff)
   4.289 -  define umin where "umin = (\<lambda>n. (INF m:{n..}. u m))"
   4.290 -  have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
   4.291 -  then have "umin \<longlonglongrightarrow> liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
   4.292 -  then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
   4.293 -  have "\<And>n. umin(r n) = u(r n)" unfolding umin_def using mono
   4.294 -    by (metis le_INF_iff antisym atLeast_def mem_Collect_eq order_refl)
   4.295 -  then have "umin o r = u o r" unfolding o_def by simp
   4.296 -  then have "(u o r) \<longlonglongrightarrow> liminf u" using * by simp
   4.297 -  then show ?thesis using \<open>strict_mono r\<close> by blast
   4.298 -next
   4.299 -  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<ge> u p))"
   4.300 -  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p > u m" by (force simp: not_le le_less)
   4.301 -  have "\<exists>r. \<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))"
   4.302 -  proof (rule dependent_nat_choice)
   4.303 -    fix x assume "N < x"
   4.304 -    then have a: "finite {N<..x}" "{N<..x} \<noteq> {}" by simp_all
   4.305 -    have "Min {u i |i. i \<in> {N<..x}} \<in> {u i |i. i \<in> {N<..x}}" apply (rule Min_in) using a by (auto)
   4.306 -    then obtain p where "p \<in> {N<..x}" and upmin: "u p = Min{u i |i. i \<in> {N<..x}}" by auto
   4.307 -    define U where "U = {m. m > p \<and> u p > u m}"
   4.308 -    have "U \<noteq> {}" unfolding U_def using N[of p] \<open>p \<in> {N<..x}\<close> by auto
   4.309 -    define y where "y = Inf U"
   4.310 -    then have "y \<in> U" using \<open>U \<noteq> {}\<close> by (simp add: Inf_nat_def1)
   4.311 -    have a: "\<And>i. i \<in> {N<..x} \<Longrightarrow> u i \<ge> u p"
   4.312 -    proof -
   4.313 -      fix i assume "i \<in> {N<..x}"
   4.314 -      then have "u i \<in> {u i |i. i \<in> {N<..x}}" by blast
   4.315 -      then show "u i \<ge> u p" using upmin by simp
   4.316 -    qed
   4.317 -    moreover have "u p > u y" using \<open>y \<in> U\<close> U_def by auto
   4.318 -    ultimately have "y \<notin> {N<..x}" using not_le by blast
   4.319 -    moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
   4.320 -    ultimately have "y > x" by auto
   4.321 -
   4.322 -    have "\<And>i. i \<in> {N<..y} \<Longrightarrow> u i \<ge> u y"
   4.323 -    proof -
   4.324 -      fix i assume "i \<in> {N<..y}" show "u i \<ge> u y"
   4.325 -      proof (cases)
   4.326 -        assume "i = y"
   4.327 -        then show ?thesis by simp
   4.328 -      next
   4.329 -        assume "\<not>(i=y)"
   4.330 -        then have i:"i \<in> {N<..<y}" using \<open>i \<in> {N<..y}\<close> by simp
   4.331 -        have "u i \<ge> u p"
   4.332 -        proof (cases)
   4.333 -          assume "i \<le> x"
   4.334 -          then have "i \<in> {N<..x}" using i by simp
   4.335 -          then show ?thesis using a by simp
   4.336 -        next
   4.337 -          assume "\<not>(i \<le> x)"
   4.338 -          then have "i > x" by simp
   4.339 -          then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
   4.340 -          have "i < Inf U" using i y_def by simp
   4.341 -          then have "i \<notin> U" using Inf_nat_def not_less_Least by auto
   4.342 -          then show ?thesis using U_def * by auto
   4.343 -        qed
   4.344 -        then show "u i \<ge> u y" using \<open>u p > u y\<close> by auto
   4.345 -      qed
   4.346 -    qed
   4.347 -    then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
   4.348 -    then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" by auto
   4.349 -  qed (auto)
   4.350 -  then obtain r :: "nat \<Rightarrow> nat" 
   4.351 -    where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))" by auto
   4.352 -  have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
   4.353 -  have "decseq (u o r)" unfolding o_def using r by (simp add: decseq_SucI order.strict_implies_order)
   4.354 -  then have "(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)" using LIMSEQ_INF by blast
   4.355 -  then have "liminf (u o r) = (INF n. (u o r) n)" by (simp add: lim_imp_Liminf)
   4.356 -  moreover have "liminf (u o r) \<ge> liminf u" using \<open>strict_mono r\<close> by (simp add: liminf_subseq_mono)
   4.357 -  ultimately have "(INF n. (u o r) n) \<ge> liminf u" by simp
   4.358 -
   4.359 -  {
   4.360 -    fix i assume i: "i \<in> {N<..}"
   4.361 -    obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
   4.362 -    then have "i \<in> {N<..r(Suc n)}" using i by simp
   4.363 -    then have "u i \<ge> u (r(Suc n))" using r by simp
   4.364 -    then have "u i \<ge> (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
   4.365 -  }
   4.366 -  then have "(INF i:{N<..}. u i) \<ge> (INF n. (u o r) n)" using INF_greatest by blast
   4.367 -  then have "liminf u \<ge> (INF n. (u o r) n)" unfolding Liminf_def
   4.368 -    by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
   4.369 -  then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
   4.370 -  then have "(u o r) \<longlonglongrightarrow> liminf u" using \<open>(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)\<close> by simp
   4.371 -  then show ?thesis using \<open>strict_mono r\<close> by auto
   4.372 -qed
   4.373 -
   4.374 -
   4.375 -subsection \<open>Extended-Real.thy\<close>
   4.376 -
   4.377 -text\<open>The proof of this one is copied from \verb+ereal_add_mono+.\<close>
   4.378 -lemma ereal_add_strict_mono2:
   4.379 -  fixes a b c d :: ereal
   4.380 -  assumes "a < b"
   4.381 -    and "c < d"
   4.382 -  shows "a + c < b + d"
   4.383 -using assms
   4.384 -apply (cases a)
   4.385 -apply (cases rule: ereal3_cases[of b c d], auto)
   4.386 -apply (cases rule: ereal3_cases[of b c d], auto)
   4.387 -done
   4.388 -
   4.389 -text \<open>The next ones are analogues of \verb+mult_mono+ and \verb+mult_mono'+ in ereal.\<close>
   4.390 -
   4.391 -lemma ereal_mult_mono:
   4.392 -  fixes a b c d::ereal
   4.393 -  assumes "b \<ge> 0" "c \<ge> 0" "a \<le> b" "c \<le> d"
   4.394 -  shows "a * c \<le> b * d"
   4.395 -by (metis ereal_mult_right_mono mult.commute order_trans assms)
   4.396 -
   4.397 -lemma ereal_mult_mono':
   4.398 -  fixes a b c d::ereal
   4.399 -  assumes "a \<ge> 0" "c \<ge> 0" "a \<le> b" "c \<le> d"
   4.400 -  shows "a * c \<le> b * d"
   4.401 -by (metis ereal_mult_right_mono mult.commute order_trans assms)
   4.402 -
   4.403 -lemma ereal_mult_mono_strict:
   4.404 -  fixes a b c d::ereal
   4.405 -  assumes "b > 0" "c > 0" "a < b" "c < d"
   4.406 -  shows "a * c < b * d"
   4.407 -proof -
   4.408 -  have "c < \<infinity>" using \<open>c < d\<close> by auto
   4.409 -  then have "a * c < b * c" by (metis ereal_mult_strict_left_mono[OF assms(3) assms(2)] mult.commute)
   4.410 -  moreover have "b * c \<le> b * d" using assms(2) assms(4) by (simp add: assms(1) ereal_mult_left_mono less_imp_le)
   4.411 -  ultimately show ?thesis by simp
   4.412 -qed
   4.413 -
   4.414 -lemma ereal_mult_mono_strict':
   4.415 -  fixes a b c d::ereal
   4.416 -  assumes "a > 0" "c > 0" "a < b" "c < d"
   4.417 -  shows "a * c < b * d"
   4.418 -apply (rule ereal_mult_mono_strict, auto simp add: assms) using assms by auto
   4.419 -
   4.420 -lemma ereal_abs_add:
   4.421 -  fixes a b::ereal
   4.422 -  shows "abs(a+b) \<le> abs a + abs b"
   4.423 -by (cases rule: ereal2_cases[of a b]) (auto)
   4.424 -
   4.425 -lemma ereal_abs_diff:
   4.426 -  fixes a b::ereal
   4.427 -  shows "abs(a-b) \<le> abs a + abs b"
   4.428 -by (cases rule: ereal2_cases[of a b]) (auto)
   4.429 -
   4.430 -lemma sum_constant_ereal:
   4.431 -  fixes a::ereal
   4.432 -  shows "(\<Sum>i\<in>I. a) = a * card I"
   4.433 -apply (cases "finite I", induct set: finite, simp_all)
   4.434 -apply (cases a, auto, metis (no_types, hide_lams) add.commute mult.commute semiring_normalization_rules(3))
   4.435 -done
   4.436 -
   4.437 -lemma real_lim_then_eventually_real:
   4.438 -  assumes "(u \<longlongrightarrow> ereal l) F"
   4.439 -  shows "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) F"
   4.440 -proof -
   4.441 -  have "ereal l \<in> {-\<infinity><..<(\<infinity>::ereal)}" by simp
   4.442 -  moreover have "open {-\<infinity><..<(\<infinity>::ereal)}" by simp
   4.443 -  ultimately have "eventually (\<lambda>n. u n \<in> {-\<infinity><..<(\<infinity>::ereal)}) F" using assms tendsto_def by blast
   4.444 -  moreover have "\<And>x. x \<in> {-\<infinity><..<(\<infinity>::ereal)} \<Longrightarrow> x = ereal(real_of_ereal x)" using ereal_real by auto
   4.445 -  ultimately show ?thesis by (metis (mono_tags, lifting) eventually_mono)
   4.446 -qed
   4.447 -
   4.448 -lemma ereal_Inf_cmult:
   4.449 -  assumes "c>(0::real)"
   4.450 -  shows "Inf {ereal c * x |x. P x} = ereal c * Inf {x. P x}"
   4.451 -proof -
   4.452 -  have "(\<lambda>x::ereal. c * x) (Inf {x::ereal. P x}) = Inf ((\<lambda>x::ereal. c * x)`{x::ereal. P x})"
   4.453 -    apply (rule mono_bij_Inf)
   4.454 -    apply (simp add: assms ereal_mult_left_mono less_imp_le mono_def)
   4.455 -    apply (rule bij_betw_byWitness[of _ "\<lambda>x. (x::ereal) / c"], auto simp add: assms ereal_mult_divide)
   4.456 -    using assms ereal_divide_eq apply auto
   4.457 -    done
   4.458 -  then show ?thesis by (simp only: setcompr_eq_image[symmetric])
   4.459 -qed
   4.460 -
   4.461 -
   4.462 -subsubsection \<open>Continuity of addition\<close>
   4.463 -
   4.464 -text \<open>The next few lemmas remove an unnecessary assumption in \verb+tendsto_add_ereal+, culminating
   4.465 -in \verb+tendsto_add_ereal_general+ which essentially says that the addition
   4.466 -is continuous on ereal times ereal, except at $(-\infty, \infty)$ and $(\infty, -\infty)$.
   4.467 -It is much more convenient in many situations, see for instance the proof of
   4.468 -\verb+tendsto_sum_ereal+ below.\<close>
   4.469 -
   4.470 -lemma tendsto_add_ereal_PInf:
   4.471 -  fixes y :: ereal
   4.472 -  assumes y: "y \<noteq> -\<infinity>"
   4.473 -  assumes f: "(f \<longlongrightarrow> \<infinity>) F" and g: "(g \<longlongrightarrow> y) F"
   4.474 -  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> \<infinity>) F"
   4.475 -proof -
   4.476 -  have "\<exists>C. eventually (\<lambda>x. g x > ereal C) F"
   4.477 -  proof (cases y)
   4.478 -    case (real r)
   4.479 -    have "y > y-1" using y real by (simp add: ereal_between(1))
   4.480 -    then have "eventually (\<lambda>x. g x > y - 1) F" using g y order_tendsto_iff by auto
   4.481 -    moreover have "y-1 = ereal(real_of_ereal(y-1))"
   4.482 -      by (metis real ereal_eq_1(1) ereal_minus(1) real_of_ereal.simps(1))
   4.483 -    ultimately have "eventually (\<lambda>x. g x > ereal(real_of_ereal(y - 1))) F" by simp
   4.484 -    then show ?thesis by auto
   4.485 -  next
   4.486 -    case (PInf)
   4.487 -    have "eventually (\<lambda>x. g x > ereal 0) F" using g PInf by (simp add: tendsto_PInfty)
   4.488 -    then show ?thesis by auto
   4.489 -  qed (simp add: y)
   4.490 -  then obtain C::real where ge: "eventually (\<lambda>x. g x > ereal C) F" by auto
   4.491 -
   4.492 -  {
   4.493 -    fix M::real
   4.494 -    have "eventually (\<lambda>x. f x > ereal(M - C)) F" using f by (simp add: tendsto_PInfty)
   4.495 -    then have "eventually (\<lambda>x. (f x > ereal (M-C)) \<and> (g x > ereal C)) F"
   4.496 -      by (auto simp add: ge eventually_conj_iff)
   4.497 -    moreover have "\<And>x. ((f x > ereal (M-C)) \<and> (g x > ereal C)) \<Longrightarrow> (f x + g x > ereal M)"
   4.498 -      using ereal_add_strict_mono2 by fastforce
   4.499 -    ultimately have "eventually (\<lambda>x. f x + g x > ereal M) F" using eventually_mono by force
   4.500 -  }
   4.501 -  then show ?thesis by (simp add: tendsto_PInfty)
   4.502 -qed
   4.503 -
   4.504 -text\<open>One would like to deduce the next lemma from the previous one, but the fact
   4.505 -that $-(x+y)$ is in general different from $(-x) + (-y)$ in ereal creates difficulties,
   4.506 -so it is more efficient to copy the previous proof.\<close>
   4.507 -
   4.508 -lemma tendsto_add_ereal_MInf:
   4.509 -  fixes y :: ereal
   4.510 -  assumes y: "y \<noteq> \<infinity>"
   4.511 -  assumes f: "(f \<longlongrightarrow> -\<infinity>) F" and g: "(g \<longlongrightarrow> y) F"
   4.512 -  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> -\<infinity>) F"
   4.513 -proof -
   4.514 -  have "\<exists>C. eventually (\<lambda>x. g x < ereal C) F"
   4.515 -  proof (cases y)
   4.516 -    case (real r)
   4.517 -    have "y < y+1" using y real by (simp add: ereal_between(1))
   4.518 -    then have "eventually (\<lambda>x. g x < y + 1) F" using g y order_tendsto_iff by force
   4.519 -    moreover have "y+1 = ereal(real_of_ereal (y+1))" by (simp add: real)
   4.520 -    ultimately have "eventually (\<lambda>x. g x < ereal(real_of_ereal(y + 1))) F" by simp
   4.521 -    then show ?thesis by auto
   4.522 -  next
   4.523 -    case (MInf)
   4.524 -    have "eventually (\<lambda>x. g x < ereal 0) F" using g MInf by (simp add: tendsto_MInfty)
   4.525 -    then show ?thesis by auto
   4.526 -  qed (simp add: y)
   4.527 -  then obtain C::real where ge: "eventually (\<lambda>x. g x < ereal C) F" by auto
   4.528 -
   4.529 -  {
   4.530 -    fix M::real
   4.531 -    have "eventually (\<lambda>x. f x < ereal(M - C)) F" using f by (simp add: tendsto_MInfty)
   4.532 -    then have "eventually (\<lambda>x. (f x < ereal (M- C)) \<and> (g x < ereal C)) F"
   4.533 -      by (auto simp add: ge eventually_conj_iff)
   4.534 -    moreover have "\<And>x. ((f x < ereal (M-C)) \<and> (g x < ereal C)) \<Longrightarrow> (f x + g x < ereal M)"
   4.535 -      using ereal_add_strict_mono2 by fastforce
   4.536 -    ultimately have "eventually (\<lambda>x. f x + g x < ereal M) F" using eventually_mono by force
   4.537 -  }
   4.538 -  then show ?thesis by (simp add: tendsto_MInfty)
   4.539 -qed
   4.540 -
   4.541 -lemma tendsto_add_ereal_general1:
   4.542 -  fixes x y :: ereal
   4.543 -  assumes y: "\<bar>y\<bar> \<noteq> \<infinity>"
   4.544 -  assumes f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   4.545 -  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   4.546 -proof (cases x)
   4.547 -  case (real r)
   4.548 -  have a: "\<bar>x\<bar> \<noteq> \<infinity>" by (simp add: real)
   4.549 -  show ?thesis by (rule tendsto_add_ereal[OF a, OF y, OF f, OF g])
   4.550 -next
   4.551 -  case PInf
   4.552 -  then show ?thesis using tendsto_add_ereal_PInf assms by force
   4.553 -next
   4.554 -  case MInf
   4.555 -  then show ?thesis using tendsto_add_ereal_MInf assms
   4.556 -    by (metis abs_ereal.simps(3) ereal_MInfty_eq_plus)
   4.557 -qed
   4.558 -
   4.559 -lemma tendsto_add_ereal_general2:
   4.560 -  fixes x y :: ereal
   4.561 -  assumes x: "\<bar>x\<bar> \<noteq> \<infinity>"
   4.562 -      and f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   4.563 -  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   4.564 -proof -
   4.565 -  have "((\<lambda>x. g x + f x) \<longlongrightarrow> x + y) F"
   4.566 -    using tendsto_add_ereal_general1[OF x, OF g, OF f] add.commute[of "y", of "x"] by simp
   4.567 -  moreover have "\<And>x. g x + f x = f x + g x" using add.commute by auto
   4.568 -  ultimately show ?thesis by simp
   4.569 -qed
   4.570 -
   4.571 -text \<open>The next lemma says that the addition is continuous on ereal, except at
   4.572 -the pairs $(-\infty, \infty)$ and $(\infty, -\infty)$.\<close>
   4.573 -
   4.574 -lemma tendsto_add_ereal_general [tendsto_intros]:
   4.575 -  fixes x y :: ereal
   4.576 -  assumes "\<not>((x=\<infinity> \<and> y=-\<infinity>) \<or> (x=-\<infinity> \<and> y=\<infinity>))"
   4.577 -      and f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   4.578 -  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   4.579 -proof (cases x)
   4.580 -  case (real r)
   4.581 -  show ?thesis
   4.582 -    apply (rule tendsto_add_ereal_general2) using real assms by auto
   4.583 -next
   4.584 -  case (PInf)
   4.585 -  then have "y \<noteq> -\<infinity>" using assms by simp
   4.586 -  then show ?thesis using tendsto_add_ereal_PInf PInf assms by auto
   4.587 -next
   4.588 -  case (MInf)
   4.589 -  then have "y \<noteq> \<infinity>" using assms by simp
   4.590 -  then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
   4.591 -qed
   4.592 -
   4.593 -subsubsection \<open>Continuity of multiplication\<close>
   4.594 -
   4.595 -text \<open>In the same way as for addition, we prove that the multiplication is continuous on
   4.596 -ereal times ereal, except at $(\infty, 0)$ and $(-\infty, 0)$ and $(0, \infty)$ and $(0, -\infty)$,
   4.597 -starting with specific situations.\<close>
   4.598 -
   4.599 -lemma tendsto_mult_real_ereal:
   4.600 -  assumes "(u \<longlongrightarrow> ereal l) F" "(v \<longlongrightarrow> ereal m) F"
   4.601 -  shows "((\<lambda>n. u n * v n) \<longlongrightarrow> ereal l * ereal m) F"
   4.602 -proof -
   4.603 -  have ureal: "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) F" by (rule real_lim_then_eventually_real[OF assms(1)])
   4.604 -  then have "((\<lambda>n. ereal(real_of_ereal(u n))) \<longlongrightarrow> ereal l) F" using assms by auto
   4.605 -  then have limu: "((\<lambda>n. real_of_ereal(u n)) \<longlongrightarrow> l) F" by auto
   4.606 -  have vreal: "eventually (\<lambda>n. v n = ereal(real_of_ereal(v n))) F" by (rule real_lim_then_eventually_real[OF assms(2)])
   4.607 -  then have "((\<lambda>n. ereal(real_of_ereal(v n))) \<longlongrightarrow> ereal m) F" using assms by auto
   4.608 -  then have limv: "((\<lambda>n. real_of_ereal(v n)) \<longlongrightarrow> m) F" by auto
   4.609 -
   4.610 -  {
   4.611 -    fix n assume "u n = ereal(real_of_ereal(u n))" "v n = ereal(real_of_ereal(v n))"
   4.612 -    then have "ereal(real_of_ereal(u n) * real_of_ereal(v n)) = u n * v n" by (metis times_ereal.simps(1))
   4.613 -  }
   4.614 -  then have *: "eventually (\<lambda>n. ereal(real_of_ereal(u n) * real_of_ereal(v n)) = u n * v n) F"
   4.615 -    using eventually_elim2[OF ureal vreal] by auto
   4.616 -
   4.617 -  have "((\<lambda>n. real_of_ereal(u n) * real_of_ereal(v n)) \<longlongrightarrow> l * m) F" using tendsto_mult[OF limu limv] by auto
   4.618 -  then have "((\<lambda>n. ereal(real_of_ereal(u n)) * real_of_ereal(v n)) \<longlongrightarrow> ereal(l * m)) F" by auto
   4.619 -  then show ?thesis using * filterlim_cong by fastforce
   4.620 -qed
   4.621 -
   4.622 -lemma tendsto_mult_ereal_PInf:
   4.623 -  fixes f g::"_ \<Rightarrow> ereal"
   4.624 -  assumes "(f \<longlongrightarrow> l) F" "l>0" "(g \<longlongrightarrow> \<infinity>) F"
   4.625 -  shows "((\<lambda>x. f x * g x) \<longlongrightarrow> \<infinity>) F"
   4.626 -proof -
   4.627 -  obtain a::real where "0 < ereal a" "a < l" using assms(2) using ereal_dense2 by blast
   4.628 -  have *: "eventually (\<lambda>x. f x > a) F" using \<open>a < l\<close> assms(1) by (simp add: order_tendsto_iff)
   4.629 -  {
   4.630 -    fix K::real
   4.631 -    define M where "M = max K 1"
   4.632 -    then have "M > 0" by simp
   4.633 -    then have "ereal(M/a) > 0" using \<open>ereal a > 0\<close> by simp
   4.634 -    then have "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > ereal a * ereal(M/a))"
   4.635 -      using ereal_mult_mono_strict'[where ?c = "M/a", OF \<open>0 < ereal a\<close>] by auto
   4.636 -    moreover have "ereal a * ereal(M/a) = M" using \<open>ereal a > 0\<close> by simp
   4.637 -    ultimately have "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > M)" by simp
   4.638 -    moreover have "M \<ge> K" unfolding M_def by simp
   4.639 -    ultimately have Imp: "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > K)"
   4.640 -      using ereal_less_eq(3) le_less_trans by blast
   4.641 -
   4.642 -    have "eventually (\<lambda>x. g x > M/a) F" using assms(3) by (simp add: tendsto_PInfty)
   4.643 -    then have "eventually (\<lambda>x. (f x > a) \<and> (g x > M/a)) F"
   4.644 -      using * by (auto simp add: eventually_conj_iff)
   4.645 -    then have "eventually (\<lambda>x. f x * g x > K) F" using eventually_mono Imp by force
   4.646 -  }
   4.647 -  then show ?thesis by (auto simp add: tendsto_PInfty)
   4.648 -qed
   4.649 -
   4.650 -lemma tendsto_mult_ereal_pos:
   4.651 -  fixes f g::"_ \<Rightarrow> ereal"
   4.652 -  assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "l>0" "m>0"
   4.653 -  shows "((\<lambda>x. f x * g x) \<longlongrightarrow> l * m) F"
   4.654 -proof (cases)
   4.655 -  assume *: "l = \<infinity> \<or> m = \<infinity>"
   4.656 -  then show ?thesis
   4.657 -  proof (cases)
   4.658 -    assume "m = \<infinity>"
   4.659 -    then show ?thesis using tendsto_mult_ereal_PInf assms by auto
   4.660 -  next
   4.661 -    assume "\<not>(m = \<infinity>)"
   4.662 -    then have "l = \<infinity>" using * by simp
   4.663 -    then have "((\<lambda>x. g x * f x) \<longlongrightarrow> l * m) F" using tendsto_mult_ereal_PInf assms by auto
   4.664 -    moreover have "\<And>x. g x * f x = f x * g x" using mult.commute by auto
   4.665 -    ultimately show ?thesis by simp
   4.666 -  qed
   4.667 -next
   4.668 -  assume "\<not>(l = \<infinity> \<or> m = \<infinity>)"
   4.669 -  then have "l < \<infinity>" "m < \<infinity>" by auto
   4.670 -  then obtain lr mr where "l = ereal lr" "m = ereal mr"
   4.671 -    using \<open>l>0\<close> \<open>m>0\<close> by (metis ereal_cases ereal_less(6) not_less_iff_gr_or_eq)
   4.672 -  then show ?thesis using tendsto_mult_real_ereal assms by auto
   4.673 -qed
   4.674 -
   4.675 -text \<open>We reduce the general situation to the positive case by multiplying by suitable signs.
   4.676 -Unfortunately, as ereal is not a ring, all the neat sign lemmas are not available there. We
   4.677 -give the bare minimum we need.\<close>
   4.678 -
   4.679 -lemma ereal_sgn_abs:
   4.680 -  fixes l::ereal
   4.681 -  shows "sgn(l) * l = abs(l)"
   4.682 -apply (cases l) by (auto simp add: sgn_if ereal_less_uminus_reorder)
   4.683 -
   4.684 -lemma sgn_squared_ereal:
   4.685 -  assumes "l \<noteq> (0::ereal)"
   4.686 -  shows "sgn(l) * sgn(l) = 1"
   4.687 -apply (cases l) using assms by (auto simp add: one_ereal_def sgn_if)
   4.688 -
   4.689 -lemma tendsto_mult_ereal [tendsto_intros]:
   4.690 -  fixes f g::"_ \<Rightarrow> ereal"
   4.691 -  assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "\<not>((l=0 \<and> abs(m) = \<infinity>) \<or> (m=0 \<and> abs(l) = \<infinity>))"
   4.692 -  shows "((\<lambda>x. f x * g x) \<longlongrightarrow> l * m) F"
   4.693 -proof (cases)
   4.694 -  assume "l=0 \<or> m=0"
   4.695 -  then have "abs(l) \<noteq> \<infinity>" "abs(m) \<noteq> \<infinity>" using assms(3) by auto
   4.696 -  then obtain lr mr where "l = ereal lr" "m = ereal mr" by auto
   4.697 -  then show ?thesis using tendsto_mult_real_ereal assms by auto
   4.698 -next
   4.699 -  have sgn_finite: "\<And>a::ereal. abs(sgn a) \<noteq> \<infinity>"
   4.700 -    by (metis MInfty_neq_ereal(2) PInfty_neq_ereal(2) abs_eq_infinity_cases ereal_times(1) ereal_times(3) ereal_uminus_eq_reorder sgn_ereal.elims)
   4.701 -  then have sgn_finite2: "\<And>a b::ereal. abs(sgn a * sgn b) \<noteq> \<infinity>"
   4.702 -    by (metis abs_eq_infinity_cases abs_ereal.simps(2) abs_ereal.simps(3) ereal_mult_eq_MInfty ereal_mult_eq_PInfty)
   4.703 -  assume "\<not>(l=0 \<or> m=0)"
   4.704 -  then have "l \<noteq> 0" "m \<noteq> 0" by auto
   4.705 -  then have "abs(l) > 0" "abs(m) > 0"
   4.706 -    by (metis abs_ereal_ge0 abs_ereal_less0 abs_ereal_pos ereal_uminus_uminus ereal_uminus_zero less_le not_less)+
   4.707 -  then have "sgn(l) * l > 0" "sgn(m) * m > 0" using ereal_sgn_abs by auto
   4.708 -  moreover have "((\<lambda>x. sgn(l) * f x) \<longlongrightarrow> (sgn(l) * l)) F"
   4.709 -    by (rule tendsto_cmult_ereal, auto simp add: sgn_finite assms(1))
   4.710 -  moreover have "((\<lambda>x. sgn(m) * g x) \<longlongrightarrow> (sgn(m) * m)) F"
   4.711 -    by (rule tendsto_cmult_ereal, auto simp add: sgn_finite assms(2))
   4.712 -  ultimately have *: "((\<lambda>x. (sgn(l) * f x) * (sgn(m) * g x)) \<longlongrightarrow> (sgn(l) * l) * (sgn(m) * m)) F"
   4.713 -    using tendsto_mult_ereal_pos by force
   4.714 -  have "((\<lambda>x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x))) \<longlongrightarrow> (sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m))) F"
   4.715 -    by (rule tendsto_cmult_ereal, auto simp add: sgn_finite2 *)
   4.716 -  moreover have "\<And>x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x)) = f x * g x"
   4.717 -    by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
   4.718 -  moreover have "(sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m)) = l * m"
   4.719 -    by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
   4.720 -  ultimately show ?thesis by auto
   4.721 -qed
   4.722 -
   4.723 -lemma tendsto_cmult_ereal_general [tendsto_intros]:
   4.724 -  fixes f::"_ \<Rightarrow> ereal" and c::ereal
   4.725 -  assumes "(f \<longlongrightarrow> l) F" "\<not> (l=0 \<and> abs(c) = \<infinity>)"
   4.726 -  shows "((\<lambda>x. c * f x) \<longlongrightarrow> c * l) F"
   4.727 -by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
   4.728 -
   4.729 -
   4.730 -subsubsection \<open>Continuity of division\<close>
   4.731 -
   4.732 -lemma tendsto_inverse_ereal_PInf:
   4.733 -  fixes u::"_ \<Rightarrow> ereal"
   4.734 -  assumes "(u \<longlongrightarrow> \<infinity>) F"
   4.735 -  shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 0) F"
   4.736 -proof -
   4.737 -  {
   4.738 -    fix e::real assume "e>0"
   4.739 -    have "1/e < \<infinity>" by auto
   4.740 -    then have "eventually (\<lambda>n. u n > 1/e) F" using assms(1) by (simp add: tendsto_PInfty)
   4.741 -    moreover
   4.742 -    {
   4.743 -      fix z::ereal assume "z>1/e"
   4.744 -      then have "z>0" using \<open>e>0\<close> using less_le_trans not_le by fastforce
   4.745 -      then have "1/z \<ge> 0" by auto
   4.746 -      moreover have "1/z < e" using \<open>e>0\<close> \<open>z>1/e\<close>
   4.747 -        apply (cases z) apply auto
   4.748 -        by (metis (mono_tags, hide_lams) less_ereal.simps(2) less_ereal.simps(4) divide_less_eq ereal_divide_less_pos ereal_less(4)
   4.749 -            ereal_less_eq(4) less_le_trans mult_eq_0_iff not_le not_one_less_zero times_ereal.simps(1))
   4.750 -      ultimately have "1/z \<ge> 0" "1/z < e" by auto
   4.751 -    }
   4.752 -    ultimately have "eventually (\<lambda>n. 1/u n<e) F" "eventually (\<lambda>n. 1/u n\<ge>0) F" by (auto simp add: eventually_mono)
   4.753 -  } note * = this
   4.754 -  show ?thesis
   4.755 -  proof (subst order_tendsto_iff, auto)
   4.756 -    fix a::ereal assume "a<0"
   4.757 -    then show "eventually (\<lambda>n. 1/u n > a) F" using *(2) eventually_mono less_le_trans linordered_field_no_ub by fastforce
   4.758 -  next
   4.759 -    fix a::ereal assume "a>0"
   4.760 -    then obtain e::real where "e>0" "a>e" using ereal_dense2 ereal_less(2) by blast
   4.761 -    then have "eventually (\<lambda>n. 1/u n < e) F" using *(1) by auto
   4.762 -    then show "eventually (\<lambda>n. 1/u n < a) F" using \<open>a>e\<close> by (metis (mono_tags, lifting) eventually_mono less_trans)
   4.763 -  qed
   4.764 -qed
   4.765 -
   4.766 -text \<open>The next lemma deserves to exist by itself, as it is so common and useful.\<close>
   4.767 -
   4.768 -lemma tendsto_inverse_real [tendsto_intros]:
   4.769 -  fixes u::"_ \<Rightarrow> real"
   4.770 -  shows "(u \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. 1/ u x) \<longlongrightarrow> 1/l) F"
   4.771 -  using tendsto_inverse unfolding inverse_eq_divide .
   4.772 -
   4.773 -lemma tendsto_inverse_ereal [tendsto_intros]:
   4.774 -  fixes u::"_ \<Rightarrow> ereal"
   4.775 -  assumes "(u \<longlongrightarrow> l) F" "l \<noteq> 0"
   4.776 -  shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 1/l) F"
   4.777 -proof (cases l)
   4.778 -  case (real r)
   4.779 -  then have "r \<noteq> 0" using assms(2) by auto
   4.780 -  then have "1/l = ereal(1/r)" using real by (simp add: one_ereal_def)
   4.781 -  define v where "v = (\<lambda>n. real_of_ereal(u n))"
   4.782 -  have ureal: "eventually (\<lambda>n. u n = ereal(v n)) F" unfolding v_def using real_lim_then_eventually_real assms(1) real by auto
   4.783 -  then have "((\<lambda>n. ereal(v n)) \<longlongrightarrow> ereal r) F" using assms real v_def by auto
   4.784 -  then have *: "((\<lambda>n. v n) \<longlongrightarrow> r) F" by auto
   4.785 -  then have "((\<lambda>n. 1/v n) \<longlongrightarrow> 1/r) F" using \<open>r \<noteq> 0\<close> tendsto_inverse_real by auto
   4.786 -  then have lim: "((\<lambda>n. ereal(1/v n)) \<longlongrightarrow> 1/l) F" using \<open>1/l = ereal(1/r)\<close> by auto
   4.787 -
   4.788 -  have "r \<in> -{0}" "open (-{(0::real)})" using \<open>r \<noteq> 0\<close> by auto
   4.789 -  then have "eventually (\<lambda>n. v n \<in> -{0}) F" using * using topological_tendstoD by blast
   4.790 -  then have "eventually (\<lambda>n. v n \<noteq> 0) F" by auto
   4.791 -  moreover
   4.792 -  {
   4.793 -    fix n assume H: "v n \<noteq> 0" "u n = ereal(v n)"
   4.794 -    then have "ereal(1/v n) = 1/ereal(v n)" by (simp add: one_ereal_def)
   4.795 -    then have "ereal(1/v n) = 1/u n" using H(2) by simp
   4.796 -  }
   4.797 -  ultimately have "eventually (\<lambda>n. ereal(1/v n) = 1/u n) F" using ureal eventually_elim2 by force
   4.798 -  with Lim_transform_eventually[OF this lim] show ?thesis by simp
   4.799 -next
   4.800 -  case (PInf)
   4.801 -  then have "1/l = 0" by auto
   4.802 -  then show ?thesis using tendsto_inverse_ereal_PInf assms PInf by auto
   4.803 -next
   4.804 -  case (MInf)
   4.805 -  then have "1/l = 0" by auto
   4.806 -  have "1/z = -1/ -z" if "z < 0" for z::ereal
   4.807 -    apply (cases z) using divide_ereal_def \<open> z < 0 \<close> by auto
   4.808 -  moreover have "eventually (\<lambda>n. u n < 0) F" by (metis (no_types) MInf assms(1) tendsto_MInfty zero_ereal_def)
   4.809 -  ultimately have *: "eventually (\<lambda>n. -1/-u n = 1/u n) F" by (simp add: eventually_mono)
   4.810 -
   4.811 -  define v where "v = (\<lambda>n. - u n)"
   4.812 -  have "(v \<longlongrightarrow> \<infinity>) F" unfolding v_def using MInf assms(1) tendsto_uminus_ereal by fastforce
   4.813 -  then have "((\<lambda>n. 1/v n) \<longlongrightarrow> 0) F" using tendsto_inverse_ereal_PInf by auto
   4.814 -  then have "((\<lambda>n. -1/v n) \<longlongrightarrow> 0) F" using tendsto_uminus_ereal by fastforce
   4.815 -  then show ?thesis unfolding v_def using Lim_transform_eventually[OF *] \<open> 1/l = 0 \<close> by auto
   4.816 -qed
   4.817 -
   4.818 -lemma tendsto_divide_ereal [tendsto_intros]:
   4.819 -  fixes f g::"_ \<Rightarrow> ereal"
   4.820 -  assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "m \<noteq> 0" "\<not>(abs(l) = \<infinity> \<and> abs(m) = \<infinity>)"
   4.821 -  shows "((\<lambda>x. f x / g x) \<longlongrightarrow> l / m) F"
   4.822 -proof -
   4.823 -  define h where "h = (\<lambda>x. 1/ g x)"
   4.824 -  have *: "(h \<longlongrightarrow> 1/m) F" unfolding h_def using assms(2) assms(3) tendsto_inverse_ereal by auto
   4.825 -  have "((\<lambda>x. f x * h x) \<longlongrightarrow> l * (1/m)) F"
   4.826 -    apply (rule tendsto_mult_ereal[OF assms(1) *]) using assms(3) assms(4) by (auto simp add: divide_ereal_def)
   4.827 -  moreover have "f x * h x = f x / g x" for x unfolding h_def by (simp add: divide_ereal_def)
   4.828 -  moreover have "l * (1/m) = l/m" by (simp add: divide_ereal_def)
   4.829 -  ultimately show ?thesis unfolding h_def using Lim_transform_eventually by auto
   4.830 -qed
   4.831 -
   4.832 -
   4.833 -subsubsection \<open>Further limits\<close>
   4.834 -
   4.835 -lemma id_nat_ereal_tendsto_PInf [tendsto_intros]:
   4.836 -  "(\<lambda> n::nat. real n) \<longlonglongrightarrow> \<infinity>"
   4.837 -by (simp add: filterlim_real_sequentially tendsto_PInfty_eq_at_top)
   4.838 -
   4.839 -lemma tendsto_at_top_pseudo_inverse [tendsto_intros]:
   4.840 -  fixes u::"nat \<Rightarrow> nat"
   4.841 -  assumes "LIM n sequentially. u n :> at_top"
   4.842 -  shows "LIM n sequentially. Inf {N. u N \<ge> n} :> at_top"
   4.843 -proof -
   4.844 -  {
   4.845 -    fix C::nat
   4.846 -    define M where "M = Max {u n| n. n \<le> C}+1"
   4.847 -    {
   4.848 -      fix n assume "n \<ge> M"
   4.849 -      have "eventually (\<lambda>N. u N \<ge> n) sequentially" using assms
   4.850 -        by (simp add: filterlim_at_top)
   4.851 -      then have *: "{N. u N \<ge> n} \<noteq> {}" by force
   4.852 -
   4.853 -      have "N > C" if "u N \<ge> n" for N
   4.854 -      proof (rule ccontr)
   4.855 -        assume "\<not>(N > C)"
   4.856 -        have "u N \<le> Max {u n| n. n \<le> C}"
   4.857 -          apply (rule Max_ge) using \<open>\<not>(N > C)\<close> by auto
   4.858 -        then show False using \<open>u N \<ge> n\<close> \<open>n \<ge> M\<close> unfolding M_def by auto
   4.859 -      qed
   4.860 -      then have **: "{N. u N \<ge> n} \<subseteq> {C..}" by fastforce
   4.861 -      have "Inf {N. u N \<ge> n} \<ge> C"
   4.862 -        by (metis "*" "**" Inf_nat_def1 atLeast_iff subset_eq)
   4.863 -    }
   4.864 -    then have "eventually (\<lambda>n. Inf {N. u N \<ge> n} \<ge> C) sequentially"
   4.865 -      using eventually_sequentially by auto
   4.866 -  }
   4.867 -  then show ?thesis using filterlim_at_top by auto
   4.868 -qed
   4.869 -
   4.870 -lemma pseudo_inverse_finite_set:
   4.871 -  fixes u::"nat \<Rightarrow> nat"
   4.872 -  assumes "LIM n sequentially. u n :> at_top"
   4.873 -  shows "finite {N. u N \<le> n}"
   4.874 -proof -
   4.875 -  fix n
   4.876 -  have "eventually (\<lambda>N. u N \<ge> n+1) sequentially" using assms
   4.877 -    by (simp add: filterlim_at_top)
   4.878 -  then obtain N1 where N1: "\<And>N. N \<ge> N1 \<Longrightarrow> u N \<ge> n + 1"
   4.879 -    using eventually_sequentially by auto
   4.880 -  have "{N. u N \<le> n} \<subseteq> {..<N1}"
   4.881 -    apply auto using N1 by (metis Suc_eq_plus1 not_less not_less_eq_eq)
   4.882 -  then show "finite {N. u N \<le> n}" by (simp add: finite_subset)
   4.883 -qed
   4.884 -
   4.885 -lemma tendsto_at_top_pseudo_inverse2 [tendsto_intros]:
   4.886 -  fixes u::"nat \<Rightarrow> nat"
   4.887 -  assumes "LIM n sequentially. u n :> at_top"
   4.888 -  shows "LIM n sequentially. Max {N. u N \<le> n} :> at_top"
   4.889 -proof -
   4.890 -  {
   4.891 -    fix N0::nat
   4.892 -    have "N0 \<le> Max {N. u N \<le> n}" if "n \<ge> u N0" for n
   4.893 -      apply (rule Max.coboundedI) using pseudo_inverse_finite_set[OF assms] that by auto
   4.894 -    then have "eventually (\<lambda>n. N0 \<le> Max {N. u N \<le> n}) sequentially"
   4.895 -      using eventually_sequentially by blast
   4.896 -  }
   4.897 -  then show ?thesis using filterlim_at_top by auto
   4.898 -qed
   4.899 -
   4.900 -lemma ereal_truncation_top [tendsto_intros]:
   4.901 -  fixes x::ereal
   4.902 -  shows "(\<lambda>n::nat. min x n) \<longlonglongrightarrow> x"
   4.903 -proof (cases x)
   4.904 -  case (real r)
   4.905 -  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   4.906 -  then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   4.907 -  then have "eventually (\<lambda>n. min x n = x) sequentially" using eventually_at_top_linorder by blast
   4.908 -  then show ?thesis by (simp add: Lim_eventually)
   4.909 -next
   4.910 -  case (PInf)
   4.911 -  then have "min x n = n" for n::nat by (auto simp add: min_def)
   4.912 -  then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto
   4.913 -next
   4.914 -  case (MInf)
   4.915 -  then have "min x n = x" for n::nat by (auto simp add: min_def)
   4.916 -  then show ?thesis by auto
   4.917 -qed
   4.918 -
   4.919 -lemma ereal_truncation_real_top [tendsto_intros]:
   4.920 -  fixes x::ereal
   4.921 -  assumes "x \<noteq> - \<infinity>"
   4.922 -  shows "(\<lambda>n::nat. real_of_ereal(min x n)) \<longlonglongrightarrow> x"
   4.923 -proof (cases x)
   4.924 -  case (real r)
   4.925 -  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   4.926 -  then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   4.927 -  then have "real_of_ereal(min x n) = r" if "n \<ge> K" for n using real that by auto
   4.928 -  then have "eventually (\<lambda>n. real_of_ereal(min x n) = r) sequentially" using eventually_at_top_linorder by blast
   4.929 -  then have "(\<lambda>n. real_of_ereal(min x n)) \<longlonglongrightarrow> r" by (simp add: Lim_eventually)
   4.930 -  then show ?thesis using real by auto
   4.931 -next
   4.932 -  case (PInf)
   4.933 -  then have "real_of_ereal(min x n) = n" for n::nat by (auto simp add: min_def)
   4.934 -  then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto
   4.935 -qed (simp add: assms)
   4.936 -
   4.937 -lemma ereal_truncation_bottom [tendsto_intros]:
   4.938 -  fixes x::ereal
   4.939 -  shows "(\<lambda>n::nat. max x (- real n)) \<longlonglongrightarrow> x"
   4.940 -proof (cases x)
   4.941 -  case (real r)
   4.942 -  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   4.943 -  then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   4.944 -  then have "eventually (\<lambda>n. max x (-real n) = x) sequentially" using eventually_at_top_linorder by blast
   4.945 -  then show ?thesis by (simp add: Lim_eventually)
   4.946 -next
   4.947 -  case (MInf)
   4.948 -  then have "max x (-real n) = (-1)* ereal(real n)" for n::nat by (auto simp add: max_def)
   4.949 -  moreover have "(\<lambda>n. (-1)* ereal(real n)) \<longlonglongrightarrow> -\<infinity>"
   4.950 -    using tendsto_cmult_ereal[of "-1", OF _ id_nat_ereal_tendsto_PInf] by (simp add: one_ereal_def)
   4.951 -  ultimately show ?thesis using MInf by auto
   4.952 -next
   4.953 -  case (PInf)
   4.954 -  then have "max x (-real n) = x" for n::nat by (auto simp add: max_def)
   4.955 -  then show ?thesis by auto
   4.956 -qed
   4.957 -
   4.958 -lemma ereal_truncation_real_bottom [tendsto_intros]:
   4.959 -  fixes x::ereal
   4.960 -  assumes "x \<noteq> \<infinity>"
   4.961 -  shows "(\<lambda>n::nat. real_of_ereal(max x (- real n))) \<longlonglongrightarrow> x"
   4.962 -proof (cases x)
   4.963 -  case (real r)
   4.964 -  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   4.965 -  then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   4.966 -  then have "real_of_ereal(max x (-real n)) = r" if "n \<ge> K" for n using real that by auto
   4.967 -  then have "eventually (\<lambda>n. real_of_ereal(max x (-real n)) = r) sequentially" using eventually_at_top_linorder by blast
   4.968 -  then have "(\<lambda>n. real_of_ereal(max x (-real n))) \<longlonglongrightarrow> r" by (simp add: Lim_eventually)
   4.969 -  then show ?thesis using real by auto
   4.970 -next
   4.971 -  case (MInf)
   4.972 -  then have "real_of_ereal(max x (-real n)) = (-1)* ereal(real n)" for n::nat by (auto simp add: max_def)
   4.973 -  moreover have "(\<lambda>n. (-1)* ereal(real n)) \<longlonglongrightarrow> -\<infinity>"
   4.974 -    using tendsto_cmult_ereal[of "-1", OF _ id_nat_ereal_tendsto_PInf] by (simp add: one_ereal_def)
   4.975 -  ultimately show ?thesis using MInf by auto
   4.976 -qed (simp add: assms)
   4.977 -
   4.978 -text \<open>the next one is copied from \verb+tendsto_sum+.\<close>
   4.979 -lemma tendsto_sum_ereal [tendsto_intros]:
   4.980 -  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
   4.981 -  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
   4.982 -          "\<And>i. abs(a i) \<noteq> \<infinity>"
   4.983 -  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
   4.984 -proof (cases "finite S")
   4.985 -  assume "finite S" then show ?thesis using assms
   4.986 -    by (induct, simp, simp add: tendsto_add_ereal_general2 assms)
   4.987 -qed(simp)
   4.988 -
   4.989 -subsubsection \<open>Limsups and liminfs\<close>
   4.990 -
   4.991 -lemma limsup_finite_then_bounded:
   4.992 -  fixes u::"nat \<Rightarrow> real"
   4.993 -  assumes "limsup u < \<infinity>"
   4.994 -  shows "\<exists>C. \<forall>n. u n \<le> C"
   4.995 -proof -
   4.996 -  obtain C where C: "limsup u < C" "C < \<infinity>" using assms ereal_dense2 by blast
   4.997 -  then have "C = ereal(real_of_ereal C)" using ereal_real by force
   4.998 -  have "eventually (\<lambda>n. u n < C) sequentially" using C(1) unfolding Limsup_def
   4.999 -    apply (auto simp add: INF_less_iff)
  4.1000 -    using SUP_lessD eventually_mono by fastforce
  4.1001 -  then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> u n < C" using eventually_sequentially by auto
  4.1002 -  define D where "D = max (real_of_ereal C) (Max {u n |n. n \<le> N})"
  4.1003 -  have "\<And>n. u n \<le> D"
  4.1004 -  proof -
  4.1005 -    fix n show "u n \<le> D"
  4.1006 -    proof (cases)
  4.1007 -      assume *: "n \<le> N"
  4.1008 -      have "u n \<le> Max {u n |n. n \<le> N}" by (rule Max_ge, auto simp add: *)
  4.1009 -      then show "u n \<le> D" unfolding D_def by linarith
  4.1010 -    next
  4.1011 -      assume "\<not>(n \<le> N)"
  4.1012 -      then have "n \<ge> N" by simp
  4.1013 -      then have "u n < C" using N by auto
  4.1014 -      then have "u n < real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
  4.1015 -      then show "u n \<le> D" unfolding D_def by linarith
  4.1016 -    qed
  4.1017 -  qed
  4.1018 -  then show ?thesis by blast
  4.1019 -qed
  4.1020 -
  4.1021 -lemma liminf_finite_then_bounded_below:
  4.1022 -  fixes u::"nat \<Rightarrow> real"
  4.1023 -  assumes "liminf u > -\<infinity>"
  4.1024 -  shows "\<exists>C. \<forall>n. u n \<ge> C"
  4.1025 -proof -
  4.1026 -  obtain C where C: "liminf u > C" "C > -\<infinity>" using assms using ereal_dense2 by blast
  4.1027 -  then have "C = ereal(real_of_ereal C)" using ereal_real by force
  4.1028 -  have "eventually (\<lambda>n. u n > C) sequentially" using C(1) unfolding Liminf_def
  4.1029 -    apply (auto simp add: less_SUP_iff)
  4.1030 -    using eventually_elim2 less_INF_D by fastforce
  4.1031 -  then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> u n > C" using eventually_sequentially by auto
  4.1032 -  define D where "D = min (real_of_ereal C) (Min {u n |n. n \<le> N})"
  4.1033 -  have "\<And>n. u n \<ge> D"
  4.1034 -  proof -
  4.1035 -    fix n show "u n \<ge> D"
  4.1036 -    proof (cases)
  4.1037 -      assume *: "n \<le> N"
  4.1038 -      have "u n \<ge> Min {u n |n. n \<le> N}" by (rule Min_le, auto simp add: *)
  4.1039 -      then show "u n \<ge> D" unfolding D_def by linarith
  4.1040 -    next
  4.1041 -      assume "\<not>(n \<le> N)"
  4.1042 -      then have "n \<ge> N" by simp
  4.1043 -      then have "u n > C" using N by auto
  4.1044 -      then have "u n > real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
  4.1045 -      then show "u n \<ge> D" unfolding D_def by linarith
  4.1046 -    qed
  4.1047 -  qed
  4.1048 -  then show ?thesis by blast
  4.1049 -qed
  4.1050 -
  4.1051 -lemma liminf_upper_bound:
  4.1052 -  fixes u:: "nat \<Rightarrow> ereal"
  4.1053 -  assumes "liminf u < l"
  4.1054 -  shows "\<exists>N>k. u N < l"
  4.1055 -by (metis assms gt_ex less_le_trans liminf_bounded_iff not_less)
  4.1056 -
  4.1057 -text \<open>The following statement about limsups is reduced to a statement about limits using
  4.1058 -subsequences thanks to \verb+limsup_subseq_lim+. The statement for limits follows for instance from
  4.1059 -\verb+tendsto_add_ereal_general+.\<close>
  4.1060 -
  4.1061 -lemma ereal_limsup_add_mono:
  4.1062 -  fixes u v::"nat \<Rightarrow> ereal"
  4.1063 -  shows "limsup (\<lambda>n. u n + v n) \<le> limsup u + limsup v"
  4.1064 -proof (cases)
  4.1065 -  assume "(limsup u = \<infinity>) \<or> (limsup v = \<infinity>)"
  4.1066 -  then have "limsup u + limsup v = \<infinity>" by simp
  4.1067 -  then show ?thesis by auto
  4.1068 -next
  4.1069 -  assume "\<not>((limsup u = \<infinity>) \<or> (limsup v = \<infinity>))"
  4.1070 -  then have "limsup u < \<infinity>" "limsup v < \<infinity>" by auto
  4.1071 -
  4.1072 -  define w where "w = (\<lambda>n. u n + v n)"
  4.1073 -  obtain r where r: "strict_mono r" "(w o r) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
  4.1074 -  obtain s where s: "strict_mono s" "(u o r o s) \<longlonglongrightarrow> limsup (u o r)" using limsup_subseq_lim by auto
  4.1075 -  obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
  4.1076 -
  4.1077 -  define a where "a = r o s o t"
  4.1078 -  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
  4.1079 -  have l:"(w o a) \<longlonglongrightarrow> limsup w"
  4.1080 -         "(u o a) \<longlonglongrightarrow> limsup (u o r)"
  4.1081 -         "(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
  4.1082 -  apply (metis (no_types, lifting) r(2) s(1) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  4.1083 -  apply (metis (no_types, lifting) s(2) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  4.1084 -  apply (metis (no_types, lifting) t(2) a_def comp_assoc)
  4.1085 -  done
  4.1086 -
  4.1087 -  have "limsup (u o r) \<le> limsup u" by (simp add: limsup_subseq_mono r(1))
  4.1088 -  then have a: "limsup (u o r) \<noteq> \<infinity>" using \<open>limsup u < \<infinity>\<close> by auto
  4.1089 -  have "limsup (v o r o s) \<le> limsup v" 
  4.1090 -    by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) strict_mono_o)
  4.1091 -  then have b: "limsup (v o r o s) \<noteq> \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
  4.1092 -
  4.1093 -  have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)"
  4.1094 -    using l tendsto_add_ereal_general a b by fastforce
  4.1095 -  moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
  4.1096 -  ultimately have "(w o a) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)" by simp
  4.1097 -  then have "limsup w = limsup (u o r) + limsup (v o r o s)" using l(1) LIMSEQ_unique by blast
  4.1098 -  then have "limsup w \<le> limsup u + limsup v"
  4.1099 -    using \<open>limsup (u o r) \<le> limsup u\<close> \<open>limsup (v o r o s) \<le> limsup v\<close> ereal_add_mono by simp
  4.1100 -  then show ?thesis unfolding w_def by simp
  4.1101 -qed
  4.1102 -
  4.1103 -text \<open>There is an asymmetry between liminfs and limsups in ereal, as $\infty + (-\infty) = \infty$.
  4.1104 -This explains why there are more assumptions in the next lemma dealing with liminfs that in the
  4.1105 -previous one about limsups.\<close>
  4.1106 -
  4.1107 -lemma ereal_liminf_add_mono:
  4.1108 -  fixes u v::"nat \<Rightarrow> ereal"
  4.1109 -  assumes "\<not>((liminf u = \<infinity> \<and> liminf v = -\<infinity>) \<or> (liminf u = -\<infinity> \<and> liminf v = \<infinity>))"
  4.1110 -  shows "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
  4.1111 -proof (cases)
  4.1112 -  assume "(liminf u = -\<infinity>) \<or> (liminf v = -\<infinity>)"
  4.1113 -  then have *: "liminf u + liminf v = -\<infinity>" using assms by auto
  4.1114 -  show ?thesis by (simp add: *)
  4.1115 -next
  4.1116 -  assume "\<not>((liminf u = -\<infinity>) \<or> (liminf v = -\<infinity>))"
  4.1117 -  then have "liminf u > -\<infinity>" "liminf v > -\<infinity>" by auto
  4.1118 -
  4.1119 -  define w where "w = (\<lambda>n. u n + v n)"
  4.1120 -  obtain r where r: "strict_mono r" "(w o r) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
  4.1121 -  obtain s where s: "strict_mono s" "(u o r o s) \<longlonglongrightarrow> liminf (u o r)" using liminf_subseq_lim by auto
  4.1122 -  obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> liminf (v o r o s)" using liminf_subseq_lim by auto
  4.1123 -
  4.1124 -  define a where "a = r o s o t"
  4.1125 -  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
  4.1126 -  have l:"(w o a) \<longlonglongrightarrow> liminf w"
  4.1127 -         "(u o a) \<longlonglongrightarrow> liminf (u o r)"
  4.1128 -         "(v o a) \<longlonglongrightarrow> liminf (v o r o s)"
  4.1129 -  apply (metis (no_types, lifting) r(2) s(1) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  4.1130 -  apply (metis (no_types, lifting) s(2) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  4.1131 -  apply (metis (no_types, lifting) t(2) a_def comp_assoc)
  4.1132 -  done
  4.1133 -
  4.1134 -  have "liminf (u o r) \<ge> liminf u" by (simp add: liminf_subseq_mono r(1))
  4.1135 -  then have a: "liminf (u o r) \<noteq> -\<infinity>" using \<open>liminf u > -\<infinity>\<close> by auto
  4.1136 -  have "liminf (v o r o s) \<ge> liminf v" 
  4.1137 -    by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) strict_mono_o)
  4.1138 -  then have b: "liminf (v o r o s) \<noteq> -\<infinity>" using \<open>liminf v > -\<infinity>\<close> by auto
  4.1139 -
  4.1140 -  have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)"
  4.1141 -    using l tendsto_add_ereal_general a b by fastforce
  4.1142 -  moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
  4.1143 -  ultimately have "(w o a) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)" by simp
  4.1144 -  then have "liminf w = liminf (u o r) + liminf (v o r o s)" using l(1) LIMSEQ_unique by blast
  4.1145 -  then have "liminf w \<ge> liminf u + liminf v"
  4.1146 -    using \<open>liminf (u o r) \<ge> liminf u\<close> \<open>liminf (v o r o s) \<ge> liminf v\<close> ereal_add_mono by simp
  4.1147 -  then show ?thesis unfolding w_def by simp
  4.1148 -qed
  4.1149 -
  4.1150 -lemma ereal_limsup_lim_add:
  4.1151 -  fixes u v::"nat \<Rightarrow> ereal"
  4.1152 -  assumes "u \<longlonglongrightarrow> a" "abs(a) \<noteq> \<infinity>"
  4.1153 -  shows "limsup (\<lambda>n. u n + v n) = a + limsup v"
  4.1154 -proof -
  4.1155 -  have "limsup u = a" using assms(1) using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  4.1156 -  have "(\<lambda>n. -u n) \<longlonglongrightarrow> -a" using assms(1) by auto
  4.1157 -  then have "limsup (\<lambda>n. -u n) = -a" using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  4.1158 -
  4.1159 -  have "limsup (\<lambda>n. u n + v n) \<le> limsup u + limsup v"
  4.1160 -    by (rule ereal_limsup_add_mono)
  4.1161 -  then have up: "limsup (\<lambda>n. u n + v n) \<le> a + limsup v" using \<open>limsup u = a\<close> by simp
  4.1162 -
  4.1163 -  have a: "limsup (\<lambda>n. (u n + v n) + (-u n)) \<le> limsup (\<lambda>n. u n + v n) + limsup (\<lambda>n. -u n)"
  4.1164 -    by (rule ereal_limsup_add_mono)
  4.1165 -  have "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) sequentially" using assms
  4.1166 -    real_lim_then_eventually_real by auto
  4.1167 -  moreover have "\<And>x. x = ereal(real_of_ereal(x)) \<Longrightarrow> x + (-x) = 0"
  4.1168 -    by (metis plus_ereal.simps(1) right_minus uminus_ereal.simps(1) zero_ereal_def)
  4.1169 -  ultimately have "eventually (\<lambda>n. u n + (-u n) = 0) sequentially"
  4.1170 -    by (metis (mono_tags, lifting) eventually_mono)
  4.1171 -  moreover have "\<And>n. u n + (-u n) = 0 \<Longrightarrow> u n + v n + (-u n) = v n"
  4.1172 -    by (metis add.commute add.left_commute add.left_neutral)
  4.1173 -  ultimately have "eventually (\<lambda>n. u n + v n + (-u n) = v n) sequentially"
  4.1174 -    using eventually_mono by force
  4.1175 -  then have "limsup v = limsup (\<lambda>n. u n + v n + (-u n))" using Limsup_eq by force
  4.1176 -  then have "limsup v \<le> limsup (\<lambda>n. u n + v n) -a" using a \<open>limsup (\<lambda>n. -u n) = -a\<close> by (simp add: minus_ereal_def)
  4.1177 -  then have "limsup (\<lambda>n. u n + v n) \<ge> a + limsup v" using assms(2) by (metis add.commute ereal_le_minus)
  4.1178 -  then show ?thesis using up by simp
  4.1179 -qed
  4.1180 -
  4.1181 -lemma ereal_limsup_lim_mult:
  4.1182 -  fixes u v::"nat \<Rightarrow> ereal"
  4.1183 -  assumes "u \<longlonglongrightarrow> a" "a>0" "a \<noteq> \<infinity>"
  4.1184 -  shows "limsup (\<lambda>n. u n * v n) = a * limsup v"
  4.1185 -proof -
  4.1186 -  define w where "w = (\<lambda>n. u n * v n)"
  4.1187 -  obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
  4.1188 -  have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
  4.1189 -  with tendsto_mult_ereal[OF this r(2)] have "(\<lambda>n. (u o r) n * (v o r) n) \<longlonglongrightarrow> a * limsup v" using assms(2) assms(3) by auto
  4.1190 -  moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
  4.1191 -  ultimately have "(w o r) \<longlonglongrightarrow> a * limsup v" unfolding w_def by presburger
  4.1192 -  then have "limsup (w o r) = a * limsup v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  4.1193 -  then have I: "limsup w \<ge> a * limsup v" by (metis limsup_subseq_mono r(1))
  4.1194 -
  4.1195 -  obtain s where s: "strict_mono s" "(w o s) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
  4.1196 -  have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
  4.1197 -  have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
  4.1198 -  moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
  4.1199 -  moreover have "(w o s) n / (u o s) n = (v o s) n" if "(u o s) n > 0" "(u o s) n < \<infinity>" for n
  4.1200 -    unfolding w_def using that by (auto simp add: ereal_divide_eq)
  4.1201 -  ultimately have "eventually (\<lambda>n. (w o s) n / (u o s) n = (v o s) n) sequentially" using eventually_elim2 by force
  4.1202 -  moreover have "(\<lambda>n. (w o s) n / (u o s) n) \<longlonglongrightarrow> (limsup w) / a"
  4.1203 -    apply (rule tendsto_divide_ereal[OF s(2) *]) using assms(2) assms(3) by auto
  4.1204 -  ultimately have "(v o s) \<longlonglongrightarrow> (limsup w) / a" using Lim_transform_eventually by fastforce
  4.1205 -  then have "limsup (v o s) = (limsup w) / a" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  4.1206 -  then have "limsup v \<ge> (limsup w) / a" by (metis limsup_subseq_mono s(1))
  4.1207 -  then have "a * limsup v \<ge> limsup w" using assms(2) assms(3) by (simp add: ereal_divide_le_pos)
  4.1208 -  then show ?thesis using I unfolding w_def by auto
  4.1209 -qed
  4.1210 -
  4.1211 -lemma ereal_liminf_lim_mult:
  4.1212 -  fixes u v::"nat \<Rightarrow> ereal"
  4.1213 -  assumes "u \<longlonglongrightarrow> a" "a>0" "a \<noteq> \<infinity>"
  4.1214 -  shows "liminf (\<lambda>n. u n * v n) = a * liminf v"
  4.1215 -proof -
  4.1216 -  define w where "w = (\<lambda>n. u n * v n)"
  4.1217 -  obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
  4.1218 -  have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
  4.1219 -  with tendsto_mult_ereal[OF this r(2)] have "(\<lambda>n. (u o r) n * (v o r) n) \<longlonglongrightarrow> a * liminf v" using assms(2) assms(3) by auto
  4.1220 -  moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
  4.1221 -  ultimately have "(w o r) \<longlonglongrightarrow> a * liminf v" unfolding w_def by presburger
  4.1222 -  then have "liminf (w o r) = a * liminf v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  4.1223 -  then have I: "liminf w \<le> a * liminf v" by (metis liminf_subseq_mono r(1))
  4.1224 -
  4.1225 -  obtain s where s: "strict_mono s" "(w o s) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
  4.1226 -  have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
  4.1227 -  have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
  4.1228 -  moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
  4.1229 -  moreover have "(w o s) n / (u o s) n = (v o s) n" if "(u o s) n > 0" "(u o s) n < \<infinity>" for n
  4.1230 -    unfolding w_def using that by (auto simp add: ereal_divide_eq)
  4.1231 -  ultimately have "eventually (\<lambda>n. (w o s) n / (u o s) n = (v o s) n) sequentially" using eventually_elim2 by force
  4.1232 -  moreover have "(\<lambda>n. (w o s) n / (u o s) n) \<longlonglongrightarrow> (liminf w) / a"
  4.1233 -    apply (rule tendsto_divide_ereal[OF s(2) *]) using assms(2) assms(3) by auto
  4.1234 -  ultimately have "(v o s) \<longlonglongrightarrow> (liminf w) / a" using Lim_transform_eventually by fastforce
  4.1235 -  then have "liminf (v o s) = (liminf w) / a" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  4.1236 -  then have "liminf v \<le> (liminf w) / a" by (metis liminf_subseq_mono s(1))
  4.1237 -  then have "a * liminf v \<le> liminf w" using assms(2) assms(3) by (simp add: ereal_le_divide_pos)
  4.1238 -  then show ?thesis using I unfolding w_def by auto
  4.1239 -qed
  4.1240 -
  4.1241 -lemma ereal_liminf_lim_add:
  4.1242 -  fixes u v::"nat \<Rightarrow> ereal"
  4.1243 -  assumes "u \<longlonglongrightarrow> a" "abs(a) \<noteq> \<infinity>"
  4.1244 -  shows "liminf (\<lambda>n. u n + v n) = a + liminf v"
  4.1245 -proof -
  4.1246 -  have "liminf u = a" using assms(1) tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  4.1247 -  then have *: "abs(liminf u) \<noteq> \<infinity>" using assms(2) by auto
  4.1248 -  have "(\<lambda>n. -u n) \<longlonglongrightarrow> -a" using assms(1) by auto
  4.1249 -  then have "liminf (\<lambda>n. -u n) = -a" using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  4.1250 -  then have **: "abs(liminf (\<lambda>n. -u n)) \<noteq> \<infinity>" using assms(2) by auto
  4.1251 -
  4.1252 -  have "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
  4.1253 -    apply (rule ereal_liminf_add_mono) using * by auto
  4.1254 -  then have up: "liminf (\<lambda>n. u n + v n) \<ge> a + liminf v" using \<open>liminf u = a\<close> by simp
  4.1255 -
  4.1256 -  have a: "liminf (\<lambda>n. (u n + v n) + (-u n)) \<ge> liminf (\<lambda>n. u n + v n) + liminf (\<lambda>n. -u n)"
  4.1257 -    apply (rule ereal_liminf_add_mono) using ** by auto
  4.1258 -  have "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) sequentially" using assms
  4.1259 -    real_lim_then_eventually_real by auto
  4.1260 -  moreover have "\<And>x. x = ereal(real_of_ereal(x)) \<Longrightarrow> x + (-x) = 0"
  4.1261 -    by (metis plus_ereal.simps(1) right_minus uminus_ereal.simps(1) zero_ereal_def)
  4.1262 -  ultimately have "eventually (\<lambda>n. u n + (-u n) = 0) sequentially"
  4.1263 -    by (metis (mono_tags, lifting) eventually_mono)
  4.1264 -  moreover have "\<And>n. u n + (-u n) = 0 \<Longrightarrow> u n + v n + (-u n) = v n"
  4.1265 -    by (metis add.commute add.left_commute add.left_neutral)
  4.1266 -  ultimately have "eventually (\<lambda>n. u n + v n + (-u n) = v n) sequentially"
  4.1267 -    using eventually_mono by force
  4.1268 -  then have "liminf v = liminf (\<lambda>n. u n + v n + (-u n))" using Liminf_eq by force
  4.1269 -  then have "liminf v \<ge> liminf (\<lambda>n. u n + v n) -a" using a \<open>liminf (\<lambda>n. -u n) = -a\<close> by (simp add: minus_ereal_def)
  4.1270 -  then have "liminf (\<lambda>n. u n + v n) \<le> a + liminf v" using assms(2) by (metis add.commute ereal_minus_le)
  4.1271 -  then show ?thesis using up by simp
  4.1272 -qed
  4.1273 -
  4.1274 -lemma ereal_liminf_limsup_add:
  4.1275 -  fixes u v::"nat \<Rightarrow> ereal"
  4.1276 -  shows "liminf (\<lambda>n. u n + v n) \<le> liminf u + limsup v"
  4.1277 -proof (cases)
  4.1278 -  assume "limsup v = \<infinity> \<or> liminf u = \<infinity>"
  4.1279 -  then show ?thesis by auto
  4.1280 -next
  4.1281 -  assume "\<not>(limsup v = \<infinity> \<or> liminf u = \<infinity>)"
  4.1282 -  then have "limsup v < \<infinity>" "liminf u < \<infinity>" by auto
  4.1283 -
  4.1284 -  define w where "w = (\<lambda>n. u n + v n)"
  4.1285 -  obtain r where r: "strict_mono r" "(u o r) \<longlonglongrightarrow> liminf u" using liminf_subseq_lim by auto
  4.1286 -  obtain s where s: "strict_mono s" "(w o r o s) \<longlonglongrightarrow> liminf (w o r)" using liminf_subseq_lim by auto
  4.1287 -  obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
  4.1288 -
  4.1289 -  define a where "a = r o s o t"
  4.1290 -  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
  4.1291 -  have l:"(u o a) \<longlonglongrightarrow> liminf u"
  4.1292 -         "(w o a) \<longlonglongrightarrow> liminf (w o r)"
  4.1293 -         "(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
  4.1294 -  apply (metis (no_types, lifting) r(2) s(1) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  4.1295 -  apply (metis (no_types, lifting) s(2) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  4.1296 -  apply (metis (no_types, lifting) t(2) a_def comp_assoc)
  4.1297 -  done
  4.1298 -
  4.1299 -  have "liminf (w o r) \<ge> liminf w" by (simp add: liminf_subseq_mono r(1))
  4.1300 -  have "limsup (v o r o s) \<le> limsup v" 
  4.1301 -    by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) strict_mono_o)
  4.1302 -  then have b: "limsup (v o r o s) < \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
  4.1303 -
  4.1304 -  have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf u + limsup (v o r o s)"
  4.1305 -    apply (rule tendsto_add_ereal_general) using b \<open>liminf u < \<infinity>\<close> l(1) l(3) by force+
  4.1306 -  moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
  4.1307 -  ultimately have "(w o a) \<longlonglongrightarrow> liminf u + limsup (v o r o s)" by simp
  4.1308 -  then have "liminf (w o r) = liminf u + limsup (v o r o s)" using l(2) using LIMSEQ_unique by blast
  4.1309 -  then have "liminf w \<le> liminf u + limsup v"
  4.1310 -    using \<open>liminf (w o r) \<ge> liminf w\<close> \<open>limsup (v o r o s) \<le> limsup v\<close>
  4.1311 -    by (metis add_mono_thms_linordered_semiring(2) le_less_trans not_less)
  4.1312 -  then show ?thesis unfolding w_def by simp
  4.1313 -qed
  4.1314 -
  4.1315 -lemma ereal_liminf_limsup_minus:
  4.1316 -  fixes u v::"nat \<Rightarrow> ereal"
  4.1317 -  shows "liminf (\<lambda>n. u n - v n) \<le> limsup u - limsup v"
  4.1318 -  unfolding minus_ereal_def
  4.1319 -  apply (subst add.commute)
  4.1320 -  apply (rule order_trans[OF ereal_liminf_limsup_add])
  4.1321 -  using ereal_Limsup_uminus[of sequentially "\<lambda>n. - v n"]
  4.1322 -  apply (simp add: add.commute)
  4.1323 -  done
  4.1324 -
  4.1325 -
  4.1326 -lemma liminf_minus_ennreal:
  4.1327 -  fixes u v::"nat \<Rightarrow> ennreal"
  4.1328 -  shows "(\<And>n. v n \<le> u n) \<Longrightarrow> liminf (\<lambda>n. u n - v n) \<le> limsup u - limsup v"
  4.1329 -  unfolding liminf_SUP_INF limsup_INF_SUP
  4.1330 -  including ennreal.lifting
  4.1331 -proof (transfer, clarsimp)
  4.1332 -  fix v u :: "nat \<Rightarrow> ereal" assume *: "\<forall>x. 0 \<le> v x" "\<forall>x. 0 \<le> u x" "\<And>n. v n \<le> u n"
  4.1333 -  moreover have "0 \<le> limsup u - limsup v"
  4.1334 -    using * by (intro ereal_diff_positive Limsup_mono always_eventually) simp
  4.1335 -  moreover have "0 \<le> (SUPREMUM {x..} v)" for x
  4.1336 -    using * by (intro SUP_upper2[of x]) auto
  4.1337 -  moreover have "0 \<le> (SUPREMUM {x..} u)" for x
  4.1338 -    using * by (intro SUP_upper2[of x]) auto
  4.1339 -  ultimately show "(SUP n. INF n:{n..}. max 0 (u n - v n))
  4.1340 -            \<le> max 0 ((INF x. max 0 (SUPREMUM {x..} u)) - (INF x. max 0 (SUPREMUM {x..} v)))"
  4.1341 -    by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
  4.1342 -qed
  4.1343 -
  4.1344  (*
  4.1345      Notation
  4.1346  *)
     5.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Fri Aug 18 22:55:54 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Sun Aug 20 03:35:20 2017 +0200
     5.3 @@ -10,6 +10,7 @@
     5.4    "HOL-Library.Discrete"
     5.5    "HOL-Library.Extended_Real"
     5.6    "HOL-Library.Liminf_Limsup"
     5.7 +  "Extended_Real_Limits"
     5.8  begin
     5.9  
    5.10  text \<open>
    5.11 @@ -707,6 +708,41 @@
    5.12      by (intro exI[of _ "of_real r"]) simp
    5.13  qed
    5.14  
    5.15 +lemma conv_radius_conv_Sup:
    5.16 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
    5.17 +  shows "conv_radius f = Sup {r. \<forall>z. ereal (norm z) < r \<longrightarrow> summable (\<lambda>n. f n * z ^ n)}"
    5.18 +proof (rule Sup_eqI [symmetric], goal_cases)
    5.19 +  case (1 r)
    5.20 +  thus ?case
    5.21 +    by (intro conv_radius_geI_ex') auto
    5.22 +next
    5.23 +  case (2 r)
    5.24 +  from 2[of 0] have r: "r \<ge> 0" by auto
    5.25 +  show ?case
    5.26 +  proof (intro conv_radius_leI_ex' r)
    5.27 +    fix R assume R: "R > 0" "ereal R > r"
    5.28 +    with r obtain r' where [simp]: "r = ereal r'" by (cases r) auto
    5.29 +    show "\<not>summable (\<lambda>n. f n * of_real R ^ n)"
    5.30 +    proof
    5.31 +      assume *: "summable (\<lambda>n. f n * of_real R ^ n)"
    5.32 +      define R' where "R' = (R + r') / 2"
    5.33 +      from R have R': "R' > r'" "R' < R" by (simp_all add: R'_def)
    5.34 +      hence "\<forall>z. norm z < R' \<longrightarrow> summable (\<lambda>n. f n * z ^ n)"
    5.35 +        using powser_inside[OF *] by auto
    5.36 +      from 2[of R'] and this have "R' \<le> r'" by auto
    5.37 +      with \<open>R' > r'\<close> show False by simp
    5.38 +    qed
    5.39 +  qed
    5.40 +qed
    5.41 +
    5.42 +lemma conv_radius_shift:
    5.43 +  fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
    5.44 +  shows   "conv_radius (\<lambda>n. f (n + m)) = conv_radius f"
    5.45 +  unfolding conv_radius_conv_Sup summable_powser_ignore_initial_segment ..
    5.46 +
    5.47 +lemma conv_radius_norm [simp]: "conv_radius (\<lambda>x. norm (f x)) = conv_radius f"
    5.48 +  by (simp add: conv_radius_def)
    5.49 +
    5.50  lemma conv_radius_ratio_limit_ereal:
    5.51    fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
    5.52    assumes nz:  "eventually (\<lambda>n. f n \<noteq> 0) sequentially"
    5.53 @@ -773,6 +809,31 @@
    5.54    shows   "conv_radius f = c'"
    5.55    using assms by (intro conv_radius_ratio_limit_ereal_nonzero) simp_all
    5.56  
    5.57 +lemma conv_radius_cmult_left:
    5.58 +  assumes "c \<noteq> (0 :: 'a :: {banach, real_normed_div_algebra})"
    5.59 +  shows   "conv_radius (\<lambda>n. c * f n) = conv_radius f"
    5.60 +proof -
    5.61 +  have "conv_radius (\<lambda>n. c * f n) = 
    5.62 +          inverse (limsup (\<lambda>n. ereal (root n (norm (c * f n)))))"
    5.63 +    unfolding conv_radius_def ..
    5.64 +  also have "(\<lambda>n. ereal (root n (norm (c * f n)))) = 
    5.65 +               (\<lambda>n. ereal (root n (norm c)) * ereal (root n (norm (f n))))"
    5.66 +    by (rule ext) (auto simp: norm_mult real_root_mult)
    5.67 +  also have "limsup \<dots> = ereal 1 * limsup (\<lambda>n. ereal (root n (norm (f n))))"
    5.68 +    using assms by (intro ereal_limsup_lim_mult tendsto_ereal LIMSEQ_root_const) auto
    5.69 +  also have "inverse \<dots> = conv_radius f" by (simp add: conv_radius_def)
    5.70 +  finally show ?thesis .
    5.71 +qed
    5.72 +
    5.73 +lemma conv_radius_cmult_right:
    5.74 +  assumes "c \<noteq> (0 :: 'a :: {banach, real_normed_div_algebra})"
    5.75 +  shows   "conv_radius (\<lambda>n. f n * c) = conv_radius f"
    5.76 +proof -
    5.77 +  have "conv_radius (\<lambda>n. f n * c) = conv_radius (\<lambda>n. c * f n)"
    5.78 +    by (simp add: conv_radius_def norm_mult mult.commute)
    5.79 +  with conv_radius_cmult_left[OF assms, of f] show ?thesis by simp
    5.80 +qed
    5.81 +
    5.82  lemma conv_radius_mult_power:
    5.83    assumes "c \<noteq> (0 :: 'a :: {real_normed_div_algebra,banach})"
    5.84    shows   "conv_radius (\<lambda>n. c ^ n * f n) = conv_radius f / ereal (norm c)"
     6.1 --- a/src/HOL/Limits.thy	Fri Aug 18 22:55:54 2017 +0200
     6.2 +++ b/src/HOL/Limits.thy	Sun Aug 20 03:35:20 2017 +0200
     6.3 @@ -1617,6 +1617,17 @@
     6.4  qed simp
     6.5  
     6.6  
     6.7 +lemma filterlim_divide_at_infinity:
     6.8 +  fixes f g :: "'a \<Rightarrow> 'a :: real_normed_field"
     6.9 +  assumes "filterlim f (nhds c) F" "filterlim g (at 0) F" "c \<noteq> 0"
    6.10 +  shows   "filterlim (\<lambda>x. f x / g x) at_infinity F"
    6.11 +proof -
    6.12 +  have "filterlim (\<lambda>x. f x * inverse (g x)) at_infinity F"
    6.13 +    by (intro tendsto_mult_filterlim_at_infinity[OF assms(1,3)]
    6.14 +          filterlim_compose [OF filterlim_inverse_at_infinity assms(2)])
    6.15 +  thus ?thesis by (simp add: field_simps)
    6.16 +qed
    6.17 +
    6.18  subsection \<open>Floor and Ceiling\<close>
    6.19  
    6.20  lemma eventually_floor_less:
     7.1 --- a/src/HOL/Series.thy	Fri Aug 18 22:55:54 2017 +0200
     7.2 +++ b/src/HOL/Series.thy	Sun Aug 20 03:35:20 2017 +0200
     7.3 @@ -983,6 +983,20 @@
     7.4    finally show ?thesis .
     7.5  qed
     7.6  
     7.7 +lemma summable_powser_ignore_initial_segment:
     7.8 +  fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra"
     7.9 +  shows "summable (\<lambda>n. f (n + m) * z ^ n) \<longleftrightarrow> summable (\<lambda>n. f n * z ^ n)"
    7.10 +proof (induction m)
    7.11 +  case (Suc m)
    7.12 +  have "summable (\<lambda>n. f (n + Suc m) * z ^ n) = summable (\<lambda>n. f (Suc n + m) * z ^ n)"
    7.13 +    by simp
    7.14 +  also have "\<dots> = summable (\<lambda>n. f (n + m) * z ^ n)"
    7.15 +    by (rule summable_powser_split_head)
    7.16 +  also have "\<dots> = summable (\<lambda>n. f n * z ^ n)"
    7.17 +    by (rule Suc.IH)
    7.18 +  finally show ?case .
    7.19 +qed simp_all
    7.20 +
    7.21  lemma powser_split_head:
    7.22    fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
    7.23    assumes "summable (\<lambda>n. f n * z ^ n)"