1604 proof |
1604 proof |
1605 show "\<exists>a b::ereal. a \<noteq> b" |
1605 show "\<exists>a b::ereal. a \<noteq> b" |
1606 using zero_neq_one by blast |
1606 using zero_neq_one by blast |
1607 qed |
1607 qed |
1608 |
1608 |
|
1609 lemma ereal_Sup: |
|
1610 assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>" |
|
1611 shows "ereal (Sup A) = (SUP a:A. ereal a)" |
|
1612 proof (rule antisym) |
|
1613 obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}" |
|
1614 using * by (force simp: bot_ereal_def) |
|
1615 then have upper: "\<And>a. a \<in> A \<Longrightarrow> a \<le> r" |
|
1616 by (auto intro!: SUP_upper simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq) |
|
1617 |
|
1618 show "ereal (Sup A) \<le> (SUP a:A. ereal a)" |
|
1619 using upper by (simp add: r[symmetric] cSup_least[OF `A \<noteq> {}`]) |
|
1620 show "(SUP a:A. ereal a) \<le> ereal (Sup A)" |
|
1621 using upper `A \<noteq> {}` by (intro SUP_least) (auto intro!: cSup_upper bdd_aboveI) |
|
1622 qed |
|
1623 |
|
1624 lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))" |
|
1625 using ereal_Sup[of "f`A"] by auto |
|
1626 |
|
1627 lemma ereal_Inf: |
|
1628 assumes *: "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>" |
|
1629 shows "ereal (Inf A) = (INF a:A. ereal a)" |
|
1630 proof (rule antisym) |
|
1631 obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}" |
|
1632 using * by (force simp: top_ereal_def) |
|
1633 then have lower: "\<And>a. a \<in> A \<Longrightarrow> r \<le> a" |
|
1634 by (auto intro!: INF_lower simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq) |
|
1635 |
|
1636 show "(INF a:A. ereal a) \<le> ereal (Inf A)" |
|
1637 using lower by (simp add: r[symmetric] cInf_greatest[OF `A \<noteq> {}`]) |
|
1638 show "ereal (Inf A) \<le> (INF a:A. ereal a)" |
|
1639 using lower `A \<noteq> {}` by (intro INF_greatest) (auto intro!: cInf_lower bdd_belowI) |
|
1640 qed |
|
1641 |
|
1642 lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))" |
|
1643 using ereal_Inf[of "f`A"] by auto |
|
1644 |
1609 lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S" |
1645 lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S" |
1610 by (auto intro!: SUP_eqI |
1646 by (auto intro!: SUP_eqI |
1611 simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff |
1647 simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff |
1612 intro!: complete_lattice_class.Inf_lower2) |
1648 intro!: complete_lattice_class.Inf_lower2) |
1613 |
1649 |
1703 proof (rule Inf_less_iff[THEN iffD1]) |
1739 proof (rule Inf_less_iff[THEN iffD1]) |
1704 show "Inf X < Inf X + e" |
1740 show "Inf X < Inf X + e" |
1705 using assms by (cases e) auto |
1741 using assms by (cases e) auto |
1706 qed |
1742 qed |
1707 |
1743 |
|
1744 lemma SUP_PInfty: |
|
1745 fixes f :: "'a \<Rightarrow> ereal" |
|
1746 assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i" |
|
1747 shows "(SUP i:A. f i) = \<infinity>" |
|
1748 unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def] |
|
1749 apply simp |
|
1750 proof safe |
|
1751 fix x :: ereal |
|
1752 assume "x \<noteq> \<infinity>" |
|
1753 show "\<exists>i\<in>A. x < f i" |
|
1754 proof (cases x) |
|
1755 case PInf |
|
1756 with `x \<noteq> \<infinity>` show ?thesis |
|
1757 by simp |
|
1758 next |
|
1759 case MInf |
|
1760 with assms[of "0"] show ?thesis |
|
1761 by force |
|
1762 next |
|
1763 case (real r) |
|
1764 with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)" |
|
1765 by auto |
|
1766 moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i" |
|
1767 using assms .. |
|
1768 ultimately show ?thesis |
|
1769 by (auto intro!: bexI[of _ i]) |
|
1770 qed |
|
1771 qed |
|
1772 |
1708 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>" |
1773 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>" |
1709 proof - |
1774 by (rule SUP_PInfty) auto |
1710 { |
|
1711 fix x :: ereal |
|
1712 assume "x \<noteq> \<infinity>" |
|
1713 then have "\<exists>k::nat. x < ereal (real k)" |
|
1714 proof (cases x) |
|
1715 case MInf |
|
1716 then show ?thesis |
|
1717 by (intro exI[of _ 0]) auto |
|
1718 next |
|
1719 case (real r) |
|
1720 moreover obtain k :: nat where "r < real k" |
|
1721 using ex_less_of_nat by (auto simp: real_eq_of_nat) |
|
1722 ultimately show ?thesis |
|
1723 by auto |
|
1724 qed simp |
|
1725 } |
|
1726 then show ?thesis |
|
1727 using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. ereal (real n)"] |
|
1728 by (auto simp: top_ereal_def) |
|
1729 qed |
|
1730 |
1775 |
1731 lemma Inf_less: |
1776 lemma Inf_less: |
1732 fixes x :: ereal |
1777 fixes x :: ereal |
1733 assumes "(INF i:A. f i) < x" |
1778 assumes "(INF i:A. f i) < x" |
1734 shows "\<exists>i. i \<in> A \<and> f i \<le> x" |
1779 shows "\<exists>i. i \<in> A \<and> f i \<le> x" |
1927 |
1972 |
1928 lemma SUP_ereal_add_right: |
1973 lemma SUP_ereal_add_right: |
1929 fixes c :: ereal |
1974 fixes c :: ereal |
1930 shows "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> 0 \<le> c \<Longrightarrow> (SUP i:I. c + f i) = c + SUPREMUM I f" |
1975 shows "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> 0 \<le> c \<Longrightarrow> (SUP i:I. c + f i) = c + SUPREMUM I f" |
1931 using SUP_ereal_add_left[of I f c] by (simp add: add_ac) |
1976 using SUP_ereal_add_left[of I f c] by (simp add: add_ac) |
1932 |
|
1933 lemma SUP_PInfty: |
|
1934 fixes f :: "'a \<Rightarrow> ereal" |
|
1935 assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i" |
|
1936 shows "(SUP i:A. f i) = \<infinity>" |
|
1937 unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def] |
|
1938 apply simp |
|
1939 proof safe |
|
1940 fix x :: ereal |
|
1941 assume "x \<noteq> \<infinity>" |
|
1942 show "\<exists>i\<in>A. x < f i" |
|
1943 proof (cases x) |
|
1944 case PInf |
|
1945 with `x \<noteq> \<infinity>` show ?thesis |
|
1946 by simp |
|
1947 next |
|
1948 case MInf |
|
1949 with assms[of "0"] show ?thesis |
|
1950 by force |
|
1951 next |
|
1952 case (real r) |
|
1953 with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)" |
|
1954 by auto |
|
1955 moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i" |
|
1956 using assms .. |
|
1957 ultimately show ?thesis |
|
1958 by (auto intro!: bexI[of _ i]) |
|
1959 qed |
|
1960 qed |
|
1961 |
1977 |
1962 lemma Sup_countable_SUP: |
1978 lemma Sup_countable_SUP: |
1963 assumes "A \<noteq> {}" |
1979 assumes "A \<noteq> {}" |
1964 shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f" |
1980 shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f" |
1965 proof (cases "Sup A") |
1981 proof (cases "Sup A") |
2662 shows "c * (a + b) = c * a + c * b" |
2678 shows "c * (a + b) = c * a + c * b" |
2663 using assms |
2679 using assms |
2664 by (cases rule: ereal3_cases[of a b c]) |
2680 by (cases rule: ereal3_cases[of a b c]) |
2665 (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff) |
2681 (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff) |
2666 |
2682 |
2667 lemma ereal_pos_le_distrib: |
|
2668 fixes a b c :: ereal |
|
2669 assumes "c \<ge> 0" |
|
2670 shows "c * (a + b) \<le> c * a + c * b" |
|
2671 using assms |
|
2672 by (cases rule: ereal3_cases[of a b c]) (auto simp add: field_simps) |
|
2673 |
|
2674 lemma ereal_max_mono: "(a::ereal) \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> max a c \<le> max b d" |
2683 lemma ereal_max_mono: "(a::ereal) \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> max a c \<le> max b d" |
2675 by (metis sup_ereal_def sup_mono) |
2684 by (metis sup_ereal_def sup_mono) |
2676 |
2685 |
2677 lemma ereal_max_least: "(a::ereal) \<le> x \<Longrightarrow> c \<le> x \<Longrightarrow> max a c \<le> x" |
2686 lemma ereal_max_least: "(a::ereal) \<le> x \<Longrightarrow> c \<le> x \<Longrightarrow> max a c \<le> x" |
2678 by (metis sup_ereal_def sup_least) |
2687 by (metis sup_ereal_def sup_least) |