# HG changeset patch
# User hoelzl
# Date 1454997872 -3600
# Node ID 7c288c0c7300c14307e571dbe7638a3eecb98da2
# Parent  4a35e3945cab1008f435e92e945bba51790fca0d
add tendsto_add_ereal_nonneg

diff -r 4a35e3945cab -r 7c288c0c7300 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Feb 09 07:04:20 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Tue Feb 09 07:04:32 2016 +0100
@@ -2702,6 +2702,37 @@
     by (simp add: x' y' cong: filterlim_cong)
 qed
 
+lemma tendsto_add_ereal_nonneg:
+  fixes x y :: "ereal"
+  assumes "x \<noteq> -\<infinity>" "y \<noteq> -\<infinity>" "(f \<longlongrightarrow> x) F" "(g \<longlongrightarrow> y) F"
+  shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
+proof cases
+  assume "x = \<infinity> \<or> y = \<infinity>"
+  moreover
+  { fix y :: ereal and f g :: "'a \<Rightarrow> ereal" assume "y \<noteq> -\<infinity>" "(f \<longlongrightarrow> \<infinity>) F" "(g \<longlongrightarrow> y) F"
+    then obtain y' where "-\<infinity> < y'" "y' < y"
+      using dense[of "-\<infinity>" y] by auto
+    have "((\<lambda>x. f x + g x) \<longlongrightarrow> \<infinity>) F"
+    proof (rule tendsto_sandwich)
+      have "\<forall>\<^sub>F x in F. y' < g x"
+        using order_tendstoD(1)[OF \<open>(g \<longlongrightarrow> y) F\<close> \<open>y' < y\<close>] by auto
+      then show "\<forall>\<^sub>F x in F. f x + y' \<le> f x + g x"
+        by eventually_elim (auto intro!: add_mono)
+      show "\<forall>\<^sub>F n in F. f n + g n \<le> \<infinity>" "((\<lambda>n. \<infinity>) \<longlongrightarrow> \<infinity>) F"
+        by auto
+      show "((\<lambda>x. f x + y') \<longlongrightarrow> \<infinity>) F"
+        using tendsto_cadd_ereal[of y' \<infinity> f F] \<open>(f \<longlongrightarrow> \<infinity>) F\<close> \<open>-\<infinity> < y'\<close> by auto
+    qed }
+  note this[of y f g] this[of x g f]
+  ultimately show ?thesis
+    using assms by (auto simp: add_ac)
+next
+  assume "\<not> (x = \<infinity> \<or> y = \<infinity>)"
+  with assms tendsto_add_ereal[of x y f F g]
+  show ?thesis
+    by auto
+qed
+
 lemma ereal_inj_affinity:
   fixes m t :: ereal
   assumes "\<bar>m\<bar> \<noteq> \<infinity>"