591 case (real r) |
591 case (real r) |
592 then show ?thesis |
592 then show ?thesis |
593 using reals_Archimedean2[of r] by simp |
593 using reals_Archimedean2[of r] by simp |
594 qed simp_all |
594 qed simp_all |
595 |
595 |
596 lemma ereal_add_mono: |
596 lemma ereal_add_strict_mono2: |
597 fixes a b c d :: ereal |
597 fixes a b c d :: ereal |
598 assumes "a \<le> b" |
598 assumes "a < b" |
599 and "c \<le> d" |
599 and "c < d" |
600 shows "a + c \<le> b + d" |
600 shows "a + c < b + d" |
601 using assms |
601 using assms |
602 apply (cases a) |
602 apply (cases a) |
603 apply (cases rule: ereal3_cases[of b c d], auto) |
603 apply (cases rule: ereal3_cases[of b c d], auto) |
604 apply (cases rule: ereal3_cases[of b c d], auto) |
604 apply (cases rule: ereal3_cases[of b c d], auto) |
605 done |
605 done |
606 |
606 |
607 lemma ereal_minus_le_minus[simp]: |
607 lemma ereal_minus_le_minus[simp]: |
608 fixes a b :: ereal |
608 fixes a b :: ereal |
609 shows "- a \<le> - b \<longleftrightarrow> b \<le> a" |
609 shows "- a \<le> - b \<longleftrightarrow> b \<le> a" |
610 by (cases rule: ereal2_cases[of a b]) auto |
610 by (cases rule: ereal2_cases[of a b]) auto |
671 |
671 |
672 lemma ereal_abs_leI: |
672 lemma ereal_abs_leI: |
673 fixes x y :: ereal |
673 fixes x y :: ereal |
674 shows "\<lbrakk> x \<le> y; -x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y" |
674 shows "\<lbrakk> x \<le> y; -x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y" |
675 by(cases x y rule: ereal2_cases)(simp_all) |
675 by(cases x y rule: ereal2_cases)(simp_all) |
|
676 |
|
677 lemma ereal_abs_add: |
|
678 fixes a b::ereal |
|
679 shows "abs(a+b) \<le> abs a + abs b" |
|
680 by (cases rule: ereal2_cases[of a b]) (auto) |
676 |
681 |
677 lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>" |
682 lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>" |
678 by (cases x) auto |
683 by (cases x) auto |
679 |
684 |
680 lemma abs_real_of_ereal[simp]: "\<bar>real_of_ereal (x :: ereal)\<bar> = real_of_ereal \<bar>x\<bar>" |
685 lemma abs_real_of_ereal[simp]: "\<bar>real_of_ereal (x :: ereal)\<bar> = real_of_ereal \<bar>x\<bar>" |
780 and ereal_decseq_uminus[simp]: "decseq (\<lambda>x. - f x) \<longleftrightarrow> incseq f" |
785 and ereal_decseq_uminus[simp]: "decseq (\<lambda>x. - f x) \<longleftrightarrow> incseq f" |
781 unfolding decseq_def incseq_def by auto |
786 unfolding decseq_def incseq_def by auto |
782 |
787 |
783 lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))" |
788 lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))" |
784 unfolding incseq_def by auto |
789 unfolding incseq_def by auto |
785 |
|
786 lemma ereal_add_nonneg_nonneg[simp]: |
|
787 fixes a b :: ereal |
|
788 shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b" |
|
789 using add_mono[of 0 a 0 b] by simp |
|
790 |
790 |
791 lemma sum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)" |
791 lemma sum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)" |
792 proof (cases "finite A") |
792 proof (cases "finite A") |
793 case True |
793 case True |
794 then show ?thesis by induct auto |
794 then show ?thesis by induct auto |
1047 lemma ereal_mult_left_mono: |
1047 lemma ereal_mult_left_mono: |
1048 fixes a b c :: ereal |
1048 fixes a b c :: ereal |
1049 shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" |
1049 shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" |
1050 using ereal_mult_right_mono |
1050 using ereal_mult_right_mono |
1051 by (simp add: mult.commute[of c]) |
1051 by (simp add: mult.commute[of c]) |
|
1052 |
|
1053 lemma ereal_mult_mono: |
|
1054 fixes a b c d::ereal |
|
1055 assumes "b \<ge> 0" "c \<ge> 0" "a \<le> b" "c \<le> d" |
|
1056 shows "a * c \<le> b * d" |
|
1057 by (metis ereal_mult_right_mono mult.commute order_trans assms) |
|
1058 |
|
1059 lemma ereal_mult_mono': |
|
1060 fixes a b c d::ereal |
|
1061 assumes "a \<ge> 0" "c \<ge> 0" "a \<le> b" "c \<le> d" |
|
1062 shows "a * c \<le> b * d" |
|
1063 by (metis ereal_mult_right_mono mult.commute order_trans assms) |
|
1064 |
|
1065 lemma ereal_mult_mono_strict: |
|
1066 fixes a b c d::ereal |
|
1067 assumes "b > 0" "c > 0" "a < b" "c < d" |
|
1068 shows "a * c < b * d" |
|
1069 proof - |
|
1070 have "c < \<infinity>" using \<open>c < d\<close> by auto |
|
1071 then have "a * c < b * c" by (metis ereal_mult_strict_left_mono[OF assms(3) assms(2)] mult.commute) |
|
1072 moreover have "b * c \<le> b * d" using assms(2) assms(4) by (simp add: assms(1) ereal_mult_left_mono less_imp_le) |
|
1073 ultimately show ?thesis by simp |
|
1074 qed |
|
1075 |
|
1076 lemma ereal_mult_mono_strict': |
|
1077 fixes a b c d::ereal |
|
1078 assumes "a > 0" "c > 0" "a < b" "c < d" |
|
1079 shows "a * c < b * d" |
|
1080 apply (rule ereal_mult_mono_strict, auto simp add: assms) using assms by auto |
1052 |
1081 |
1053 lemma zero_less_one_ereal[simp]: "0 \<le> (1::ereal)" |
1082 lemma zero_less_one_ereal[simp]: "0 \<le> (1::ereal)" |
1054 by (simp add: one_ereal_def zero_ereal_def) |
1083 by (simp add: one_ereal_def zero_ereal_def) |
1055 |
1084 |
1056 lemma ereal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * (b :: ereal)" |
1085 lemma ereal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * (b :: ereal)" |
1482 by(cases x y rule: ereal2_cases) simp_all |
1511 by(cases x y rule: ereal2_cases) simp_all |
1483 |
1512 |
1484 lemma ediff_le_self [simp]: "x - y \<le> (x :: enat)" |
1513 lemma ediff_le_self [simp]: "x - y \<le> (x :: enat)" |
1485 by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all |
1514 by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all |
1486 |
1515 |
|
1516 lemma ereal_abs_diff: |
|
1517 fixes a b::ereal |
|
1518 shows "abs(a-b) \<le> abs a + abs b" |
|
1519 by (cases rule: ereal2_cases[of a b]) (auto) |
|
1520 |
|
1521 |
1487 subsubsection \<open>Division\<close> |
1522 subsubsection \<open>Division\<close> |
1488 |
1523 |
1489 instantiation ereal :: inverse |
1524 instantiation ereal :: inverse |
1490 begin |
1525 begin |
1491 |
1526 |
2261 by (cases c) (auto simp: \<open>I \<noteq> {}\<close>) |
2296 by (cases c) (auto simp: \<open>I \<noteq> {}\<close>) |
2262 next |
2297 next |
2263 case False |
2298 case False |
2264 then show ?thesis |
2299 then show ?thesis |
2265 by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"]) |
2300 by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"]) |
2266 (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>) |
2301 (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>) |
2267 qed |
2302 qed |
2268 |
2303 |
2269 lemma SUP_ereal_add_right: |
2304 lemma SUP_ereal_add_right: |
2270 fixes c :: ereal |
2305 fixes c :: ereal |
2271 shows "I \<noteq> {} \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> (SUP i:I. c + f i) = c + (SUP i:I. f i)" |
2306 shows "I \<noteq> {} \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> (SUP i:I. c + f i) = c + (SUP i:I. f i)" |
2320 apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty]) |
2355 apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty]) |
2321 apply (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2)) |
2356 apply (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2)) |
2322 apply (subst (2) add.commute) |
2357 apply (subst (2) add.commute) |
2323 apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty assms(3)]) |
2358 apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty assms(3)]) |
2324 apply (subst (2) add.commute) |
2359 apply (subst (2) add.commute) |
2325 apply (rule SUP_combine[symmetric] ereal_add_mono inc[THEN monoD] | assumption)+ |
2360 apply (rule SUP_combine[symmetric] add_mono inc[THEN monoD] | assumption)+ |
2326 done |
2361 done |
2327 |
2362 |
2328 lemma INF_eq_minf: "(INF i:I. f i::ereal) \<noteq> -\<infinity> \<longleftrightarrow> (\<exists>b>-\<infinity>. \<forall>i\<in>I. b \<le> f i)" |
2363 lemma INF_eq_minf: "(INF i:I. f i::ereal) \<noteq> -\<infinity> \<longleftrightarrow> (\<exists>b>-\<infinity>. \<forall>i\<in>I. b \<le> f i)" |
2329 unfolding bot_ereal_def[symmetric] INF_eq_bot_iff by (auto simp: not_less) |
2364 unfolding bot_ereal_def[symmetric] INF_eq_bot_iff by (auto simp: not_less) |
2330 |
2365 |
2334 proof - |
2369 proof - |
2335 have "(INF i:I. f i) \<noteq> -\<infinity>" |
2370 have "(INF i:I. f i) \<noteq> -\<infinity>" |
2336 unfolding INF_eq_minf using assms by (intro exI[of _ 0]) auto |
2371 unfolding INF_eq_minf using assms by (intro exI[of _ 0]) auto |
2337 then show ?thesis |
2372 then show ?thesis |
2338 by (subst continuous_at_Inf_mono[where f="\<lambda>x. x + c"]) |
2373 by (subst continuous_at_Inf_mono[where f="\<lambda>x. x + c"]) |
2339 (auto simp: mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close> continuous_at_imp_continuous_at_within continuous_at) |
2374 (auto simp: mono_def add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close> continuous_at_imp_continuous_at_within continuous_at) |
2340 qed |
2375 qed |
2341 |
2376 |
2342 lemma INF_ereal_add_right: |
2377 lemma INF_ereal_add_right: |
2343 assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x" |
2378 assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x" |
2344 shows "(INF i:I. c + f i :: ereal) = c + (INF i:I. f i)" |
2379 shows "(INF i:I. c + f i :: ereal) = c + (INF i:I. f i)" |
2355 next |
2390 next |
2356 assume "I \<noteq> {}" |
2391 assume "I \<noteq> {}" |
2357 show ?thesis |
2392 show ?thesis |
2358 proof (rule antisym) |
2393 proof (rule antisym) |
2359 show "(INF i:I. f i) + (INF i:I. g i) \<le> (INF i:I. f i + g i)" |
2394 show "(INF i:I. f i) + (INF i:I. g i) \<le> (INF i:I. f i + g i)" |
2360 by (rule INF_greatest; intro ereal_add_mono INF_lower) |
2395 by (rule INF_greatest; intro add_mono INF_lower) |
2361 next |
2396 next |
2362 have "(INF i:I. f i + g i) \<le> (INF i:I. (INF j:I. f i + g j))" |
2397 have "(INF i:I. f i + g i) \<le> (INF i:I. (INF j:I. f i + g j))" |
2363 using directed by (intro INF_greatest) (blast intro: INF_lower2) |
2398 using directed by (intro INF_greatest) (blast intro: INF_lower2) |
2364 also have "\<dots> = (INF i:I. f i + (INF i:I. g i))" |
2399 also have "\<dots> = (INF i:I. f i + (INF i:I. g i))" |
2365 using nonneg by (intro INF_cong refl INF_ereal_add_right \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0]) |
2400 using nonneg by (intro INF_cong refl INF_ereal_add_right \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0]) |
3090 and "c \<noteq> \<infinity>" |
3125 and "c \<noteq> \<infinity>" |
3091 shows "c * (a + b) = c * a + c * b" |
3126 shows "c * (a + b) = c * a + c * b" |
3092 using assms |
3127 using assms |
3093 by (cases rule: ereal3_cases[of a b c]) |
3128 by (cases rule: ereal3_cases[of a b c]) |
3094 (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff) |
3129 (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff) |
3095 |
|
3096 lemma ereal_max_mono: "(a::ereal) \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> max a c \<le> max b d" |
|
3097 by (metis sup_ereal_def sup_mono) |
|
3098 |
|
3099 lemma ereal_max_least: "(a::ereal) \<le> x \<Longrightarrow> c \<le> x \<Longrightarrow> max a c \<le> x" |
|
3100 by (metis sup_ereal_def sup_least) |
|
3101 |
3130 |
3102 lemma ereal_LimI_finite: |
3131 lemma ereal_LimI_finite: |
3103 fixes x :: ereal |
3132 fixes x :: ereal |
3104 assumes "\<bar>x\<bar> \<noteq> \<infinity>" |
3133 assumes "\<bar>x\<bar> \<noteq> \<infinity>" |
3105 and "\<And>r. 0 < r \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r" |
3134 and "\<And>r. 0 < r \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r" |
3204 fix P let ?P' = "\<lambda>x. P x \<and> 0 \<le> f x" |
3233 fix P let ?P' = "\<lambda>x. P x \<and> 0 \<le> f x" |
3205 assume "eventually P F" |
3234 assume "eventually P F" |
3206 with ev show "eventually ?P' F" |
3235 with ev show "eventually ?P' F" |
3207 by eventually_elim auto |
3236 by eventually_elim auto |
3208 have "?INF P f + (SUP P:?F. ?INF P g) \<le> ?INF ?P' f + (SUP P:?F. ?INF P g)" |
3237 have "?INF P f + (SUP P:?F. ?INF P g) \<le> ?INF ?P' f + (SUP P:?F. ?INF P g)" |
3209 by (intro ereal_add_mono INF_mono) auto |
3238 by (intro add_mono INF_mono) auto |
3210 also have "\<dots> = (SUP P':?F. ?INF ?P' f + ?INF P' g)" |
3239 also have "\<dots> = (SUP P':?F. ?INF ?P' f + ?INF P' g)" |
3211 proof (rule SUP_ereal_add_right[symmetric]) |
3240 proof (rule SUP_ereal_add_right[symmetric]) |
3212 show "INFIMUM {x. P x \<and> 0 \<le> f x} f \<noteq> - \<infinity>" |
3241 show "INFIMUM {x. P x \<and> 0 \<le> f x} f \<noteq> - \<infinity>" |
3213 unfolding bot_ereal_def[symmetric] INF_eq_bot_iff |
3242 unfolding bot_ereal_def[symmetric] INF_eq_bot_iff |
3214 by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def) |
3243 by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def) |
3221 show "?INF P f + ?INF Q g \<le> (SUP P:?F. INF x:Collect P. f x + g x)" |
3250 show "?INF P f + ?INF Q g \<le> (SUP P:?F. INF x:Collect P. f x + g x)" |
3222 proof (rule SUP_upper2) |
3251 proof (rule SUP_upper2) |
3223 show "(\<lambda>x. P x \<and> Q x) \<in> ?F" |
3252 show "(\<lambda>x. P x \<and> Q x) \<in> ?F" |
3224 using * by (auto simp: eventually_conj) |
3253 using * by (auto simp: eventually_conj) |
3225 show "?INF P f + ?INF Q g \<le> (INF x:{x. P x \<and> Q x}. f x + g x)" |
3254 show "?INF P f + ?INF Q g \<le> (INF x:{x. P x \<and> Q x}. f x + g x)" |
3226 by (intro INF_greatest ereal_add_mono) (auto intro: INF_lower) |
3255 by (intro INF_greatest add_mono) (auto intro: INF_lower) |
3227 qed |
3256 qed |
3228 qed |
3257 qed |
3229 finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. INF x:Collect P. f x + g x)" . |
3258 finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. INF x:Collect P. f x + g x)" . |
3230 qed |
3259 qed |
3231 |
3260 |
3298 fixes f :: "nat \<Rightarrow> ereal" |
3327 fixes f :: "nat \<Rightarrow> ereal" |
3299 assumes "\<And>i. 0 \<le> f i" |
3328 assumes "\<And>i. 0 \<le> f i" |
3300 shows "f sums (SUP n. \<Sum>i<n. f i)" |
3329 shows "f sums (SUP n. \<Sum>i<n. f i)" |
3301 proof - |
3330 proof - |
3302 have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)" |
3331 have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)" |
3303 using ereal_add_mono[OF _ assms] |
3332 using add_mono[OF _ assms] |
3304 by (auto intro!: incseq_SucI) |
3333 by (auto intro!: incseq_SucI) |
3305 from LIMSEQ_SUP[OF this] |
3334 from LIMSEQ_SUP[OF this] |
3306 show ?thesis unfolding sums_def |
3335 show ?thesis unfolding sums_def |
3307 by (simp add: atLeast0LessThan) |
3336 by (simp add: atLeast0LessThan) |
3308 qed |
3337 qed |
3397 assumes "\<And>i. 0 \<le> f i" |
3426 assumes "\<And>i. 0 \<le> f i" |
3398 and "\<And>i. 0 \<le> g i" |
3427 and "\<And>i. 0 \<le> g i" |
3399 shows "(\<Sum>i. f i + g i) = suminf f + suminf g" |
3428 shows "(\<Sum>i. f i + g i) = suminf f + suminf g" |
3400 apply (subst (1 2 3) suminf_ereal_eq_SUP) |
3429 apply (subst (1 2 3) suminf_ereal_eq_SUP) |
3401 unfolding sum.distrib |
3430 unfolding sum.distrib |
3402 apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_sumI sum_nonneg ballI)+ |
3431 apply (intro assms add_nonneg_nonneg SUP_ereal_add_pos incseq_sumI sum_nonneg ballI)+ |
3403 done |
3432 done |
3404 |
3433 |
3405 lemma suminf_cmult_ereal: |
3434 lemma suminf_cmult_ereal: |
3406 fixes f g :: "nat \<Rightarrow> ereal" |
3435 fixes f g :: "nat \<Rightarrow> ereal" |
3407 assumes "\<And>i. 0 \<le> f i" |
3436 assumes "\<And>i. 0 \<le> f i" |
3654 next |
3683 next |
3655 assume "I \<noteq> {}" |
3684 assume "I \<noteq> {}" |
3656 show ?thesis |
3685 show ?thesis |
3657 proof (rule antisym) |
3686 proof (rule antisym) |
3658 show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)" |
3687 show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)" |
3659 by (rule SUP_least; intro ereal_add_mono SUP_upper) |
3688 by (rule SUP_least; intro add_mono SUP_upper) |
3660 next |
3689 next |
3661 have "bot < (SUP i:I. g i)" |
3690 have "bot < (SUP i:I. g i)" |
3662 using \<open>I \<noteq> {}\<close> nonneg(2) by (auto simp: bot_ereal_def less_SUP_iff) |
3691 using \<open>I \<noteq> {}\<close> nonneg(2) by (auto simp: bot_ereal_def less_SUP_iff) |
3663 then have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))" |
3692 then have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))" |
3664 by (intro SUP_ereal_add_left[symmetric] \<open>I \<noteq> {}\<close>) auto |
3693 by (intro SUP_ereal_add_left[symmetric] \<open>I \<noteq> {}\<close>) auto |
3686 using insert by (auto intro!: sum_nonneg nonneg) |
3715 using insert by (auto intro!: sum_nonneg nonneg) |
3687 next |
3716 next |
3688 fix i j assume "i \<in> I" "j \<in> I" |
3717 fix i j assume "i \<in> I" "j \<in> I" |
3689 from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k .. |
3718 from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k .. |
3690 then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)" |
3719 then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)" |
3691 by (intro bexI[of _ k]) (auto intro!: ereal_add_mono sum_mono) |
3720 by (intro bexI[of _ k]) (auto intro!: add_mono sum_mono) |
3692 qed |
3721 qed |
3693 ultimately show ?case |
3722 ultimately show ?case |
3694 by simp |
3723 by simp |
3695 qed (simp_all add: SUP_constant \<open>I \<noteq> {}\<close>) |
3724 qed (simp_all add: SUP_constant \<open>I \<noteq> {}\<close>) |
3696 from this[of A] show ?thesis by simp |
3725 from this[of A] show ?thesis by simp |
4102 "(c::real) \<ge> 0 \<Longrightarrow> limsup (\<lambda>n. ereal c * f n) = ereal c * limsup f" |
4131 "(c::real) \<ge> 0 \<Longrightarrow> limsup (\<lambda>n. ereal c * f n) = ereal c * limsup f" |
4103 by (subst (1 2) mult.commute, rule limsup_ereal_mult_right) simp_all |
4132 by (subst (1 2) mult.commute, rule limsup_ereal_mult_right) simp_all |
4104 |
4133 |
4105 lemma Limsup_add_ereal_right: |
4134 lemma Limsup_add_ereal_right: |
4106 "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Limsup F (\<lambda>n. g n + (c :: ereal)) = Limsup F g + c" |
4135 "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Limsup F (\<lambda>n. g n + (c :: ereal)) = Limsup F g + c" |
4107 by (rule Limsup_compose_continuous_mono) (auto simp: mono_def ereal_add_mono continuous_on_def) |
4136 by (rule Limsup_compose_continuous_mono) (auto simp: mono_def add_mono continuous_on_def) |
4108 |
4137 |
4109 lemma Limsup_add_ereal_left: |
4138 lemma Limsup_add_ereal_left: |
4110 "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Limsup F (\<lambda>n. (c :: ereal) + g n) = c + Limsup F g" |
4139 "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Limsup F (\<lambda>n. (c :: ereal) + g n) = c + Limsup F g" |
4111 by (subst (1 2) add.commute) (rule Limsup_add_ereal_right) |
4140 by (subst (1 2) add.commute) (rule Limsup_add_ereal_right) |
4112 |
4141 |
4113 lemma Liminf_add_ereal_right: |
4142 lemma Liminf_add_ereal_right: |
4114 "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Liminf F (\<lambda>n. g n + (c :: ereal)) = Liminf F g + c" |
4143 "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Liminf F (\<lambda>n. g n + (c :: ereal)) = Liminf F g + c" |
4115 by (rule Liminf_compose_continuous_mono) (auto simp: mono_def ereal_add_mono continuous_on_def) |
4144 by (rule Liminf_compose_continuous_mono) (auto simp: mono_def add_mono continuous_on_def) |
4116 |
4145 |
4117 lemma Liminf_add_ereal_left: |
4146 lemma Liminf_add_ereal_left: |
4118 "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Liminf F (\<lambda>n. (c :: ereal) + g n) = c + Liminf F g" |
4147 "F \<noteq> bot \<Longrightarrow> abs c \<noteq> \<infinity> \<Longrightarrow> Liminf F (\<lambda>n. (c :: ereal) + g n) = c + Liminf F g" |
4119 by (subst (1 2) add.commute) (rule Liminf_add_ereal_right) |
4148 by (subst (1 2) add.commute) (rule Liminf_add_ereal_right) |
4120 |
4149 |