34 shows "continuous (at_left x) f" |
34 shows "continuous (at_left x) f" |
35 proof cases |
35 proof cases |
36 assume "x = bot" then show ?thesis |
36 assume "x = bot" then show ?thesis |
37 by (simp add: trivial_limit_at_left_bot) |
37 by (simp add: trivial_limit_at_left_bot) |
38 next |
38 next |
39 assume x: "x \<noteq> bot" |
39 assume x: "x \<noteq> bot" |
40 show ?thesis |
40 show ?thesis |
41 unfolding continuous_within |
41 unfolding continuous_within |
42 proof (intro tendsto_at_left_sequentially[of bot]) |
42 proof (intro tendsto_at_left_sequentially[of bot]) |
43 fix S :: "nat \<Rightarrow> 'a" assume S: "incseq S" and S_x: "S ----> x" |
43 fix S :: "nat \<Rightarrow> 'a" assume S: "incseq S" and S_x: "S ----> x" |
44 from S_x have x_eq: "x = (SUP i. S i)" |
44 from S_x have x_eq: "x = (SUP i. S i)" |
52 lemma sup_continuous_iff_at_left: |
52 lemma sup_continuous_iff_at_left: |
53 fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}" |
53 fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}" |
54 shows "sup_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_left x) f) \<and> mono f" |
54 shows "sup_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_left x) f) \<and> mono f" |
55 using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f] |
55 using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f] |
56 sup_continuous_mono[of f] by auto |
56 sup_continuous_mono[of f] by auto |
57 |
57 |
58 lemma continuous_at_right_imp_inf_continuous: |
58 lemma continuous_at_right_imp_inf_continuous: |
59 fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}" |
59 fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}" |
60 assumes "mono f" "\<And>x. continuous (at_right x) f" |
60 assumes "mono f" "\<And>x. continuous (at_right x) f" |
61 shows "inf_continuous f" |
61 shows "inf_continuous f" |
62 unfolding inf_continuous_def |
62 unfolding inf_continuous_def |
71 shows "continuous (at_right x) f" |
71 shows "continuous (at_right x) f" |
72 proof cases |
72 proof cases |
73 assume "x = top" then show ?thesis |
73 assume "x = top" then show ?thesis |
74 by (simp add: trivial_limit_at_right_top) |
74 by (simp add: trivial_limit_at_right_top) |
75 next |
75 next |
76 assume x: "x \<noteq> top" |
76 assume x: "x \<noteq> top" |
77 show ?thesis |
77 show ?thesis |
78 unfolding continuous_within |
78 unfolding continuous_within |
79 proof (intro tendsto_at_right_sequentially[of _ top]) |
79 proof (intro tendsto_at_right_sequentially[of _ top]) |
80 fix S :: "nat \<Rightarrow> 'a" assume S: "decseq S" and S_x: "S ----> x" |
80 fix S :: "nat \<Rightarrow> 'a" assume S: "decseq S" and S_x: "S ----> x" |
81 from S_x have x_eq: "x = (INF i. S i)" |
81 from S_x have x_eq: "x = (INF i. S i)" |
591 |
591 |
592 lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>" |
592 lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>" |
593 by (cases x) auto |
593 by (cases x) auto |
594 |
594 |
595 lemma ereal_abs_leI: |
595 lemma ereal_abs_leI: |
596 fixes x y :: ereal |
596 fixes x y :: ereal |
597 shows "\<lbrakk> x \<le> y; -x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y" |
597 shows "\<lbrakk> x \<le> y; -x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y" |
598 by(cases x y rule: ereal2_cases)(simp_all) |
598 by(cases x y rule: ereal2_cases)(simp_all) |
599 |
599 |
600 lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>" |
600 lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>" |
601 by (cases x) auto |
601 by (cases x) auto |
879 (simp_all add: zero_ereal_def zero_less_mult_iff) |
879 (simp_all add: zero_ereal_def zero_less_mult_iff) |
880 qed |
880 qed |
881 |
881 |
882 end |
882 end |
883 |
883 |
884 lemma [simp]: |
884 lemma [simp]: |
885 shows ereal_1_times: "ereal 1 * x = x" |
885 shows ereal_1_times: "ereal 1 * x = x" |
886 and times_ereal_1: "x * ereal 1 = x" |
886 and times_ereal_1: "x * ereal 1 = x" |
887 by(simp_all add: one_ereal_def[symmetric]) |
887 by(simp_all add: one_ereal_def[symmetric]) |
888 |
888 |
889 lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))" |
889 lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))" |
1032 lemma ereal_left_mult_cong: |
1032 lemma ereal_left_mult_cong: |
1033 fixes a b c :: ereal |
1033 fixes a b c :: ereal |
1034 shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * d" |
1034 shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * d" |
1035 by (cases "c = 0") simp_all |
1035 by (cases "c = 0") simp_all |
1036 |
1036 |
1037 lemma ereal_right_mult_cong: |
1037 lemma ereal_right_mult_cong: |
1038 fixes a b c :: ereal |
1038 fixes a b c :: ereal |
1039 shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = d * b" |
1039 shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = d * b" |
1040 by (cases "c = 0") simp_all |
1040 by (cases "c = 0") simp_all |
1041 |
1041 |
1042 lemma ereal_distrib: |
1042 lemma ereal_distrib: |
1400 fixes x y :: ereal |
1400 fixes x y :: ereal |
1401 shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>" |
1401 shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>" |
1402 by (cases x y rule: ereal2_cases) simp_all |
1402 by (cases x y rule: ereal2_cases) simp_all |
1403 |
1403 |
1404 lemma ereal_diff_add_eq_diff_diff_swap: |
1404 lemma ereal_diff_add_eq_diff_diff_swap: |
1405 fixes x y z :: ereal |
1405 fixes x y z :: ereal |
1406 shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - (y + z) = x - y - z" |
1406 shows "\<bar>y\<bar> \<noteq> \<infinity> \<Longrightarrow> x - (y + z) = x - y - z" |
1407 by(cases x y z rule: ereal3_cases) simp_all |
1407 by(cases x y z rule: ereal3_cases) simp_all |
1408 |
1408 |
1409 lemma ereal_diff_add_assoc2: |
1409 lemma ereal_diff_add_assoc2: |
1410 fixes x y z :: ereal |
1410 fixes x y z :: ereal |
1412 by(cases x y z rule: ereal3_cases) simp_all |
1412 by(cases x y z rule: ereal3_cases) simp_all |
1413 |
1413 |
1414 lemma ereal_add_uminus_conv_diff: fixes x y z :: ereal shows "- x + y = y - x" |
1414 lemma ereal_add_uminus_conv_diff: fixes x y z :: ereal shows "- x + y = y - x" |
1415 by(cases x y rule: ereal2_cases) simp_all |
1415 by(cases x y rule: ereal2_cases) simp_all |
1416 |
1416 |
1417 lemma ereal_minus_diff_eq: |
1417 lemma ereal_minus_diff_eq: |
1418 fixes x y :: ereal |
1418 fixes x y :: ereal |
1419 shows "\<lbrakk> x = \<infinity> \<longrightarrow> y \<noteq> \<infinity>; x = -\<infinity> \<longrightarrow> y \<noteq> - \<infinity> \<rbrakk> \<Longrightarrow> - (x - y) = y - x" |
1419 shows "\<lbrakk> x = \<infinity> \<longrightarrow> y \<noteq> \<infinity>; x = -\<infinity> \<longrightarrow> y \<noteq> - \<infinity> \<rbrakk> \<Longrightarrow> - (x - y) = y - x" |
1420 by(cases x y rule: ereal2_cases) simp_all |
1420 by(cases x y rule: ereal2_cases) simp_all |
1421 |
1421 |
1422 lemma ediff_le_self [simp]: "x - y \<le> (x :: enat)" |
1422 lemma ediff_le_self [simp]: "x - y \<le> (x :: enat)" |
1423 by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all |
1423 by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all |
1743 instance |
1743 instance |
1744 by standard (simp add: open_ereal_generated) |
1744 by standard (simp add: open_ereal_generated) |
1745 |
1745 |
1746 end |
1746 end |
1747 |
1747 |
1748 lemma continuous_on_compose': |
|
1749 "continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow> f`s \<subseteq> t \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))" |
|
1750 using continuous_on_compose[of s f g] continuous_on_subset[of t g "f`s"] by auto |
|
1751 |
|
1752 lemma continuous_on_ereal[continuous_intros]: |
1748 lemma continuous_on_ereal[continuous_intros]: |
1753 assumes f: "continuous_on s f" shows "continuous_on s (\<lambda>x. ereal (f x))" |
1749 assumes f: "continuous_on s f" shows "continuous_on s (\<lambda>x. ereal (f x))" |
1754 by (rule continuous_on_compose'[OF f continuous_onI_mono[of ereal UNIV]]) auto |
1750 by (rule continuous_on_compose2 [OF continuous_onI_mono[of ereal UNIV] f]) auto |
1755 |
1751 |
1756 lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F" |
1752 lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F" |
1757 using isCont_tendsto_compose[of x ereal f F] continuous_on_ereal[of UNIV "\<lambda>x. x"] |
1753 using isCont_tendsto_compose[of x ereal f F] continuous_on_ereal[of UNIV "\<lambda>x. x"] |
1758 by (simp add: continuous_on_eq_continuous_at) |
1754 by (simp add: continuous_on_eq_continuous_at) |
1759 |
1755 |
1805 assume "- \<infinity> < c" "c < 0" |
1801 assume "- \<infinity> < c" "c < 0" |
1806 then have "0 < - c" "- c < \<infinity>" |
1802 then have "0 < - c" "- c < \<infinity>" |
1807 by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0]) |
1803 by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0]) |
1808 then have "((\<lambda>x. (- c) * f x) ---> (- c) * x) F" |
1804 then have "((\<lambda>x. (- c) * f x) ---> (- c) * x) F" |
1809 by (rule *) |
1805 by (rule *) |
1810 from tendsto_uminus_ereal[OF this] show ?thesis |
1806 from tendsto_uminus_ereal[OF this] show ?thesis |
1811 by simp |
1807 by simp |
1812 qed (auto intro!: *) |
1808 qed (auto intro!: *) |
1813 qed |
1809 qed |
1814 |
1810 |
1815 lemma tendsto_cmult_ereal_not_0[tendsto_intros, simp, intro]: |
1811 lemma tendsto_cmult_ereal_not_0[tendsto_intros, simp, intro]: |
2117 by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"]) |
2113 by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"]) |
2118 (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close> |
2114 (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close> |
2119 intro!: ereal_mult_left_mono c) |
2115 intro!: ereal_mult_left_mono c) |
2120 qed |
2116 qed |
2121 |
2117 |
2122 lemma countable_approach: |
2118 lemma countable_approach: |
2123 fixes x :: ereal |
2119 fixes x :: ereal |
2124 assumes "x \<noteq> -\<infinity>" |
2120 assumes "x \<noteq> -\<infinity>" |
2125 shows "\<exists>f. incseq f \<and> (\<forall>i::nat. f i < x) \<and> (f ----> x)" |
2121 shows "\<exists>f. incseq f \<and> (\<forall>i::nat. f i < x) \<and> (f ----> x)" |
2126 proof (cases x) |
2122 proof (cases x) |
2127 case (real r) |
2123 case (real r) |
2128 moreover have "(\<lambda>n. r - inverse (real (Suc n))) ----> r - 0" |
2124 moreover have "(\<lambda>n. r - inverse (real (Suc n))) ----> r - 0" |
2129 by (intro tendsto_intros LIMSEQ_inverse_real_of_nat) |
2125 by (intro tendsto_intros LIMSEQ_inverse_real_of_nat) |
2130 ultimately show ?thesis |
2126 ultimately show ?thesis |
2131 by (intro exI[of _ "\<lambda>n. x - inverse (Suc n)"]) (auto simp: incseq_def) |
2127 by (intro exI[of _ "\<lambda>n. x - inverse (Suc n)"]) (auto simp: incseq_def) |
2132 next |
2128 next |
2133 case PInf with LIMSEQ_SUP[of "\<lambda>n::nat. ereal (real n)"] show ?thesis |
2129 case PInf with LIMSEQ_SUP[of "\<lambda>n::nat. ereal (real n)"] show ?thesis |
2134 by (intro exI[of _ "\<lambda>n. ereal (real n)"]) (auto simp: incseq_def SUP_nat_Infty) |
2130 by (intro exI[of _ "\<lambda>n. ereal (real n)"]) (auto simp: incseq_def SUP_nat_Infty) |
2135 qed (simp add: assms) |
2131 qed (simp add: assms) |
2136 |
2132 |
2137 lemma Sup_countable_SUP: |
2133 lemma Sup_countable_SUP: |
3273 fix i assume "i \<in> I" then show "0 \<le> f n i" "0 \<le> (\<Sum>l\<in>N. f l i)" |
3269 fix i assume "i \<in> I" then show "0 \<le> f n i" "0 \<le> (\<Sum>l\<in>N. f l i)" |
3274 using insert by (auto intro!: setsum_nonneg nonneg) |
3270 using insert by (auto intro!: setsum_nonneg nonneg) |
3275 next |
3271 next |
3276 fix i j assume "i \<in> I" "j \<in> I" |
3272 fix i j assume "i \<in> I" "j \<in> I" |
3277 from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k .. |
3273 from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k .. |
3278 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)" |
3274 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)" |
3279 by (intro bexI[of _ k]) (auto intro!: ereal_add_mono setsum_mono) |
3275 by (intro bexI[of _ k]) (auto intro!: ereal_add_mono setsum_mono) |
3280 qed |
3276 qed |
3281 ultimately show ?case |
3277 ultimately show ?case |
3282 by simp |
3278 by simp |
3283 qed (simp_all add: SUP_constant \<open>I \<noteq> {}\<close>) |
3279 qed (simp_all add: SUP_constant \<open>I \<noteq> {}\<close>) |
3473 fixes X :: "nat \<Rightarrow> real" and L :: real |
3469 fixes X :: "nat \<Rightarrow> real" and L :: real |
3474 assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X" |
3470 assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X" |
3475 shows "X ----> L" |
3471 shows "X ----> L" |
3476 proof - |
3472 proof - |
3477 from 1 2 have "limsup X \<le> liminf X" by auto |
3473 from 1 2 have "limsup X \<le> liminf X" by auto |
3478 hence 3: "limsup X = liminf X" |
3474 hence 3: "limsup X = liminf X" |
3479 apply (subst eq_iff, rule conjI) |
3475 apply (subst eq_iff, rule conjI) |
3480 by (rule Liminf_le_Limsup, auto) |
3476 by (rule Liminf_le_Limsup, auto) |
3481 hence 4: "convergent (\<lambda>n. ereal (X n))" |
3477 hence 4: "convergent (\<lambda>n. ereal (X n))" |
3482 by (subst convergent_ereal) |
3478 by (subst convergent_ereal) |
3483 hence "limsup X = lim (\<lambda>n. ereal(X n))" |
3479 hence "limsup X = lim (\<lambda>n. ereal(X n))" |
3484 by (rule convergent_limsup_cl) |
3480 by (rule convergent_limsup_cl) |
3485 also from 1 2 3 have "limsup X = L" by auto |
3481 also from 1 2 3 have "limsup X = L" by auto |
3486 finally have "lim (\<lambda>n. ereal(X n)) = L" .. |
3482 finally have "lim (\<lambda>n. ereal(X n)) = L" .. |
3487 hence "(\<lambda>n. ereal (X n)) ----> L" |
3483 hence "(\<lambda>n. ereal (X n)) ----> L" |
3488 apply (elim subst) |
3484 apply (elim subst) |
3489 by (subst convergent_LIMSEQ_iff [symmetric], rule 4) |
3485 by (subst convergent_LIMSEQ_iff [symmetric], rule 4) |
3490 thus ?thesis by simp |
3486 thus ?thesis by simp |
3491 qed |
3487 qed |
3492 |
3488 |
3493 lemma liminf_PInfty: |
3489 lemma liminf_PInfty: |
3494 fixes X :: "nat \<Rightarrow> ereal" |
3490 fixes X :: "nat \<Rightarrow> ereal" |
3640 |
3636 |
3641 lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)" |
3637 lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)" |
3642 proof - |
3638 proof - |
3643 have **: "((\<lambda>x. ereal (inverse x)) ---> ereal 0) at_infinity" |
3639 have **: "((\<lambda>x. ereal (inverse x)) ---> ereal 0) at_infinity" |
3644 by (intro tendsto_intros tendsto_inverse_0) |
3640 by (intro tendsto_intros tendsto_inverse_0) |
3645 |
3641 |
3646 show ?thesis |
3642 show ?thesis |
3647 by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def) |
3643 by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def) |
3648 (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity |
3644 (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity |
3649 intro!: filterlim_mono_eventually[OF **]) |
3645 intro!: filterlim_mono_eventually[OF **]) |
3650 qed |
3646 qed |
3651 |
3647 |
3652 lemma inverse_ereal_tendsto_pos: |
3648 lemma inverse_ereal_tendsto_pos: |
3653 fixes x :: ereal assumes "0 < x" |
3649 fixes x :: ereal assumes "0 < x" |
3654 shows "inverse -- x --> inverse x" |
3650 shows "inverse -- x --> inverse x" |
3655 proof (cases x) |
3651 proof (cases x) |
3656 case (real r) |
3652 case (real r) |
3657 with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)" |
3653 with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)" |