1980 definition integrable_on (infixr "integrable'_on" 46) |
1980 definition integrable_on (infixr "integrable'_on" 46) |
1981 where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)" |
1981 where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)" |
1982 |
1982 |
1983 definition "integral i f = (SOME y. (f has_integral y) i)" |
1983 definition "integral i f = (SOME y. (f has_integral y) i)" |
1984 |
1984 |
1985 lemma integrable_integral[dest]: |
1985 lemma integrable_integral[dest]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i" |
1986 "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i" |
1986 unfolding integrable_on_def integral_def by (rule someI_ex) |
1987 unfolding integrable_on_def integral_def by(rule someI_ex) |
|
1988 |
1987 |
1989 lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s" |
1988 lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s" |
1990 unfolding integrable_on_def by auto |
1989 unfolding integrable_on_def by auto |
1991 |
1990 |
1992 lemma has_integral_integral:"f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s" |
1991 lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s" |
1993 by auto |
1992 by auto |
1994 |
1993 |
1995 lemma setsum_content_null: |
1994 lemma setsum_content_null: |
1996 assumes "content({a..b}) = 0" "p tagged_division_of {a..b}" |
1995 assumes "content {a..b} = 0" |
|
1996 and "p tagged_division_of {a..b}" |
1997 shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)" |
1997 shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)" |
1998 proof(rule setsum_0',rule) fix y assume y:"y\<in>p" |
1998 proof (rule setsum_0', rule) |
1999 obtain x k where xk:"y = (x,k)" using surj_pair[of y] by blast |
1999 fix y |
|
2000 assume y: "y \<in> p" |
|
2001 obtain x k where xk: "y = (x, k)" |
|
2002 using surj_pair[of y] by blast |
2000 note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]] |
2003 note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]] |
2001 from this(2) guess c .. then guess d .. note c_d=this |
2004 from this(2) obtain c d where k: "k = {c..d}" by blast |
2002 have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x" unfolding xk by auto |
2005 have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x" |
2003 also have "\<dots> = 0" using content_subset[OF assm(1)[unfolded c_d]] content_pos_le[of c d] |
2006 unfolding xk by auto |
2004 unfolding assms(1) c_d by auto |
2007 also have "\<dots> = 0" |
|
2008 using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d] |
|
2009 unfolding assms(1) k |
|
2010 by auto |
2005 finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" . |
2011 finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" . |
2006 qed |
2012 qed |
2007 |
2013 |
|
2014 |
2008 subsection {* Some basic combining lemmas. *} |
2015 subsection {* Some basic combining lemmas. *} |
2009 |
2016 |
2010 lemma tagged_division_unions_exists: |
2017 lemma tagged_division_unions_exists: |
2011 assumes "finite iset" "\<forall>i \<in> iset. \<exists>p. p tagged_division_of i \<and> d fine p" |
2018 assumes "finite iset" |
2012 "\<forall>i1\<in>iset. \<forall>i2\<in>iset. ~(i1 = i2) \<longrightarrow> (interior(i1) \<inter> interior(i2) = {})" "(\<Union>iset = i)" |
2019 and "\<forall>i\<in>iset. \<exists>p. p tagged_division_of i \<and> d fine p" |
2013 obtains p where "p tagged_division_of i" "d fine p" |
2020 and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}" |
2014 proof- guess pfn using bchoice[OF assms(2)] .. note pfn = conjunctD2[OF this[rule_format]] |
2021 and "\<Union>iset = i" |
2015 show thesis apply(rule_tac p="\<Union>(pfn ` iset)" in that) unfolding assms(4)[symmetric] |
2022 obtains p where "p tagged_division_of i" and "d fine p" |
2016 apply(rule tagged_division_unions[OF assms(1) _ assms(3)]) defer |
2023 proof - |
2017 apply(rule fine_unions) using pfn by auto |
2024 obtain pfn where pfn: |
|
2025 "\<And>x. x \<in> iset \<Longrightarrow> pfn x tagged_division_of x" |
|
2026 "\<And>x. x \<in> iset \<Longrightarrow> d fine pfn x" |
|
2027 using bchoice[OF assms(2)] by auto |
|
2028 show thesis |
|
2029 apply (rule_tac p="\<Union>(pfn ` iset)" in that) |
|
2030 unfolding assms(4)[symmetric] |
|
2031 apply (rule tagged_division_unions[OF assms(1) _ assms(3)]) |
|
2032 defer |
|
2033 apply (rule fine_unions) |
|
2034 using pfn |
|
2035 apply auto |
|
2036 done |
2018 qed |
2037 qed |
2019 |
2038 |
|
2039 |
2020 subsection {* The set we're concerned with must be closed. *} |
2040 subsection {* The set we're concerned with must be closed. *} |
2021 |
2041 |
2022 lemma division_of_closed: "s division_of i \<Longrightarrow> closed (i::('n::ordered_euclidean_space) set)" |
2042 lemma division_of_closed: |
|
2043 fixes i :: "'n::ordered_euclidean_space set" |
|
2044 shows "s division_of i \<Longrightarrow> closed i" |
2023 unfolding division_of_def by fastforce |
2045 unfolding division_of_def by fastforce |
2024 |
2046 |
2025 subsection {* General bisection principle for intervals; might be useful elsewhere. *} |
2047 subsection {* General bisection principle for intervals; might be useful elsewhere. *} |
2026 |
2048 |
2027 lemma interval_bisection_step: fixes type::"'a::ordered_euclidean_space" |
2049 lemma interval_bisection_step: |
2028 assumes "P {}" "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))" "~(P {a..b::'a})" |
2050 fixes type :: "'a::ordered_euclidean_space" |
2029 obtains c d where "~(P{c..d})" |
2051 assumes "P {}" |
2030 "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i" |
2052 and "\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P (s \<union> t)" |
2031 proof- have "{a..b} \<noteq> {}" using assms(1,3) by auto |
2053 and "\<not> P {a..b::'a}" |
2032 then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" by (auto simp: interval_eq_empty not_le) |
2054 obtains c d where "\<not> P{c..d}" |
2033 { fix f have "finite f \<Longrightarrow> |
2055 and "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i" |
2034 (\<forall>s\<in>f. P s) \<Longrightarrow> |
2056 proof - |
2035 (\<forall>s\<in>f. \<exists>a b. s = {a..b}) \<Longrightarrow> |
2057 have "{a..b} \<noteq> {}" |
2036 (\<forall>s\<in>f.\<forall>t\<in>f. ~(s = t) \<longrightarrow> interior(s) \<inter> interior(t) = {}) \<Longrightarrow> P(\<Union>f)" |
2058 using assms(1,3) by auto |
2037 proof(induct f rule:finite_induct) |
2059 then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
2038 case empty show ?case using assms(1) by auto |
2060 by (auto simp: interval_eq_empty not_le) |
2039 next case (insert x f) show ?case unfolding Union_insert apply(rule assms(2)[rule_format]) |
2061 { |
2040 apply rule defer apply rule defer apply(rule inter_interior_unions_intervals) |
2062 fix f |
2041 using insert by auto |
2063 have "finite f \<Longrightarrow> |
2042 qed } note * = this |
2064 \<forall>s\<in>f. P s \<Longrightarrow> |
2043 let ?A = "{{c..d} | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or> (c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}" |
2065 \<forall>s\<in>f. \<exists>a b. s = {a..b} \<Longrightarrow> |
|
2066 \<forall>s\<in>f.\<forall>t\<in>f. s \<noteq> t \<longrightarrow> interior s \<inter> interior t = {} \<Longrightarrow> P (\<Union>f)" |
|
2067 proof (induct f rule: finite_induct) |
|
2068 case empty |
|
2069 show ?case |
|
2070 using assms(1) by auto |
|
2071 next |
|
2072 case (insert x f) |
|
2073 show ?case |
|
2074 unfolding Union_insert |
|
2075 apply (rule assms(2)[rule_format]) |
|
2076 apply rule |
|
2077 defer |
|
2078 apply rule |
|
2079 defer |
|
2080 apply (rule inter_interior_unions_intervals) |
|
2081 using insert |
|
2082 apply auto |
|
2083 done |
|
2084 qed |
|
2085 } note * = this |
|
2086 let ?A = "{{c..d} | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or> |
|
2087 (c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}" |
2044 let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i" |
2088 let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i" |
2045 { presume "\<forall>c d. ?PP c d \<longrightarrow> P {c..d} \<Longrightarrow> False" |
2089 { |
2046 thus thesis unfolding atomize_not not_all apply-apply(erule exE)+ apply(rule_tac c=x and d=xa in that) by auto } |
2090 presume "\<forall>c d. ?PP c d \<longrightarrow> P {c..d} \<Longrightarrow> False" |
2047 assume as:"\<forall>c d. ?PP c d \<longrightarrow> P {c..d}" |
2091 then show thesis |
2048 have "P (\<Union> ?A)" proof(rule *, rule_tac[2-] ballI, rule_tac[4] ballI, rule_tac[4] impI) |
2092 unfolding atomize_not not_all |
|
2093 apply - |
|
2094 apply (erule exE)+ |
|
2095 apply (rule_tac c=x and d=xa in that) |
|
2096 apply auto |
|
2097 done |
|
2098 } |
|
2099 assume as: "\<forall>c d. ?PP c d \<longrightarrow> P {c..d}" |
|
2100 have "P (\<Union> ?A)" |
|
2101 apply (rule *) |
|
2102 apply (rule_tac[2-] ballI) |
|
2103 apply (rule_tac[4] ballI) |
|
2104 apply (rule_tac[4] impI) |
|
2105 proof - |
2049 let ?B = "(\<lambda>s.{(\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i)::'a .. |
2106 let ?B = "(\<lambda>s.{(\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i)::'a .. |
2050 (\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)}) ` {s. s \<subseteq> Basis}" |
2107 (\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)}) ` {s. s \<subseteq> Basis}" |
2051 have "?A \<subseteq> ?B" proof case goal1 |
2108 have "?A \<subseteq> ?B" |
2052 then guess c unfolding mem_Collect_eq .. then guess d apply- by(erule exE,(erule conjE)+) note c_d=this[rule_format] |
2109 proof |
2053 have *:"\<And>a b c d. a = c \<Longrightarrow> b = d \<Longrightarrow> {a..b} = {c..d}" by auto |
2110 case goal1 |
2054 show "x\<in>?B" unfolding image_iff |
2111 then obtain c d where x: "x = {c..d}" |
2055 apply(rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in bexI) |
2112 "\<And>i. i \<in> Basis \<Longrightarrow> |
2056 unfolding c_d |
2113 c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or> |
2057 apply(rule *) |
2114 c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast |
|
2115 have *: "\<And>a b c d. a = c \<Longrightarrow> b = d \<Longrightarrow> {a..b} = {c..d}" |
|
2116 by auto |
|
2117 show "x \<in> ?B" |
|
2118 unfolding image_iff |
|
2119 apply (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in bexI) |
|
2120 unfolding x |
|
2121 apply (rule *) |
2058 apply (simp_all only: euclidean_eq_iff[where 'a='a] inner_setsum_left_Basis mem_Collect_eq simp_thms |
2122 apply (simp_all only: euclidean_eq_iff[where 'a='a] inner_setsum_left_Basis mem_Collect_eq simp_thms |
2059 cong: ball_cong) |
2123 cong: ball_cong) |
2060 apply safe |
2124 apply safe |
2061 proof- |
2125 proof - |
2062 fix i :: 'a assume i: "i\<in>Basis" |
2126 fix i :: 'a |
2063 thus " c \<bullet> i = (if c \<bullet> i = a \<bullet> i then a \<bullet> i else (a \<bullet> i + b \<bullet> i) / 2)" |
2127 assume i: "i \<in> Basis" |
2064 "d \<bullet> i = (if c \<bullet> i = a \<bullet> i then (a \<bullet> i + b \<bullet> i) / 2 else b \<bullet> i)" |
2128 then show "c \<bullet> i = (if c \<bullet> i = a \<bullet> i then a \<bullet> i else (a \<bullet> i + b \<bullet> i) / 2)" |
2065 using c_d(2)[of i] ab[OF i] by(auto simp add:field_simps) |
2129 and "d \<bullet> i = (if c \<bullet> i = a \<bullet> i then (a \<bullet> i + b \<bullet> i) / 2 else b \<bullet> i)" |
2066 qed qed |
2130 using x(2)[of i] ab[OF i] by (auto simp add:field_simps) |
2067 thus "finite ?A" apply(rule finite_subset) by auto |
2131 qed |
2068 fix s assume "s\<in>?A" then guess c unfolding mem_Collect_eq .. then guess d apply- by(erule exE,(erule conjE)+) |
2132 qed |
2069 note c_d=this[rule_format] |
2133 then show "finite ?A" |
2070 show "P s" unfolding c_d apply(rule as[rule_format]) proof- case goal1 thus ?case |
2134 by (rule finite_subset) auto |
2071 using c_d(2)[of i] using ab[OF `i \<in> Basis`] by auto qed |
2135 fix s |
2072 show "\<exists>a b. s = {a..b}" unfolding c_d by auto |
2136 assume "s \<in> ?A" |
2073 fix t assume "t\<in>?A" then guess e unfolding mem_Collect_eq .. then guess f apply- by(erule exE,(erule conjE)+) |
2137 then obtain c d where s: |
2074 note e_f=this[rule_format] |
2138 "s = {c..d}" |
2075 assume "s \<noteq> t" hence "\<not> (c = e \<and> d = f)" unfolding c_d e_f by auto |
2139 "\<And>i. i \<in> Basis \<Longrightarrow> |
2076 then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i':"i\<in>Basis" |
2140 c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or> |
|
2141 c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" |
|
2142 by blast |
|
2143 show "P s" |
|
2144 unfolding s |
|
2145 apply (rule as[rule_format]) |
|
2146 proof - |
|
2147 case goal1 |
|
2148 then show ?case |
|
2149 using s(2)[of i] using ab[OF `i \<in> Basis`] by auto |
|
2150 qed |
|
2151 show "\<exists>a b. s = {a..b}" |
|
2152 unfolding s by auto |
|
2153 fix t |
|
2154 assume "t \<in> ?A" |
|
2155 then obtain e f where t: |
|
2156 "t = {e..f}" |
|
2157 "\<And>i. i \<in> Basis \<Longrightarrow> |
|
2158 e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or> |
|
2159 e \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> f \<bullet> i = b \<bullet> i" |
|
2160 by blast |
|
2161 assume "s \<noteq> t" |
|
2162 then have "\<not> (c = e \<and> d = f)" |
|
2163 unfolding s t by auto |
|
2164 then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis" |
2077 unfolding euclidean_eq_iff[where 'a='a] by auto |
2165 unfolding euclidean_eq_iff[where 'a='a] by auto |
2078 hence i:"c\<bullet>i \<noteq> e\<bullet>i" "d\<bullet>i \<noteq> f\<bullet>i" apply- apply(erule_tac[!] disjE) |
2166 then have i: "c\<bullet>i \<noteq> e\<bullet>i" "d\<bullet>i \<noteq> f\<bullet>i" |
2079 proof- assume "c\<bullet>i \<noteq> e\<bullet>i" thus "d\<bullet>i \<noteq> f\<bullet>i" using c_d(2)[OF i'] e_f(2)[OF i'] by fastforce |
2167 apply - |
2080 next assume "d\<bullet>i \<noteq> f\<bullet>i" thus "c\<bullet>i \<noteq> e\<bullet>i" using c_d(2)[OF i'] e_f(2)[OF i'] by fastforce |
2168 apply(erule_tac[!] disjE) |
2081 qed have *:"\<And>s t. (\<And>a. a\<in>s \<Longrightarrow> a\<in>t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}" by auto |
2169 proof - |
2082 show "interior s \<inter> interior t = {}" unfolding e_f c_d interior_closed_interval proof(rule *) |
2170 assume "c\<bullet>i \<noteq> e\<bullet>i" |
2083 fix x assume "x\<in>{c<..<d}" "x\<in>{e<..<f}" |
2171 then show "d\<bullet>i \<noteq> f\<bullet>i" |
2084 hence x:"c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i" unfolding mem_interval using i' |
2172 using s(2)[OF i'] t(2)[OF i'] by fastforce |
2085 apply-apply(erule_tac[!] x=i in ballE)+ by auto |
2173 next |
2086 show False using c_d(2)[OF i'] apply- apply(erule_tac disjE) |
2174 assume "d\<bullet>i \<noteq> f\<bullet>i" |
2087 proof(erule_tac[!] conjE) assume as:"c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" |
2175 then show "c\<bullet>i \<noteq> e\<bullet>i" |
2088 show False using e_f(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps) |
2176 using s(2)[OF i'] t(2)[OF i'] by fastforce |
2089 next assume as:"c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" "d \<bullet> i = b \<bullet> i" |
2177 qed |
2090 show False using e_f(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps) |
2178 have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}" |
2091 qed qed qed |
2179 by auto |
2092 also have "\<Union> ?A = {a..b}" proof(rule set_eqI,rule) |
2180 show "interior s \<inter> interior t = {}" |
2093 fix x assume "x\<in>\<Union>?A" then guess Y unfolding Union_iff .. |
2181 unfolding s t interior_closed_interval |
2094 from this(1) guess c unfolding mem_Collect_eq .. then guess d .. |
2182 proof (rule *) |
2095 note c_d = this[THEN conjunct2,rule_format] `x\<in>Y`[unfolded this[THEN conjunct1]] |
2183 fix x |
2096 show "x\<in>{a..b}" unfolding mem_interval proof safe |
2184 assume "x \<in> {c<..<d}" "x \<in> {e<..<f}" |
2097 fix i :: 'a assume i: "i\<in>Basis" thus "a \<bullet> i \<le> x \<bullet> i" "x \<bullet> i \<le> b \<bullet> i" |
2185 then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i" |
2098 using c_d(1)[OF i] c_d(2)[unfolded mem_interval,THEN bspec, OF i] by auto qed |
2186 unfolding mem_interval using i' |
2099 next fix x assume x:"x\<in>{a..b}" |
2187 apply - |
2100 have "\<forall>i\<in>Basis. \<exists>c d. (c = a\<bullet>i \<and> d = (a\<bullet>i + b\<bullet>i) / 2 \<or> c = (a\<bullet>i + b\<bullet>i) / 2 \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d" |
2188 apply (erule_tac[!] x=i in ballE)+ |
2101 (is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d") unfolding mem_interval |
2189 apply auto |
|
2190 done |
|
2191 show False |
|
2192 using s(2)[OF i'] |
|
2193 apply - |
|
2194 apply (erule_tac disjE) |
|
2195 apply (erule_tac[!] conjE) |
|
2196 proof - |
|
2197 assume as: "c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" |
|
2198 show False |
|
2199 using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps) |
|
2200 next |
|
2201 assume as: "c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" "d \<bullet> i = b \<bullet> i" |
|
2202 show False |
|
2203 using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps) |
|
2204 qed |
|
2205 qed |
|
2206 qed |
|
2207 also have "\<Union> ?A = {a..b}" |
|
2208 proof (rule set_eqI,rule) |
|
2209 fix x |
|
2210 assume "x \<in> \<Union>?A" |
|
2211 then obtain c d where x: |
|
2212 "x \<in> {c..d}" |
|
2213 "\<And>i. i \<in> Basis \<Longrightarrow> |
|
2214 c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or> |
|
2215 c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast |
|
2216 show "x\<in>{a..b}" |
|
2217 unfolding mem_interval |
|
2218 proof safe |
|
2219 fix i :: 'a |
|
2220 assume i: "i \<in> Basis" |
|
2221 then show "a \<bullet> i \<le> x \<bullet> i" "x \<bullet> i \<le> b \<bullet> i" |
|
2222 using x(2)[OF i] x(1)[unfolded mem_interval,THEN bspec, OF i] by auto |
|
2223 qed |
|
2224 next |
|
2225 fix x |
|
2226 assume x: "x \<in> {a..b}" |
|
2227 have "\<forall>i\<in>Basis. |
|
2228 \<exists>c d. (c = a\<bullet>i \<and> d = (a\<bullet>i + b\<bullet>i) / 2 \<or> c = (a\<bullet>i + b\<bullet>i) / 2 \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d" |
|
2229 (is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d") |
|
2230 unfolding mem_interval |
2102 proof |
2231 proof |
2103 fix i :: 'a assume i: "i \<in> Basis" |
2232 fix i :: 'a |
|
2233 assume i: "i \<in> Basis" |
2104 have "?P i (a\<bullet>i) ((a \<bullet> i + b \<bullet> i) / 2) \<or> ?P i ((a \<bullet> i + b \<bullet> i) / 2) (b\<bullet>i)" |
2234 have "?P i (a\<bullet>i) ((a \<bullet> i + b \<bullet> i) / 2) \<or> ?P i ((a \<bullet> i + b \<bullet> i) / 2) (b\<bullet>i)" |
2105 using x[unfolded mem_interval,THEN bspec, OF i] by auto thus "\<exists>c d. ?P i c d" by blast |
2235 using x[unfolded mem_interval,THEN bspec, OF i] by auto |
|
2236 then show "\<exists>c d. ?P i c d" |
|
2237 by blast |
2106 qed |
2238 qed |
2107 thus "x\<in>\<Union>?A" |
2239 then show "x\<in>\<Union>?A" |
2108 unfolding Union_iff Bex_def mem_Collect_eq choice_Basis_iff |
2240 unfolding Union_iff Bex_def mem_Collect_eq choice_Basis_iff |
2109 apply-apply(erule exE)+ apply(rule_tac x="{xa..xaa}" in exI) unfolding mem_interval by auto |
2241 apply - |
2110 qed finally show False using assms by auto qed |
2242 apply (erule exE)+ |
2111 |
2243 apply (rule_tac x="{xa..xaa}" in exI) |
2112 lemma interval_bisection: fixes type::"'a::ordered_euclidean_space" |
2244 unfolding mem_interval |
2113 assumes "P {}" "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))" "\<not> P {a..b::'a}" |
2245 apply auto |
2114 obtains x where "x \<in> {a..b}" "\<forall>e>0. \<exists>c d. x \<in> {c..d} \<and> {c..d} \<subseteq> ball x e \<and> {c..d} \<subseteq> {a..b} \<and> ~P({c..d})" |
2246 done |
2115 proof- |
2247 qed |
|
2248 finally show False |
|
2249 using assms by auto |
|
2250 qed |
|
2251 |
|
2252 lemma interval_bisection: |
|
2253 fixes type :: "'a::ordered_euclidean_space" |
|
2254 assumes "P {}" |
|
2255 and "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))" |
|
2256 and "\<not> P {a..b::'a}" |
|
2257 obtains x where "x \<in> {a..b}" |
|
2258 and "\<forall>e>0. \<exists>c d. x \<in> {c..d} \<and> {c..d} \<subseteq> ball x e \<and> {c..d} \<subseteq> {a..b} \<and> \<not> P {c..d}" |
|
2259 proof - |
2116 have "\<forall>x. \<exists>y. \<not> P {fst x..snd x} \<longrightarrow> (\<not> P {fst y..snd y} \<and> |
2260 have "\<forall>x. \<exists>y. \<not> P {fst x..snd x} \<longrightarrow> (\<not> P {fst y..snd y} \<and> |
2117 (\<forall>i\<in>Basis. fst x\<bullet>i \<le> fst y\<bullet>i \<and> fst y\<bullet>i \<le> snd y\<bullet>i \<and> snd y\<bullet>i \<le> snd x\<bullet>i \<and> |
2261 (\<forall>i\<in>Basis. fst x\<bullet>i \<le> fst y\<bullet>i \<and> fst y\<bullet>i \<le> snd y\<bullet>i \<and> snd y\<bullet>i \<le> snd x\<bullet>i \<and> |
2118 2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))" proof case goal1 thus ?case proof- |
2262 2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))" |
|
2263 proof |
|
2264 case goal1 |
|
2265 then show ?case |
|
2266 proof - |
2119 presume "\<not> P {fst x..snd x} \<Longrightarrow> ?thesis" |
2267 presume "\<not> P {fst x..snd x} \<Longrightarrow> ?thesis" |
2120 thus ?thesis apply(cases "P {fst x..snd x}") by auto |
2268 then show ?thesis by (cases "P {fst x..snd x}") auto |
2121 next assume as:"\<not> P {fst x..snd x}" from interval_bisection_step[of P, OF assms(1-2) as] guess c d . |
2269 next |
2122 thus ?thesis apply- apply(rule_tac x="(c,d)" in exI) by auto |
2270 assume as: "\<not> P {fst x..snd x}" |
2123 qed qed then guess f apply-apply(drule choice) by(erule exE) note f=this |
2271 obtain c d where "\<not> P {c..d}" |
2124 def AB \<equiv> "\<lambda>n. (f ^^ n) (a,b)" def A \<equiv> "\<lambda>n. fst(AB n)" and B \<equiv> "\<lambda>n. snd(AB n)" note ab_def = this AB_def |
2272 "\<forall>i\<in>Basis. |
|
2273 fst x \<bullet> i \<le> c \<bullet> i \<and> |
|
2274 c \<bullet> i \<le> d \<bullet> i \<and> |
|
2275 d \<bullet> i \<le> snd x \<bullet> i \<and> |
|
2276 2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i" |
|
2277 by (rule interval_bisection_step[of P, OF assms(1-2) as]) |
|
2278 then show ?thesis |
|
2279 apply - |
|
2280 apply (rule_tac x="(c,d)" in exI) |
|
2281 apply auto |
|
2282 done |
|
2283 qed |
|
2284 qed |
|
2285 then guess f |
|
2286 apply - |
|
2287 apply (drule choice) |
|
2288 apply (erule exE) |
|
2289 done |
|
2290 note f = this |
|
2291 def AB \<equiv> "\<lambda>n. (f ^^ n) (a,b)" |
|
2292 def A \<equiv> "\<lambda>n. fst(AB n)" |
|
2293 def B \<equiv> "\<lambda>n. snd(AB n)" |
|
2294 note ab_def = A_def B_def AB_def |
2125 have "A 0 = a" "B 0 = b" "\<And>n. \<not> P {A(Suc n)..B(Suc n)} \<and> |
2295 have "A 0 = a" "B 0 = b" "\<And>n. \<not> P {A(Suc n)..B(Suc n)} \<and> |
2126 (\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and> |
2296 (\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and> |
2127 2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i)" (is "\<And>n. ?P n") |
2297 2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i)" (is "\<And>n. ?P n") |
2128 proof- show "A 0 = a" "B 0 = b" unfolding ab_def by auto |
2298 proof - |
2129 case goal3 note S = ab_def funpow.simps o_def id_apply show ?case |
2299 show "A 0 = a" "B 0 = b" |
2130 proof(induct n) case 0 thus ?case unfolding S apply(rule f[rule_format]) using assms(3) by auto |
2300 unfolding ab_def by auto |
2131 next case (Suc n) show ?case unfolding S apply(rule f[rule_format]) using Suc unfolding S by auto |
2301 case goal3 |
2132 qed qed note AB = this(1-2) conjunctD2[OF this(3),rule_format] |
2302 note S = ab_def funpow.simps o_def id_apply |
2133 |
2303 show ?case |
2134 have interv:"\<And>e. 0 < e \<Longrightarrow> \<exists>n. \<forall>x\<in>{A n..B n}. \<forall>y\<in>{A n..B n}. dist x y < e" |
2304 proof (induct n) |
2135 proof- case goal1 guess n using real_arch_pow2[of "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] .. note n=this |
2305 case 0 |
2136 show ?case apply(rule_tac x=n in exI) proof(rule,rule) |
2306 then show ?case |
2137 fix x y assume xy:"x\<in>{A n..B n}" "y\<in>{A n..B n}" |
2307 unfolding S |
2138 have "dist x y \<le> setsum (\<lambda>i. abs((x - y)\<bullet>i)) Basis" unfolding dist_norm by(rule norm_le_l1) |
2308 apply (rule f[rule_format]) using assms(3) |
|
2309 apply auto |
|
2310 done |
|
2311 next |
|
2312 case (Suc n) |
|
2313 show ?case |
|
2314 unfolding S |
|
2315 apply (rule f[rule_format]) |
|
2316 using Suc |
|
2317 unfolding S |
|
2318 apply auto |
|
2319 done |
|
2320 qed |
|
2321 qed |
|
2322 note AB = this(1-2) conjunctD2[OF this(3),rule_format] |
|
2323 |
|
2324 have interv: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. \<forall>x\<in>{A n..B n}. \<forall>y\<in>{A n..B n}. dist x y < e" |
|
2325 proof - |
|
2326 case goal1 |
|
2327 obtain n where n: "(\<Sum>i\<in>Basis. b \<bullet> i - a \<bullet> i) / e < 2 ^ n" |
|
2328 using real_arch_pow2[of "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] .. |
|
2329 show ?case |
|
2330 apply (rule_tac x=n in exI) |
|
2331 apply rule |
|
2332 apply rule |
|
2333 proof - |
|
2334 fix x y |
|
2335 assume xy: "x\<in>{A n..B n}" "y\<in>{A n..B n}" |
|
2336 have "dist x y \<le> setsum (\<lambda>i. abs((x - y)\<bullet>i)) Basis" |
|
2337 unfolding dist_norm by(rule norm_le_l1) |
2139 also have "\<dots> \<le> setsum (\<lambda>i. B n\<bullet>i - A n\<bullet>i) Basis" |
2338 also have "\<dots> \<le> setsum (\<lambda>i. B n\<bullet>i - A n\<bullet>i) Basis" |
2140 proof(rule setsum_mono) |
2339 proof (rule setsum_mono) |
2141 fix i :: 'a assume i: "i \<in> Basis" show "\<bar>(x - y) \<bullet> i\<bar> \<le> B n \<bullet> i - A n \<bullet> i" |
2340 fix i :: 'a |
2142 using xy[unfolded mem_interval,THEN bspec, OF i] by (auto simp: inner_diff_left) qed |
2341 assume i: "i \<in> Basis" |
2143 also have "\<dots> \<le> setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis / 2^n" unfolding setsum_divide_distrib |
2342 show "\<bar>(x - y) \<bullet> i\<bar> \<le> B n \<bullet> i - A n \<bullet> i" |
2144 proof(rule setsum_mono) case goal1 thus ?case |
2343 using xy[unfolded mem_interval,THEN bspec, OF i] |
2145 proof(induct n) case 0 thus ?case unfolding AB by auto |
2344 by (auto simp: inner_diff_left) |
2146 next case (Suc n) have "B (Suc n) \<bullet> i - A (Suc n) \<bullet> i \<le> (B n \<bullet> i - A n \<bullet> i) / 2" |
2345 qed |
|
2346 also have "\<dots> \<le> setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis / 2^n" |
|
2347 unfolding setsum_divide_distrib |
|
2348 proof (rule setsum_mono) |
|
2349 case goal1 |
|
2350 then show ?case |
|
2351 proof (induct n) |
|
2352 case 0 |
|
2353 then show ?case |
|
2354 unfolding AB by auto |
|
2355 next |
|
2356 case (Suc n) |
|
2357 have "B (Suc n) \<bullet> i - A (Suc n) \<bullet> i \<le> (B n \<bullet> i - A n \<bullet> i) / 2" |
2147 using AB(4)[of i n] using goal1 by auto |
2358 using AB(4)[of i n] using goal1 by auto |
2148 also have "\<dots> \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ Suc n" using Suc by(auto simp add:field_simps) finally show ?case . |
2359 also have "\<dots> \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ Suc n" |
2149 qed qed |
2360 using Suc by (auto simp add:field_simps) |
2150 also have "\<dots> < e" using n using goal1 by(auto simp add:field_simps) finally show "dist x y < e" . |
2361 finally show ?case . |
2151 qed qed |
2362 qed |
2152 { fix n m :: nat assume "m \<le> n" then have "{A n..B n} \<subseteq> {A m..B m}" |
2363 qed |
2153 proof(induct rule: inc_induct) |
2364 also have "\<dots> < e" |
2154 case (step i) show ?case |
2365 using n using goal1 by (auto simp add:field_simps) |
|
2366 finally show "dist x y < e" . |
|
2367 qed |
|
2368 qed |
|
2369 { |
|
2370 fix n m :: nat |
|
2371 assume "m \<le> n" |
|
2372 then have "{A n..B n} \<subseteq> {A m..B m}" |
|
2373 proof (induct rule: inc_induct) |
|
2374 case (step i) |
|
2375 show ?case |
2155 using AB(4) by (intro order_trans[OF step(2)] subset_interval_imp) auto |
2376 using AB(4) by (intro order_trans[OF step(2)] subset_interval_imp) auto |
2156 qed simp } note ABsubset = this |
2377 qed simp |
2157 have "\<exists>a. \<forall>n. a\<in>{A n..B n}" apply(rule decreasing_closed_nest[rule_format,OF closed_interval _ ABsubset interv]) |
2378 } note ABsubset = this |
2158 proof- fix n show "{A n..B n} \<noteq> {}" apply(cases "0<n") using AB(3)[of "n - 1"] assms(1,3) AB(1-2) by auto qed auto |
2379 have "\<exists>a. \<forall>n. a\<in>{A n..B n}" |
2159 then guess x0 .. note x0=this[rule_format] |
2380 apply (rule decreasing_closed_nest[rule_format,OF closed_interval _ ABsubset interv]) |
2160 show thesis proof(rule that[rule_format,of x0]) |
2381 proof - |
2161 show "x0\<in>{a..b}" using x0[of 0] unfolding AB . |
2382 fix n |
2162 fix e assume "0 < (e::real)" from interv[OF this] guess n .. note n=this |
2383 show "{A n..B n} \<noteq> {}" |
|
2384 apply (cases "0 < n") |
|
2385 using AB(3)[of "n - 1"] assms(1,3) AB(1-2) |
|
2386 apply auto |
|
2387 done |
|
2388 qed auto |
|
2389 then obtain x0 where x0: "\<And>n. x0 \<in> {A n..B n}" |
|
2390 by blast |
|
2391 show thesis |
|
2392 proof (rule that[rule_format, of x0]) |
|
2393 show "x0\<in>{a..b}" |
|
2394 using x0[of 0] unfolding AB . |
|
2395 fix e :: real |
|
2396 assume "e > 0" |
|
2397 from interv[OF this] obtain n |
|
2398 where n: "\<forall>x\<in>{A n..B n}. \<forall>y\<in>{A n..B n}. dist x y < e" .. |
2163 show "\<exists>c d. x0 \<in> {c..d} \<and> {c..d} \<subseteq> ball x0 e \<and> {c..d} \<subseteq> {a..b} \<and> \<not> P {c..d}" |
2399 show "\<exists>c d. x0 \<in> {c..d} \<and> {c..d} \<subseteq> ball x0 e \<and> {c..d} \<subseteq> {a..b} \<and> \<not> P {c..d}" |
2164 apply(rule_tac x="A n" in exI,rule_tac x="B n" in exI) apply(rule,rule x0) apply rule defer |
2400 apply (rule_tac x="A n" in exI) |
2165 proof show "\<not> P {A n..B n}" apply(cases "0<n") using AB(3)[of "n - 1"] assms(3) AB(1-2) by auto |
2401 apply (rule_tac x="B n" in exI) |
2166 show "{A n..B n} \<subseteq> ball x0 e" using n using x0[of n] by auto |
2402 apply rule |
2167 show "{A n..B n} \<subseteq> {a..b}" unfolding AB(1-2)[symmetric] apply(rule ABsubset) by auto |
2403 apply (rule x0) |
2168 qed qed qed |
2404 apply rule |
|
2405 defer |
|
2406 apply rule |
|
2407 proof - |
|
2408 show "\<not> P {A n..B n}" |
|
2409 apply (cases "0 < n") |
|
2410 using AB(3)[of "n - 1"] assms(3) AB(1-2) |
|
2411 apply auto |
|
2412 done |
|
2413 show "{A n..B n} \<subseteq> ball x0 e" |
|
2414 using n using x0[of n] by auto |
|
2415 show "{A n..B n} \<subseteq> {a..b}" |
|
2416 unfolding AB(1-2)[symmetric] by (rule ABsubset) auto |
|
2417 qed |
|
2418 qed |
|
2419 qed |
|
2420 |
2169 |
2421 |
2170 subsection {* Cousin's lemma. *} |
2422 subsection {* Cousin's lemma. *} |
2171 |
2423 |
2172 lemma fine_division_exists: assumes "gauge g" |
2424 lemma fine_division_exists: |
2173 obtains p where "p tagged_division_of {a..b::'a::ordered_euclidean_space}" "g fine p" |
2425 fixes a b :: "'a::ordered_euclidean_space" |
2174 proof- presume "\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p) \<Longrightarrow> False" |
2426 assumes "gauge g" |
2175 then guess p unfolding atomize_not not_not .. thus thesis apply-apply(rule that[of p]) by auto |
2427 obtains p where "p tagged_division_of {a..b}" "g fine p" |
2176 next assume as:"\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p)" |
2428 proof - |
|
2429 presume "\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p) \<Longrightarrow> False" |
|
2430 then obtain p where "p tagged_division_of {a..b}" "g fine p" by blast |
|
2431 then show thesis .. |
|
2432 next |
|
2433 assume as: "\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p)" |
2177 guess x apply(rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p",rule_format,OF _ _ as]) |
2434 guess x apply(rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p",rule_format,OF _ _ as]) |
2178 apply(rule_tac x="{}" in exI) defer apply(erule conjE exE)+ |
2435 apply(rule_tac x="{}" in exI) |
2179 proof- show "{} tagged_division_of {} \<and> g fine {}" unfolding fine_def by auto |
2436 defer apply(erule conjE exE)+ |
|
2437 proof - |
|
2438 show "{} tagged_division_of {} \<and> g fine {}" unfolding fine_def by auto |
2180 fix s t p p' assume "p tagged_division_of s" "g fine p" "p' tagged_division_of t" "g fine p'" "interior s \<inter> interior t = {}" |
2439 fix s t p p' assume "p tagged_division_of s" "g fine p" "p' tagged_division_of t" "g fine p'" "interior s \<inter> interior t = {}" |
2181 thus "\<exists>p. p tagged_division_of s \<union> t \<and> g fine p" apply-apply(rule_tac x="p \<union> p'" in exI) apply rule |
2440 then show "\<exists>p. p tagged_division_of s \<union> t \<and> g fine p" |
2182 apply(rule tagged_division_union) prefer 4 apply(rule fine_union) by auto |
2441 apply - |
|
2442 apply (rule_tac x="p \<union> p'" in exI) |
|
2443 apply rule |
|
2444 apply (rule tagged_division_union) |
|
2445 prefer 4 |
|
2446 apply (rule fine_union) |
|
2447 apply auto |
|
2448 done |
2183 qed note x=this |
2449 qed note x=this |
2184 obtain e where e:"e>0" "ball x e \<subseteq> g x" using gaugeD[OF assms, of x] unfolding open_contains_ball by auto |
2450 obtain e where e:"e > 0" "ball x e \<subseteq> g x" |
|
2451 using gaugeD[OF assms, of x] unfolding open_contains_ball by auto |
2185 from x(2)[OF e(1)] guess c d apply-apply(erule exE conjE)+ . note c_d = this |
2452 from x(2)[OF e(1)] guess c d apply-apply(erule exE conjE)+ . note c_d = this |
2186 have "g fine {(x, {c..d})}" unfolding fine_def using e using c_d(2) by auto |
2453 have "g fine {(x, {c..d})}" |
2187 thus False using tagged_division_of_self[OF c_d(1)] using c_d by auto qed |
2454 unfolding fine_def using e using c_d(2) by auto |
|
2455 then show False using tagged_division_of_self[OF c_d(1)] using c_d by auto |
|
2456 qed |
|
2457 |
2188 |
2458 |
2189 subsection {* Basic theorems about integrals. *} |
2459 subsection {* Basic theorems about integrals. *} |
2190 |
2460 |
2191 lemma has_integral_unique: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector" |
2461 lemma has_integral_unique: |
2192 assumes "(f has_integral k1) i" "(f has_integral k2) i" shows "k1 = k2" |
2462 fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::real_normed_vector" |
2193 proof(rule ccontr) let ?e = "norm(k1 - k2) / 2" assume as:"k1 \<noteq> k2" hence e:"?e > 0" by auto |
2463 assumes "(f has_integral k1) i" and "(f has_integral k2) i" |
|
2464 shows "k1 = k2" |
|
2465 proof (rule ccontr) let ?e = "norm(k1 - k2) / 2" assume as:"k1 \<noteq> k2" hence e:"?e > 0" by auto |
2194 have lem:"\<And>f::'n \<Rightarrow> 'a. \<And> a b k1 k2. |
2466 have lem:"\<And>f::'n \<Rightarrow> 'a. \<And> a b k1 k2. |
2195 (f has_integral k1) ({a..b}) \<Longrightarrow> (f has_integral k2) ({a..b}) \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> False" |
2467 (f has_integral k1) ({a..b}) \<Longrightarrow> (f has_integral k2) ({a..b}) \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> False" |
2196 proof- case goal1 let ?e = "norm(k1 - k2) / 2" from goal1(3) have e:"?e > 0" by auto |
2468 proof- case goal1 let ?e = "norm(k1 - k2) / 2" from goal1(3) have e:"?e > 0" by auto |
2197 guess d1 by(rule has_integralD[OF goal1(1) e]) note d1=this |
2469 guess d1 by(rule has_integralD[OF goal1(1) e]) note d1=this |
2198 guess d2 by(rule has_integralD[OF goal1(2) e]) note d2=this |
2470 guess d2 by(rule has_integralD[OF goal1(2) e]) note d2=this |