174 assumes "content (cbox a b) = 0" "d division_of (cbox a b)" |
174 assumes "content (cbox a b) = 0" "d division_of (cbox a b)" |
175 shows "\<forall>k\<in>d. content k = 0" |
175 shows "\<forall>k\<in>d. content k = 0" |
176 unfolding forall_in_division[OF assms(2)] |
176 unfolding forall_in_division[OF assms(2)] |
177 by (metis antisym_conv assms content_pos_le content_subset division_ofD(2)) |
177 by (metis antisym_conv assms content_pos_le content_subset division_ofD(2)) |
178 |
178 |
179 lemma setsum_content_null: |
179 lemma sum_content_null: |
180 assumes "content (cbox a b) = 0" |
180 assumes "content (cbox a b) = 0" |
181 and "p tagged_division_of (cbox a b)" |
181 and "p tagged_division_of (cbox a b)" |
182 shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)" |
182 shows "sum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)" |
183 proof (rule setsum.neutral, rule) |
183 proof (rule sum.neutral, rule) |
184 fix y |
184 fix y |
185 assume y: "y \<in> p" |
185 assume y: "y \<in> p" |
186 obtain x k where xk: "y = (x, k)" |
186 obtain x k where xk: "y = (x, k)" |
187 using surj_pair[of y] by blast |
187 using surj_pair[of y] by blast |
188 note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]] |
188 note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]] |
197 qed |
197 qed |
198 |
198 |
199 lemma operative_content[intro]: "add.operative content" |
199 lemma operative_content[intro]: "add.operative content" |
200 by (force simp add: add.operative_def content_split[symmetric] content_eq_0_interior) |
200 by (force simp add: add.operative_def content_split[symmetric] content_eq_0_interior) |
201 |
201 |
202 lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> setsum content d = content (cbox a b)" |
202 lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> sum content d = content (cbox a b)" |
203 by (metis operative_content setsum.operative_division) |
203 by (metis operative_content sum.operative_division) |
204 |
204 |
205 lemma additive_content_tagged_division: |
205 lemma additive_content_tagged_division: |
206 "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)" |
206 "d tagged_division_of (cbox a b) \<Longrightarrow> sum (\<lambda>(x,l). content l) d = content (cbox a b)" |
207 unfolding setsum.operative_tagged_division[OF operative_content, symmetric] by blast |
207 unfolding sum.operative_tagged_division[OF operative_content, symmetric] by blast |
208 |
208 |
209 lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b" |
209 lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b" |
210 by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0) |
210 by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0) |
211 |
211 |
212 lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}" |
212 lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}" |
232 |
232 |
233 lemma has_integral: |
233 lemma has_integral: |
234 "(f has_integral y) (cbox a b) \<longleftrightarrow> |
234 "(f has_integral y) (cbox a b) \<longleftrightarrow> |
235 (\<forall>e>0. \<exists>d. gauge d \<and> |
235 (\<forall>e>0. \<exists>d. gauge d \<and> |
236 (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
236 (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
237 norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))" |
237 norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))" |
238 by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff) |
238 by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff) |
239 |
239 |
240 lemma has_integral_real: |
240 lemma has_integral_real: |
241 "(f has_integral y) {a .. b::real} \<longleftrightarrow> |
241 "(f has_integral y) {a .. b::real} \<longleftrightarrow> |
242 (\<forall>e>0. \<exists>d. gauge d \<and> |
242 (\<forall>e>0. \<exists>d. gauge d \<and> |
243 (\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow> |
243 (\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow> |
244 norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))" |
244 norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))" |
245 unfolding box_real[symmetric] |
245 unfolding box_real[symmetric] |
246 by (rule has_integral) |
246 by (rule has_integral) |
247 |
247 |
248 lemma has_integralD[dest]: |
248 lemma has_integralD[dest]: |
249 assumes "(f has_integral y) (cbox a b)" |
249 assumes "(f has_integral y) (cbox a b)" |
362 lemma has_integral_const [intro]: |
362 lemma has_integral_const [intro]: |
363 fixes a b :: "'a::euclidean_space" |
363 fixes a b :: "'a::euclidean_space" |
364 shows "((\<lambda>x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)" |
364 shows "((\<lambda>x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)" |
365 using eventually_division_filter_tagged_division[of "cbox a b"] |
365 using eventually_division_filter_tagged_division[of "cbox a b"] |
366 additive_content_tagged_division[of _ a b] |
366 additive_content_tagged_division[of _ a b] |
367 by (auto simp: has_integral_cbox split_beta' scaleR_setsum_left[symmetric] |
367 by (auto simp: has_integral_cbox split_beta' scaleR_sum_left[symmetric] |
368 elim!: eventually_mono intro!: tendsto_cong[THEN iffD1, OF _ tendsto_const]) |
368 elim!: eventually_mono intro!: tendsto_cong[THEN iffD1, OF _ tendsto_const]) |
369 |
369 |
370 lemma has_integral_const_real [intro]: |
370 lemma has_integral_const_real [intro]: |
371 fixes a b :: real |
371 fixes a b :: real |
372 shows "((\<lambda>x. c) has_integral (content {a .. b} *\<^sub>R c)) {a .. b}" |
372 shows "((\<lambda>x. c) has_integral (content {a .. b} *\<^sub>R c)) {a .. b}" |
389 proof - |
389 proof - |
390 have lem: "(\<forall>x\<in>cbox a b. f x = 0) \<Longrightarrow> (f has_integral 0) (cbox a b)" for a b and f :: "'n \<Rightarrow> 'a" |
390 have lem: "(\<forall>x\<in>cbox a b. f x = 0) \<Longrightarrow> (f has_integral 0) (cbox a b)" for a b and f :: "'n \<Rightarrow> 'a" |
391 unfolding has_integral_cbox |
391 unfolding has_integral_cbox |
392 using eventually_division_filter_tagged_division[of "cbox a b"] |
392 using eventually_division_filter_tagged_division[of "cbox a b"] |
393 by (subst tendsto_cong[where g="\<lambda>_. 0"]) |
393 by (subst tendsto_cong[where g="\<lambda>_. 0"]) |
394 (auto elim!: eventually_mono intro!: setsum.neutral simp: tag_in_interval) |
394 (auto elim!: eventually_mono intro!: sum.neutral simp: tag_in_interval) |
395 { |
395 { |
396 presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis" |
396 presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis" |
397 with assms lem show ?thesis |
397 with assms lem show ?thesis |
398 by blast |
398 by blast |
399 } |
399 } |
664 fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space" |
664 fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space" |
665 assumes "f integrable_on s" |
665 assumes "f integrable_on s" |
666 shows "integral s (\<lambda>x. f x \<bullet> k) = integral s f \<bullet> k" |
666 shows "integral s (\<lambda>x. f x \<bullet> k) = integral s f \<bullet> k" |
667 unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] .. |
667 unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] .. |
668 |
668 |
669 lemma has_integral_setsum: |
669 lemma has_integral_sum: |
670 assumes "finite t" |
670 assumes "finite t" |
671 and "\<forall>a\<in>t. ((f a) has_integral (i a)) s" |
671 and "\<forall>a\<in>t. ((f a) has_integral (i a)) s" |
672 shows "((\<lambda>x. setsum (\<lambda>a. f a x) t) has_integral (setsum i t)) s" |
672 shows "((\<lambda>x. sum (\<lambda>a. f a x) t) has_integral (sum i t)) s" |
673 using assms(1) subset_refl[of t] |
673 using assms(1) subset_refl[of t] |
674 proof (induct rule: finite_subset_induct) |
674 proof (induct rule: finite_subset_induct) |
675 case empty |
675 case empty |
676 then show ?case by auto |
676 then show ?case by auto |
677 next |
677 next |
678 case (insert x F) |
678 case (insert x F) |
679 with assms show ?case |
679 with assms show ?case |
680 by (simp add: has_integral_add) |
680 by (simp add: has_integral_add) |
681 qed |
681 qed |
682 |
682 |
683 lemma integral_setsum: |
683 lemma integral_sum: |
684 "\<lbrakk>finite t; \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> |
684 "\<lbrakk>finite t; \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> |
685 integral s (\<lambda>x. setsum (\<lambda>a. f a x) t) = setsum (\<lambda>a. integral s (f a)) t" |
685 integral s (\<lambda>x. sum (\<lambda>a. f a x) t) = sum (\<lambda>a. integral s (f a)) t" |
686 by (auto intro: has_integral_setsum integrable_integral) |
686 by (auto intro: has_integral_sum integrable_integral) |
687 |
687 |
688 lemma integrable_setsum: |
688 lemma integrable_sum: |
689 "\<lbrakk>finite t; \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) t) integrable_on s" |
689 "\<lbrakk>finite t; \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. sum (\<lambda>a. f a x) t) integrable_on s" |
690 unfolding integrable_on_def |
690 unfolding integrable_on_def |
691 apply (drule bchoice) |
691 apply (drule bchoice) |
692 using has_integral_setsum[of t] |
692 using has_integral_sum[of t] |
693 apply auto |
693 apply auto |
694 done |
694 done |
695 |
695 |
696 lemma has_integral_eq: |
696 lemma has_integral_eq: |
697 assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x" |
697 assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x" |
758 by (simp add: divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse) |
758 by (simp add: divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse) |
759 |
759 |
760 lemma has_integral_null [intro]: "content(cbox a b) = 0 \<Longrightarrow> (f has_integral 0) (cbox a b)" |
760 lemma has_integral_null [intro]: "content(cbox a b) = 0 \<Longrightarrow> (f has_integral 0) (cbox a b)" |
761 unfolding has_integral_cbox |
761 unfolding has_integral_cbox |
762 using eventually_division_filter_tagged_division[of "cbox a b"] |
762 using eventually_division_filter_tagged_division[of "cbox a b"] |
763 by (subst tendsto_cong[where g="\<lambda>_. 0"]) (auto elim: eventually_mono intro: setsum_content_null) |
763 by (subst tendsto_cong[where g="\<lambda>_. 0"]) (auto elim: eventually_mono intro: sum_content_null) |
764 |
764 |
765 lemma has_integral_null_real [intro]: "content {a .. b::real} = 0 \<Longrightarrow> (f has_integral 0) {a .. b}" |
765 lemma has_integral_null_real [intro]: "content {a .. b::real} = 0 \<Longrightarrow> (f has_integral 0) {a .. b}" |
766 by (metis box_real(2) has_integral_null) |
766 by (metis box_real(2) has_integral_null) |
767 |
767 |
768 lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \<Longrightarrow> (f has_integral i) (cbox a b) \<longleftrightarrow> i = 0" |
768 lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \<Longrightarrow> (f has_integral i) (cbox a b) \<longleftrightarrow> i = 0" |
838 next |
838 next |
839 assume "(\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)" |
839 assume "(\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)" |
840 hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral ((y \<bullet> b) *\<^sub>R b)) A" |
840 hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral ((y \<bullet> b) *\<^sub>R b)) A" |
841 by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left) |
841 by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left) |
842 hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. (y \<bullet> b) *\<^sub>R b)) A" |
842 hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. (y \<bullet> b) *\<^sub>R b)) A" |
843 by (intro has_integral_setsum) (simp_all add: o_def) |
843 by (intro has_integral_sum) (simp_all add: o_def) |
844 thus "(f has_integral y) A" by (simp add: euclidean_representation) |
844 thus "(f has_integral y) A" by (simp add: euclidean_representation) |
845 qed |
845 qed |
846 |
846 |
847 lemma has_integral_componentwise: |
847 lemma has_integral_componentwise: |
848 fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space" |
848 fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space" |
863 then obtain y where "\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral y b) A" |
863 then obtain y where "\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral y b) A" |
864 unfolding integrable_on_def by (subst (asm) bchoice_iff) blast |
864 unfolding integrable_on_def by (subst (asm) bchoice_iff) blast |
865 hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral (y b *\<^sub>R b)) A" |
865 hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral (y b *\<^sub>R b)) A" |
866 by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left) |
866 by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left) |
867 hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. y b *\<^sub>R b)) A" |
867 hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. y b *\<^sub>R b)) A" |
868 by (intro has_integral_setsum) (simp_all add: o_def) |
868 by (intro has_integral_sum) (simp_all add: o_def) |
869 thus "f integrable_on A" by (auto simp: integrable_on_def o_def euclidean_representation) |
869 thus "f integrable_on A" by (auto simp: integrable_on_def o_def euclidean_representation) |
870 qed |
870 qed |
871 |
871 |
872 lemma integrable_componentwise: |
872 lemma integrable_componentwise: |
873 fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space" |
873 fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space" |
883 by (subst (asm) integrable_componentwise_iff, intro integrable_linear ballI) |
883 by (subst (asm) integrable_componentwise_iff, intro integrable_linear ballI) |
884 (simp_all add: bounded_linear_scaleR_left) |
884 (simp_all add: bounded_linear_scaleR_left) |
885 have "integral A f = integral A (\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b)" |
885 have "integral A f = integral A (\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b)" |
886 by (simp add: euclidean_representation) |
886 by (simp add: euclidean_representation) |
887 also from integrable have "\<dots> = (\<Sum>a\<in>Basis. integral A (\<lambda>x. (f x \<bullet> a) *\<^sub>R a))" |
887 also from integrable have "\<dots> = (\<Sum>a\<in>Basis. integral A (\<lambda>x. (f x \<bullet> a) *\<^sub>R a))" |
888 by (subst integral_setsum) (simp_all add: o_def) |
888 by (subst integral_sum) (simp_all add: o_def) |
889 finally show ?thesis . |
889 finally show ?thesis . |
890 qed |
890 qed |
891 |
891 |
892 lemma integrable_component: |
892 lemma integrable_component: |
893 "f integrable_on A \<Longrightarrow> (\<lambda>x. f x \<bullet> (y :: 'b :: euclidean_space)) integrable_on A" |
893 "f integrable_on A \<Longrightarrow> (\<lambda>x. f x \<bullet> (y :: 'b :: euclidean_space)) integrable_on A" |
942 then have "\<forall>n. \<exists>p. p tagged_division_of (cbox a b) \<and> (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}}) fine p" |
942 then have "\<forall>n. \<exists>p. p tagged_division_of (cbox a b) \<and> (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}}) fine p" |
943 by (meson fine_division_exists) |
943 by (meson fine_division_exists) |
944 from choice[OF this] guess p .. note p = conjunctD2[OF this[rule_format]] |
944 from choice[OF this] guess p .. note p = conjunctD2[OF this[rule_format]] |
945 have dp: "\<And>i n. i\<le>n \<Longrightarrow> d i fine p n" |
945 have dp: "\<And>i n. i\<le>n \<Longrightarrow> d i fine p n" |
946 using p(2) unfolding fine_inters by auto |
946 using p(2) unfolding fine_inters by auto |
947 have "Cauchy (\<lambda>n. setsum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))" |
947 have "Cauchy (\<lambda>n. sum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))" |
948 proof (rule CauchyI, goal_cases) |
948 proof (rule CauchyI, goal_cases) |
949 case (1 e) |
949 case (1 e) |
950 then guess N unfolding real_arch_inverse[of e] .. note N=this |
950 then guess N unfolding real_arch_inverse[of e] .. note N=this |
951 show ?case |
951 show ?case |
952 apply (rule_tac x=N in exI) |
952 apply (rule_tac x=N in exI) |
1122 using xk using content_empty by auto |
1122 using xk using content_empty by auto |
1123 then have "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0" |
1123 then have "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0" |
1124 unfolding xk split_conv by auto |
1124 unfolding xk split_conv by auto |
1125 } note [simp] = this |
1125 } note [simp] = this |
1126 have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow> |
1126 have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow> |
1127 setsum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} = |
1127 sum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} = |
1128 setsum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)" |
1128 sum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)" |
1129 by (rule setsum.mono_neutral_left) auto |
1129 by (rule sum.mono_neutral_left) auto |
1130 let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}" |
1130 let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}" |
1131 have d1_fine: "d1 fine ?M1" |
1131 have d1_fine: "d1 fine ?M1" |
1132 by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm) |
1132 by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm) |
1133 have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2" |
1133 have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2" |
1134 proof (rule d1norm [OF tagged_division_ofI d1_fine]) |
1134 proof (rule d1norm [OF tagged_division_ofI d1_fine]) |
1216 (\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - (i + j)" |
1216 (\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - (i + j)" |
1217 by auto |
1217 by auto |
1218 also have "\<dots> = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) + |
1218 also have "\<dots> = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) + |
1219 (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) - (i + j)" |
1219 (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) - (i + j)" |
1220 unfolding lem3[OF p(3)] |
1220 unfolding lem3[OF p(3)] |
1221 by (subst (1 2) setsum.reindex_nontrivial[OF p(3)]) |
1221 by (subst (1 2) sum.reindex_nontrivial[OF p(3)]) |
1222 (auto intro!: k eq0 tagged_division_split_left_inj_content[OF p(1)] tagged_division_split_right_inj_content[OF p(1)] |
1222 (auto intro!: k eq0 tagged_division_split_left_inj_content[OF p(1)] tagged_division_split_right_inj_content[OF p(1)] |
1223 simp: cont_eq)+ |
1223 simp: cont_eq)+ |
1224 also note setsum.distrib[symmetric] |
1224 also note sum.distrib[symmetric] |
1225 also have "\<And>x. x \<in> p \<Longrightarrow> |
1225 also have "\<And>x. x \<in> p \<Longrightarrow> |
1226 (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x + |
1226 (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x + |
1227 (\<lambda>(x,ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x = |
1227 (\<lambda>(x,ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x = |
1228 (\<lambda>(x,ka). content ka *\<^sub>R f x) x" |
1228 (\<lambda>(x,ka). content ka *\<^sub>R f x) x" |
1229 proof clarify |
1229 proof clarify |
1234 content b *\<^sub>R f a" |
1234 content b *\<^sub>R f a" |
1235 unfolding scaleR_left_distrib[symmetric] |
1235 unfolding scaleR_left_distrib[symmetric] |
1236 unfolding uv content_split[OF k,of u v c] |
1236 unfolding uv content_split[OF k,of u v c] |
1237 by auto |
1237 by auto |
1238 qed |
1238 qed |
1239 note setsum.cong [OF _ this] |
1239 note sum.cong [OF _ this] |
1240 finally have "(\<Sum>(x, k)\<in>{(x, kk \<inter> {x. x \<bullet> k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}}. content k *\<^sub>R f x) - i + |
1240 finally have "(\<Sum>(x, k)\<in>{(x, kk \<inter> {x. x \<bullet> k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}}. content k *\<^sub>R f x) - i + |
1241 ((\<Sum>(x, k)\<in>{(x, kk \<inter> {x. c \<le> x \<bullet> k}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}}. content k *\<^sub>R f x) - j) = |
1241 ((\<Sum>(x, k)\<in>{(x, kk \<inter> {x. c \<le> x \<bullet> k}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}}. content k *\<^sub>R f x) - j) = |
1242 (\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f x) - (i + j)" |
1242 (\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f x) - (i + j)" |
1243 by auto |
1243 by auto |
1244 } |
1244 } |
1256 and "e > 0" |
1256 and "e > 0" |
1257 and k: "k \<in> Basis" |
1257 and k: "k \<in> Basis" |
1258 obtains d where "gauge d" |
1258 obtains d where "gauge d" |
1259 "\<forall>p1 p2. p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<and> d fine p1 \<and> |
1259 "\<forall>p1 p2. p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<and> d fine p1 \<and> |
1260 p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) \<and> d fine p2 \<longrightarrow> |
1260 p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) \<and> d fine p2 \<longrightarrow> |
1261 norm ((setsum (\<lambda>(x,k). content k *\<^sub>R f x) p1 + setsum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e" |
1261 norm ((sum (\<lambda>(x,k). content k *\<^sub>R f x) p1 + sum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e" |
1262 proof - |
1262 proof - |
1263 guess d using has_integralD[OF assms(1-2)] . note d=this |
1263 guess d using has_integralD[OF assms(1-2)] . note d=this |
1264 { fix p1 p2 |
1264 { fix p1 p2 |
1265 assume "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" "d fine p1" |
1265 assume "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" "d fine p1" |
1266 note p1=tagged_division_ofD[OF this(1)] this |
1266 note p1=tagged_division_ofD[OF this(1)] this |
1285 using x interior_subset by fastforce |
1285 using x interior_subset by fastforce |
1286 have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (e / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then e/2 else 0)" |
1286 have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (e / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then e/2 else 0)" |
1287 using e k by (auto simp: inner_simps inner_not_same_Basis) |
1287 using e k by (auto simp: inner_simps inner_not_same_Basis) |
1288 have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (e / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) = |
1288 have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (e / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) = |
1289 (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))" |
1289 (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))" |
1290 using "*" by (blast intro: setsum.cong) |
1290 using "*" by (blast intro: sum.cong) |
1291 also have "\<dots> < e" |
1291 also have "\<dots> < e" |
1292 apply (subst setsum.delta) |
1292 apply (subst sum.delta) |
1293 using e |
1293 using e |
1294 apply auto |
1294 apply auto |
1295 done |
1295 done |
1296 finally have "x + (e/2) *\<^sub>R k \<in> ball x e" |
1296 finally have "x + (e/2) *\<^sub>R k \<in> ball x e" |
1297 unfolding mem_ball dist_norm by(rule le_less_trans[OF norm_le_l1]) |
1297 unfolding mem_ball dist_norm by(rule le_less_trans[OF norm_le_l1]) |
1306 then have "content b *\<^sub>R f a = 0" |
1306 then have "content b *\<^sub>R f a = 0" |
1307 by auto |
1307 by auto |
1308 } |
1308 } |
1309 then have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) = |
1309 then have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) = |
1310 norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)" |
1310 norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)" |
1311 by (subst setsum.union_inter_neutral) (auto simp: p1 p2) |
1311 by (subst sum.union_inter_neutral) (auto simp: p1 p2) |
1312 also have "\<dots> < e" |
1312 also have "\<dots> < e" |
1313 by (rule k d(2) p12 fine_union p1 p2)+ |
1313 by (rule k d(2) p12 fine_union p1 p2)+ |
1314 finally have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" . |
1314 finally have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" . |
1315 } |
1315 } |
1316 then show ?thesis |
1316 then show ?thesis |
1424 subsection \<open>Bounds on the norm of Riemann sums and the integral itself.\<close> |
1424 subsection \<open>Bounds on the norm of Riemann sums and the integral itself.\<close> |
1425 |
1425 |
1426 lemma dsum_bound: |
1426 lemma dsum_bound: |
1427 assumes "p division_of (cbox a b)" |
1427 assumes "p division_of (cbox a b)" |
1428 and "norm c \<le> e" |
1428 and "norm c \<le> e" |
1429 shows "norm (setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content(cbox a b)" |
1429 shows "norm (sum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content(cbox a b)" |
1430 proof - |
1430 proof - |
1431 have sumeq: "(\<Sum>i\<in>p. \<bar>content i\<bar>) = setsum content p" |
1431 have sumeq: "(\<Sum>i\<in>p. \<bar>content i\<bar>) = sum content p" |
1432 apply (rule setsum.cong) |
1432 apply (rule sum.cong) |
1433 using assms |
1433 using assms |
1434 apply simp |
1434 apply simp |
1435 apply (metis abs_of_nonneg assms(1) content_pos_le division_ofD(4)) |
1435 apply (metis abs_of_nonneg assms(1) content_pos_le division_ofD(4)) |
1436 done |
1436 done |
1437 have e: "0 \<le> e" |
1437 have e: "0 \<le> e" |
1438 using assms(2) norm_ge_zero order_trans by blast |
1438 using assms(2) norm_ge_zero order_trans by blast |
1439 have "norm (setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))" |
1439 have "norm (sum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))" |
1440 using norm_setsum by blast |
1440 using norm_sum by blast |
1441 also have "... \<le> e * (\<Sum>i\<in>p. \<bar>content i\<bar>)" |
1441 also have "... \<le> e * (\<Sum>i\<in>p. \<bar>content i\<bar>)" |
1442 by (simp add: setsum_distrib_left[symmetric] mult.commute assms(2) mult_right_mono setsum_nonneg) |
1442 by (simp add: sum_distrib_left[symmetric] mult.commute assms(2) mult_right_mono sum_nonneg) |
1443 also have "... \<le> e * content (cbox a b)" |
1443 also have "... \<le> e * content (cbox a b)" |
1444 apply (rule mult_left_mono [OF _ e]) |
1444 apply (rule mult_left_mono [OF _ e]) |
1445 apply (simp add: sumeq) |
1445 apply (simp add: sumeq) |
1446 using additive_content_division assms(1) eq_iff apply blast |
1446 using additive_content_division assms(1) eq_iff apply blast |
1447 done |
1447 done |
1449 qed |
1449 qed |
1450 |
1450 |
1451 lemma rsum_bound: |
1451 lemma rsum_bound: |
1452 assumes p: "p tagged_division_of (cbox a b)" |
1452 assumes p: "p tagged_division_of (cbox a b)" |
1453 and "\<forall>x\<in>cbox a b. norm (f x) \<le> e" |
1453 and "\<forall>x\<in>cbox a b. norm (f x) \<le> e" |
1454 shows "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> e * content (cbox a b)" |
1454 shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> e * content (cbox a b)" |
1455 proof (cases "cbox a b = {}") |
1455 proof (cases "cbox a b = {}") |
1456 case True show ?thesis |
1456 case True show ?thesis |
1457 using p unfolding True tagged_division_of_trivial by auto |
1457 using p unfolding True tagged_division_of_trivial by auto |
1458 next |
1458 next |
1459 case False |
1459 case False |
1460 then have e: "e \<ge> 0" |
1460 then have e: "e \<ge> 0" |
1461 by (meson ex_in_conv assms(2) norm_ge_zero order_trans) |
1461 by (meson ex_in_conv assms(2) norm_ge_zero order_trans) |
1462 have setsum_le: "setsum (content \<circ> snd) p \<le> content (cbox a b)" |
1462 have sum_le: "sum (content \<circ> snd) p \<le> content (cbox a b)" |
1463 unfolding additive_content_tagged_division[OF p, symmetric] split_def |
1463 unfolding additive_content_tagged_division[OF p, symmetric] split_def |
1464 by (auto intro: eq_refl) |
1464 by (auto intro: eq_refl) |
1465 have con: "\<And>xk. xk \<in> p \<Longrightarrow> 0 \<le> content (snd xk)" |
1465 have con: "\<And>xk. xk \<in> p \<Longrightarrow> 0 \<le> content (snd xk)" |
1466 using tagged_division_ofD(4) [OF p] content_pos_le |
1466 using tagged_division_ofD(4) [OF p] content_pos_le |
1467 by force |
1467 by force |
1468 have norm: "\<And>xk. xk \<in> p \<Longrightarrow> norm (f (fst xk)) \<le> e" |
1468 have norm: "\<And>xk. xk \<in> p \<Longrightarrow> norm (f (fst xk)) \<le> e" |
1469 unfolding fst_conv using tagged_division_ofD(2,3)[OF p] assms |
1469 unfolding fst_conv using tagged_division_ofD(2,3)[OF p] assms |
1470 by (metis prod.collapse subset_eq) |
1470 by (metis prod.collapse subset_eq) |
1471 have "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> (\<Sum>i\<in>p. norm (case i of (x, k) \<Rightarrow> content k *\<^sub>R f x))" |
1471 have "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> (\<Sum>i\<in>p. norm (case i of (x, k) \<Rightarrow> content k *\<^sub>R f x))" |
1472 by (rule norm_setsum) |
1472 by (rule norm_sum) |
1473 also have "... \<le> e * content (cbox a b)" |
1473 also have "... \<le> e * content (cbox a b)" |
1474 unfolding split_def norm_scaleR |
1474 unfolding split_def norm_scaleR |
1475 apply (rule order_trans[OF setsum_mono]) |
1475 apply (rule order_trans[OF sum_mono]) |
1476 apply (rule mult_left_mono[OF _ abs_ge_zero, of _ e]) |
1476 apply (rule mult_left_mono[OF _ abs_ge_zero, of _ e]) |
1477 apply (metis norm) |
1477 apply (metis norm) |
1478 unfolding setsum_distrib_right[symmetric] |
1478 unfolding sum_distrib_right[symmetric] |
1479 using con setsum_le |
1479 using con sum_le |
1480 apply (auto simp: mult.commute intro: mult_left_mono [OF _ e]) |
1480 apply (auto simp: mult.commute intro: mult_left_mono [OF _ e]) |
1481 done |
1481 done |
1482 finally show ?thesis . |
1482 finally show ?thesis . |
1483 qed |
1483 qed |
1484 |
1484 |
1485 lemma rsum_diff_bound: |
1485 lemma rsum_diff_bound: |
1486 assumes "p tagged_division_of (cbox a b)" |
1486 assumes "p tagged_division_of (cbox a b)" |
1487 and "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" |
1487 and "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" |
1488 shows "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - setsum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le> |
1488 shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - sum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le> |
1489 e * content (cbox a b)" |
1489 e * content (cbox a b)" |
1490 apply (rule order_trans[OF _ rsum_bound[OF assms]]) |
1490 apply (rule order_trans[OF _ rsum_bound[OF assms]]) |
1491 apply (simp add: split_def scaleR_diff_right setsum_subtractf eq_refl) |
1491 apply (simp add: split_def scaleR_diff_right sum_subtractf eq_refl) |
1492 done |
1492 done |
1493 |
1493 |
1494 lemma has_integral_bound: |
1494 lemma has_integral_bound: |
1495 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
1495 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
1496 assumes "0 \<le> B" |
1496 assumes "0 \<le> B" |
1532 |
1532 |
1533 lemma rsum_component_le: |
1533 lemma rsum_component_le: |
1534 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1534 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1535 assumes "p tagged_division_of (cbox a b)" |
1535 assumes "p tagged_division_of (cbox a b)" |
1536 and "\<forall>x\<in>cbox a b. (f x)\<bullet>i \<le> (g x)\<bullet>i" |
1536 and "\<forall>x\<in>cbox a b. (f x)\<bullet>i \<le> (g x)\<bullet>i" |
1537 shows "(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p)\<bullet>i \<le> (setsum (\<lambda>(x,k). content k *\<^sub>R g x) p)\<bullet>i" |
1537 shows "(sum (\<lambda>(x,k). content k *\<^sub>R f x) p)\<bullet>i \<le> (sum (\<lambda>(x,k). content k *\<^sub>R g x) p)\<bullet>i" |
1538 unfolding inner_setsum_left |
1538 unfolding inner_sum_left |
1539 proof (rule setsum_mono, clarify) |
1539 proof (rule sum_mono, clarify) |
1540 fix a b |
1540 fix a b |
1541 assume ab: "(a, b) \<in> p" |
1541 assume ab: "(a, b) \<in> p" |
1542 note tagged = tagged_division_ofD(2-4)[OF assms(1) ab] |
1542 note tagged = tagged_division_ofD(2-4)[OF assms(1) ab] |
1543 from this(3) guess u v by (elim exE) note b=this |
1543 from this(3) guess u v by (elim exE) note b=this |
1544 show "(content b *\<^sub>R f a) \<bullet> i \<le> (content b *\<^sub>R g a) \<bullet> i" |
1544 show "(content b *\<^sub>R f a) \<bullet> i \<le> (content b *\<^sub>R g a) \<bullet> i" |
1875 have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> (\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j)) (at_right 0)" |
1875 have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> (\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j)) (at_right 0)" |
1876 by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros) |
1876 by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros) |
1877 also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0" |
1877 also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0" |
1878 using k * |
1878 using k * |
1879 by (intro setprod_zero bexI[OF _ k]) |
1879 by (intro setprod_zero bexI[OF _ k]) |
1880 (auto simp: b'_def a'_def inner_diff inner_setsum_left inner_not_same_Basis intro!: setsum.cong) |
1880 (auto simp: b'_def a'_def inner_diff inner_sum_left inner_not_same_Basis intro!: sum.cong) |
1881 also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) = |
1881 also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) = |
1882 ((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)" |
1882 ((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)" |
1883 proof (intro tendsto_cong eventually_at_rightI) |
1883 proof (intro tendsto_cong eventually_at_rightI) |
1884 fix d :: real assume d: "d \<in> {0<..<1}" |
1884 fix d :: real assume d: "d \<in> {0<..<1}" |
1885 have "cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d} = cbox (a' d) (b' d)" for d |
1885 have "cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d} = cbox (a' d) (b' d)" for d |
1987 note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]] |
1987 note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]] |
1988 show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e" |
1988 show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e" |
1989 unfolding diff_0_right * |
1989 unfolding diff_0_right * |
1990 unfolding real_scaleR_def real_norm_def |
1990 unfolding real_scaleR_def real_norm_def |
1991 apply (subst abs_of_nonneg) |
1991 apply (subst abs_of_nonneg) |
1992 apply (rule setsum_nonneg) |
1992 apply (rule sum_nonneg) |
1993 apply rule |
1993 apply rule |
1994 unfolding split_paired_all split_conv |
1994 unfolding split_paired_all split_conv |
1995 apply (rule mult_nonneg_nonneg) |
1995 apply (rule mult_nonneg_nonneg) |
1996 apply (drule p'(4)) |
1996 apply (drule p'(4)) |
1997 apply (erule exE)+ |
1997 apply (erule exE)+ |
2003 apply (rule content_pos_le) |
2003 apply (rule content_pos_le) |
2004 apply (rule indicator_pos_le) |
2004 apply (rule indicator_pos_le) |
2005 proof - |
2005 proof - |
2006 have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le> |
2006 have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le> |
2007 (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))" |
2007 (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))" |
2008 apply (rule setsum_mono) |
2008 apply (rule sum_mono) |
2009 unfolding split_paired_all split_conv |
2009 unfolding split_paired_all split_conv |
2010 apply (rule mult_right_le_one_le) |
2010 apply (rule mult_right_le_one_le) |
2011 apply (drule p'(4)) |
2011 apply (drule p'(4)) |
2012 apply (auto simp add:interval_doublesplit[OF k]) |
2012 apply (auto simp add:interval_doublesplit[OF k]) |
2013 done |
2013 done |
2014 also have "\<dots> < e" |
2014 also have "\<dots> < e" |
2015 proof (subst setsum.over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases) |
2015 proof (subst sum.over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases) |
2016 case prems: (1 u v) |
2016 case prems: (1 u v) |
2017 then have *: "content (cbox u v) = 0" |
2017 then have *: "content (cbox u v) = 0" |
2018 unfolding content_eq_0_interior by simp |
2018 unfolding content_eq_0_interior by simp |
2019 have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)" |
2019 have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)" |
2020 unfolding interval_doublesplit[OF k] |
2020 unfolding interval_doublesplit[OF k] |
2025 then show ?case |
2025 then show ?case |
2026 unfolding * interval_doublesplit[OF k] |
2026 unfolding * interval_doublesplit[OF k] |
2027 by (blast intro: antisym) |
2027 by (blast intro: antisym) |
2028 next |
2028 next |
2029 have "(\<Sum>l\<in>snd ` p. content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) = |
2029 have "(\<Sum>l\<in>snd ` p. content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) = |
2030 setsum content ((\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}})" |
2030 sum content ((\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}})" |
2031 proof (subst (2) setsum.reindex_nontrivial) |
2031 proof (subst (2) sum.reindex_nontrivial) |
2032 fix x y assume "x \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" "y \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" |
2032 fix x y assume "x \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" "y \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" |
2033 "x \<noteq> y" and eq: "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}" |
2033 "x \<noteq> y" and eq: "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}" |
2034 then obtain x' y' where "(x', x) \<in> p" "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" "(y', y) \<in> p" "y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" |
2034 then obtain x' y' where "(x', x) \<in> p" "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" "(y', y) \<in> p" "y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" |
2035 by (auto) |
2035 by (auto) |
2036 from p'(5)[OF \<open>(x', x) \<in> p\<close> \<open>(y', y) \<in> p\<close>] \<open>x \<noteq> y\<close> have "interior (x \<inter> y) = {}" |
2036 from p'(5)[OF \<open>(x', x) \<in> p\<close> \<open>(y', y) \<in> p\<close>] \<open>x \<noteq> y\<close> have "interior (x \<inter> y) = {}" |
2039 by (auto intro: interior_mono) |
2039 by (auto intro: interior_mono) |
2040 ultimately have "interior (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}" |
2040 ultimately have "interior (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}" |
2041 by (auto simp: eq) |
2041 by (auto simp: eq) |
2042 then show "content (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0" |
2042 then show "content (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0" |
2043 using p'(4)[OF \<open>(x', x) \<in> p\<close>] by (auto simp: interval_doublesplit[OF k] content_eq_0_interior simp del: interior_Int) |
2043 using p'(4)[OF \<open>(x', x) \<in> p\<close>] by (auto simp: interval_doublesplit[OF k] content_eq_0_interior simp del: interior_Int) |
2044 qed (insert p'(1), auto intro!: setsum.mono_neutral_right) |
2044 qed (insert p'(1), auto intro!: sum.mono_neutral_right) |
2045 also have "\<dots> \<le> norm (\<Sum>l\<in>(\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}. content l *\<^sub>R 1::real)" |
2045 also have "\<dots> \<le> norm (\<Sum>l\<in>(\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}. content l *\<^sub>R 1::real)" |
2046 by simp |
2046 by simp |
2047 also have "\<dots> \<le> 1 * content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})" |
2047 also have "\<dots> \<le> 1 * content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})" |
2048 using division_doublesplit[OF p'' k, unfolded interval_doublesplit[OF k]] |
2048 using division_doublesplit[OF p'' k, unfolded interval_doublesplit[OF k]] |
2049 unfolding interval_doublesplit[OF k] by (intro dsum_bound) auto |
2049 unfolding interval_doublesplit[OF k] by (intro dsum_bound) auto |
2142 by (meson Max_ge as(1) dual_order.trans finite_imageI tagged_division_of_finite) |
2142 by (meson Max_ge as(1) dual_order.trans finite_imageI tagged_division_of_finite) |
2143 have "\<forall>i. \<exists>q. q tagged_division_of (cbox a b) \<and> (d i) fine q \<and> (\<forall>(x, k)\<in>p. k \<subseteq> (d i) x \<longrightarrow> (x, k) \<in> q)" |
2143 have "\<forall>i. \<exists>q. q tagged_division_of (cbox a b) \<and> (d i) fine q \<and> (\<forall>(x, k)\<in>p. k \<subseteq> (d i) x \<longrightarrow> (x, k) \<in> q)" |
2144 by (auto intro: tagged_division_finer[OF as(1) d(1)]) |
2144 by (auto intro: tagged_division_finer[OF as(1) d(1)]) |
2145 from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]] |
2145 from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]] |
2146 have *: "\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> (0::real)" |
2146 have *: "\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> (0::real)" |
2147 apply (rule setsum_nonneg) |
2147 apply (rule sum_nonneg) |
2148 apply safe |
2148 apply safe |
2149 unfolding real_scaleR_def |
2149 unfolding real_scaleR_def |
2150 apply (drule tagged_division_ofD(4)[OF q(1)]) |
2150 apply (drule tagged_division_ofD(4)[OF q(1)]) |
2151 apply (auto intro: mult_nonneg_nonneg) |
2151 apply (auto intro: mult_nonneg_nonneg) |
2152 done |
2152 done |
2153 have **: "finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow> |
2153 have **: "finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow> |
2154 (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> setsum f s \<le> setsum g t" for f g s t |
2154 (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> sum f s \<le> sum g t" for f g s t |
2155 apply (rule setsum_le_included[of s t g snd f]) |
2155 apply (rule sum_le_included[of s t g snd f]) |
2156 prefer 4 |
2156 prefer 4 |
2157 apply safe |
2157 apply safe |
2158 apply (erule_tac x=x in ballE) |
2158 apply (erule_tac x=x in ballE) |
2159 apply (erule exE) |
2159 apply (erule exE) |
2160 apply (rule_tac x="(xa,x)" in bexI) |
2160 apply (rule_tac x="(xa,x)" in bexI) |
2161 apply auto |
2161 apply auto |
2162 done |
2162 done |
2163 have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> setsum (\<lambda>i. (real i + 1) * |
2163 have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> sum (\<lambda>i. (real i + 1) * |
2164 norm (setsum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {..N+1}" |
2164 norm (sum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {..N+1}" |
2165 unfolding real_norm_def setsum_distrib_left abs_of_nonneg[OF *] diff_0_right |
2165 unfolding real_norm_def sum_distrib_left abs_of_nonneg[OF *] diff_0_right |
2166 apply (rule order_trans) |
2166 apply (rule order_trans) |
2167 apply (rule norm_setsum) |
2167 apply (rule norm_sum) |
2168 apply (subst sum_sum_product) |
2168 apply (subst sum_sum_product) |
2169 prefer 3 |
2169 prefer 3 |
2170 proof (rule **, safe) |
2170 proof (rule **, safe) |
2171 show "finite {(i, j) |i j. i \<in> {..N + 1} \<and> j \<in> q i}" |
2171 show "finite {(i, j) |i j. i \<in> {..N + 1} \<and> j \<in> q i}" |
2172 apply (rule finite_product_dependent) |
2172 apply (rule finite_product_dependent) |
2227 apply (rule_tac x="(x,k)" in exI) |
2227 apply (rule_tac x="(x,k)" in exI) |
2228 apply safe |
2228 apply safe |
2229 apply auto |
2229 apply auto |
2230 done |
2230 done |
2231 qed (insert as, auto) |
2231 qed (insert as, auto) |
2232 also have "\<dots> \<le> setsum (\<lambda>i. e / 2 / 2 ^ i) {..N+1}" |
2232 also have "\<dots> \<le> sum (\<lambda>i. e / 2 / 2 ^ i) {..N+1}" |
2233 proof (rule setsum_mono, goal_cases) |
2233 proof (rule sum_mono, goal_cases) |
2234 case (1 i) |
2234 case (1 i) |
2235 then show ?case |
2235 then show ?case |
2236 apply (subst mult.commute, subst pos_le_divide_eq[symmetric]) |
2236 apply (subst mult.commute, subst pos_le_divide_eq[symmetric]) |
2237 using d(2)[rule_format, of "q i" i] |
2237 using d(2)[rule_format, of "q i" i] |
2238 using q[rule_format] |
2238 using q[rule_format] |
2239 apply (auto simp add: field_simps) |
2239 apply (auto simp add: field_simps) |
2240 done |
2240 done |
2241 qed |
2241 qed |
2242 also have "\<dots> < e * inverse 2 * 2" |
2242 also have "\<dots> < e * inverse 2 * 2" |
2243 unfolding divide_inverse setsum_distrib_left[symmetric] |
2243 unfolding divide_inverse sum_distrib_left[symmetric] |
2244 apply (rule mult_strict_left_mono) |
2244 apply (rule mult_strict_left_mono) |
2245 unfolding power_inverse [symmetric] lessThan_Suc_atMost[symmetric] |
2245 unfolding power_inverse [symmetric] lessThan_Suc_atMost[symmetric] |
2246 apply (subst geometric_sum) |
2246 apply (subst geometric_sum) |
2247 using prems |
2247 using prems |
2248 apply auto |
2248 apply auto |
2638 subsection \<open>A useful lemma allowing us to factor out the content size.\<close> |
2638 subsection \<open>A useful lemma allowing us to factor out the content size.\<close> |
2639 |
2639 |
2640 lemma has_integral_factor_content: |
2640 lemma has_integral_factor_content: |
2641 "(f has_integral i) (cbox a b) \<longleftrightarrow> |
2641 "(f has_integral i) (cbox a b) \<longleftrightarrow> |
2642 (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
2642 (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
2643 norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content (cbox a b)))" |
2643 norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content (cbox a b)))" |
2644 proof (cases "content (cbox a b) = 0") |
2644 proof (cases "content (cbox a b) = 0") |
2645 case True |
2645 case True |
2646 show ?thesis |
2646 show ?thesis |
2647 unfolding has_integral_null_eq[OF True] |
2647 unfolding has_integral_null_eq[OF True] |
2648 apply safe |
2648 apply safe |
2649 apply (rule, rule, rule gauge_trivial, safe) |
2649 apply (rule, rule, rule gauge_trivial, safe) |
2650 unfolding setsum_content_null[OF True] True |
2650 unfolding sum_content_null[OF True] True |
2651 defer |
2651 defer |
2652 apply (erule_tac x=1 in allE) |
2652 apply (erule_tac x=1 in allE) |
2653 apply safe |
2653 apply safe |
2654 defer |
2654 defer |
2655 apply (rule fine_division_exists[of _ a b]) |
2655 apply (rule fine_division_exists[of _ a b]) |
2656 apply assumption |
2656 apply assumption |
2657 apply (erule_tac x=p in allE) |
2657 apply (erule_tac x=p in allE) |
2658 unfolding setsum_content_null[OF True] |
2658 unfolding sum_content_null[OF True] |
2659 apply auto |
2659 apply auto |
2660 done |
2660 done |
2661 next |
2661 next |
2662 case False |
2662 case False |
2663 note F = this[unfolded content_lt_nz[symmetric]] |
2663 note F = this[unfolded content_lt_nz[symmetric]] |
2694 qed |
2694 qed |
2695 |
2695 |
2696 lemma has_integral_factor_content_real: |
2696 lemma has_integral_factor_content_real: |
2697 "(f has_integral i) {a .. b::real} \<longleftrightarrow> |
2697 "(f has_integral i) {a .. b::real} \<longleftrightarrow> |
2698 (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow> |
2698 (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow> |
2699 norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content {a .. b} ))" |
2699 norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content {a .. b} ))" |
2700 unfolding box_real[symmetric] |
2700 unfolding box_real[symmetric] |
2701 by (rule has_integral_factor_content) |
2701 by (rule has_integral_factor_content) |
2702 |
2702 |
2703 |
2703 |
2704 subsection \<open>Fundamental theorem of calculus.\<close> |
2704 subsection \<open>Fundamental theorem of calculus.\<close> |
2736 fix p |
2736 fix p |
2737 assume as: "p tagged_division_of cbox a b" "(\<lambda>x. ball x (d x)) fine p" |
2737 assume as: "p tagged_division_of cbox a b" "(\<lambda>x. ball x (d x)) fine p" |
2738 show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b)" |
2738 show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b)" |
2739 unfolding content_real[OF assms(1), simplified box_real[symmetric]] additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of f,symmetric] |
2739 unfolding content_real[OF assms(1), simplified box_real[symmetric]] additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of f,symmetric] |
2740 unfolding additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of "\<lambda>x. x",symmetric] |
2740 unfolding additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of "\<lambda>x. x",symmetric] |
2741 unfolding setsum_distrib_left |
2741 unfolding sum_distrib_left |
2742 defer |
2742 defer |
2743 unfolding setsum_subtractf[symmetric] |
2743 unfolding sum_subtractf[symmetric] |
2744 proof (rule setsum_norm_le,safe) |
2744 proof (rule sum_norm_le,safe) |
2745 fix x k |
2745 fix x k |
2746 assume "(x, k) \<in> p" |
2746 assume "(x, k) \<in> p" |
2747 note xk = tagged_division_ofD(2-4)[OF as(1) this] |
2747 note xk = tagged_division_ofD(2-4)[OF as(1) this] |
2748 from this(3) guess u v by (elim exE) note k=this |
2748 from this(3) guess u v by (elim exE) note k=this |
2749 have *: "u \<le> v" |
2749 have *: "u \<le> v" |
2833 let ?f = "\<lambda>i. (-1) ^ i *\<^sub>R (prod (Df i t) (Dg ((p - i)) t))" |
2833 let ?f = "\<lambda>i. (-1) ^ i *\<^sub>R (prod (Df i t) (Dg ((p - i)) t))" |
2834 have "(\<Sum>i<p. (-1) ^ i *\<^sub>R (prod (Df i t) (Dg (Suc (p - Suc i)) t) + |
2834 have "(\<Sum>i<p. (-1) ^ i *\<^sub>R (prod (Df i t) (Dg (Suc (p - Suc i)) t) + |
2835 prod (Df (Suc i) t) (Dg (p - Suc i) t))) = |
2835 prod (Df (Suc i) t) (Dg (p - Suc i) t))) = |
2836 (\<Sum>i\<le>(Suc p'). ?f i - ?f (Suc i))" |
2836 (\<Sum>i\<le>(Suc p'). ?f i - ?f (Suc i))" |
2837 by (auto simp: algebra_simps p'(2) numeral_2_eq_2 * lessThan_Suc_atMost) |
2837 by (auto simp: algebra_simps p'(2) numeral_2_eq_2 * lessThan_Suc_atMost) |
2838 also note setsum_telescope |
2838 also note sum_telescope |
2839 finally |
2839 finally |
2840 have "(\<Sum>i<p. (-1) ^ i *\<^sub>R (prod (Df i t) (Dg (Suc (p - Suc i)) t) + |
2840 have "(\<Sum>i<p. (-1) ^ i *\<^sub>R (prod (Df i t) (Dg (Suc (p - Suc i)) t) + |
2841 prod (Df (Suc i) t) (Dg (p - Suc i) t))) |
2841 prod (Df (Suc i) t) (Dg (p - Suc i) t))) |
2842 = prod (f t) (Dg p t) - (- 1) ^ p *\<^sub>R prod (Df p t) (g t)" |
2842 = prod (f t) (Dg p t) - (- 1) ^ p *\<^sub>R prod (Df p t) (g t)" |
2843 unfolding p'[symmetric] |
2843 unfolding p'[symmetric] |
2882 have Dg: "\<And>m t. m < p \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> |
2882 have Dg: "\<And>m t. m < p \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> |
2883 (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a .. b})" |
2883 (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a .. b})" |
2884 unfolding Dg_def |
2884 unfolding Dg_def |
2885 by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def fact_eq divide_simps) |
2885 by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def fact_eq divide_simps) |
2886 let ?sum = "\<lambda>t. \<Sum>i<p. (- 1) ^ i *\<^sub>R Dg i t *\<^sub>R Df (p - Suc i) t" |
2886 let ?sum = "\<lambda>t. \<Sum>i<p. (- 1) ^ i *\<^sub>R Dg i t *\<^sub>R Df (p - Suc i) t" |
2887 from setsum_prod_derivatives_has_vector_derivative[of _ Dg _ _ _ Df, |
2887 from sum_prod_derivatives_has_vector_derivative[of _ Dg _ _ _ Df, |
2888 OF \<open>p > 0\<close> g0 Dg f0 Df] |
2888 OF \<open>p > 0\<close> g0 Dg f0 Df] |
2889 have deriv: "\<And>t. a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> |
2889 have deriv: "\<And>t. a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> |
2890 (?sum has_vector_derivative |
2890 (?sum has_vector_derivative |
2891 g t *\<^sub>R Df p t - (- 1) ^ p *\<^sub>R Dg p t *\<^sub>R f t) (at t within {a..b})" |
2891 g t *\<^sub>R Df p t - (- 1) ^ p *\<^sub>R Dg p t *\<^sub>R f t) (at t within {a..b})" |
2892 by auto |
2892 by auto |
2901 using \<open>p > 0\<close> |
2901 using \<open>p > 0\<close> |
2902 by (auto simp: power_mult_distrib[symmetric]) |
2902 by (auto simp: power_mult_distrib[symmetric]) |
2903 then have "?sum b = f b" |
2903 then have "?sum b = f b" |
2904 using Suc_pred'[OF \<open>p > 0\<close>] |
2904 using Suc_pred'[OF \<open>p > 0\<close>] |
2905 by (simp add: diff_eq_eq Dg_def power_0_left le_Suc_eq if_distrib |
2905 by (simp add: diff_eq_eq Dg_def power_0_left le_Suc_eq if_distrib |
2906 cond_application_beta setsum.If_cases f0) |
2906 cond_application_beta sum.If_cases f0) |
2907 also |
2907 also |
2908 have "{..<p} = (\<lambda>x. p - x - 1) ` {..<p}" |
2908 have "{..<p} = (\<lambda>x. p - x - 1) ` {..<p}" |
2909 proof safe |
2909 proof safe |
2910 fix x |
2910 fix x |
2911 assume "x < p" |
2911 assume "x < p" |
2912 thus "x \<in> (\<lambda>x. p - x - 1) ` {..<p}" |
2912 thus "x \<in> (\<lambda>x. p - x - 1) ` {..<p}" |
2913 by (auto intro!: image_eqI[where x = "p - x - 1"]) |
2913 by (auto intro!: image_eqI[where x = "p - x - 1"]) |
2914 qed simp |
2914 qed simp |
2915 from _ this |
2915 from _ this |
2916 have "?sum a = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)" |
2916 have "?sum a = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)" |
2917 by (rule setsum.reindex_cong) (auto simp add: inj_on_def Dg_def one) |
2917 by (rule sum.reindex_cong) (auto simp add: inj_on_def Dg_def one) |
2918 finally show c: ?case . |
2918 finally show c: ?case . |
2919 case 2 show ?case using c integral_unique by force |
2919 case 2 show ?case using c integral_unique by force |
2920 case 3 show ?case using c by force |
2920 case 3 show ?case using c by force |
2921 qed |
2921 qed |
2922 |
2922 |
3001 by (auto elim!: ballE[of _ _ i]) |
3001 by (auto elim!: ballE[of _ _ i]) |
3002 then show "y \<noteq> x" |
3002 then show "y \<noteq> x" |
3003 unfolding euclidean_eq_iff[where 'a='a] using i by auto |
3003 unfolding euclidean_eq_iff[where 'a='a] using i by auto |
3004 have *: "Basis = insert i (Basis - {i})" |
3004 have *: "Basis = insert i (Basis - {i})" |
3005 using i by auto |
3005 using i by auto |
3006 have "norm (y - x) < e + setsum (\<lambda>i. 0) Basis" |
3006 have "norm (y - x) < e + sum (\<lambda>i. 0) Basis" |
3007 apply (rule le_less_trans[OF norm_le_l1]) |
3007 apply (rule le_less_trans[OF norm_le_l1]) |
3008 apply (subst *) |
3008 apply (subst *) |
3009 apply (subst setsum.insert) |
3009 apply (subst sum.insert) |
3010 prefer 3 |
3010 prefer 3 |
3011 apply (rule add_less_le_mono) |
3011 apply (rule add_less_le_mono) |
3012 proof - |
3012 proof - |
3013 show "\<bar>(y - x) \<bullet> i\<bar> < e" |
3013 show "\<bar>(y - x) \<bullet> i\<bar> < e" |
3014 using di as(2) y_def i xi by (auto simp: inner_simps) |
3014 using di as(2) y_def i xi by (auto simp: inner_simps) |
3434 note ** = d(2)[OF this] |
3434 note ** = d(2)[OF this] |
3435 have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p" |
3435 have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p" |
3436 using inj(1) unfolding inj_on_def by fastforce |
3436 using inj(1) unfolding inj_on_def by fastforce |
3437 have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") |
3437 have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") |
3438 using assms(7) |
3438 using assms(7) |
3439 apply (simp only: algebra_simps add_left_cancel scaleR_right.setsum) |
3439 apply (simp only: algebra_simps add_left_cancel scaleR_right.sum) |
3440 apply (subst setsum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p]) |
3440 apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p]) |
3441 apply (auto intro!: * setsum.cong simp: bij_betw_def dest!: p(4)) |
3441 apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4)) |
3442 done |
3442 done |
3443 also have "\<dots> = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") |
3443 also have "\<dots> = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") |
3444 unfolding scaleR_diff_right scaleR_scaleR |
3444 unfolding scaleR_diff_right scaleR_scaleR |
3445 using assms(1) |
3445 using assms(1) |
3446 by auto |
3446 by auto |
3863 using as by auto |
3863 using as by auto |
3864 note * = additive_tagged_division_1'[OF assms(1) as(1), symmetric] |
3864 note * = additive_tagged_division_1'[OF assms(1) as(1), symmetric] |
3865 have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2" |
3865 have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2" |
3866 by arith |
3866 by arith |
3867 show ?case |
3867 show ?case |
3868 unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] setsum_subtractf[symmetric] split_minus |
3868 unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] sum_subtractf[symmetric] split_minus |
3869 unfolding setsum_distrib_left |
3869 unfolding sum_distrib_left |
3870 apply (subst(2) pA) |
3870 apply (subst(2) pA) |
3871 apply (subst pA) |
3871 apply (subst pA) |
3872 unfolding setsum.union_disjoint[OF pA(2-)] |
3872 unfolding sum.union_disjoint[OF pA(2-)] |
3873 proof (rule norm_triangle_le, rule **, goal_cases) |
3873 proof (rule norm_triangle_le, rule **, goal_cases) |
3874 case 1 |
3874 case 1 |
3875 show ?case |
3875 show ?case |
3876 apply (rule order_trans) |
3876 apply (rule order_trans) |
3877 apply (rule setsum_norm_le) |
3877 apply (rule sum_norm_le) |
3878 defer |
3878 defer |
3879 apply (subst setsum_divide_distrib) |
3879 apply (subst sum_divide_distrib) |
3880 apply (rule order_refl) |
3880 apply (rule order_refl) |
3881 apply safe |
3881 apply safe |
3882 apply (unfold not_le o_def split_conv fst_conv) |
3882 apply (unfold not_le o_def split_conv fst_conv) |
3883 proof (rule ccontr) |
3883 proof (rule ccontr) |
3884 fix x k |
3884 fix x k |
3928 have *: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2" |
3928 have *: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2" |
3929 by auto |
3929 by auto |
3930 case 2 |
3930 case 2 |
3931 show ?case |
3931 show ?case |
3932 apply (rule *) |
3932 apply (rule *) |
3933 apply (rule setsum_nonneg) |
3933 apply (rule sum_nonneg) |
3934 apply rule |
3934 apply rule |
3935 apply (unfold split_paired_all split_conv) |
3935 apply (unfold split_paired_all split_conv) |
3936 defer |
3936 defer |
3937 unfolding setsum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric] |
3937 unfolding sum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric] |
3938 unfolding setsum_distrib_left[symmetric] |
3938 unfolding sum_distrib_left[symmetric] |
3939 apply (subst additive_tagged_division_1[OF _ as(1)]) |
3939 apply (subst additive_tagged_division_1[OF _ as(1)]) |
3940 apply (rule assms) |
3940 apply (rule assms) |
3941 proof - |
3941 proof - |
3942 fix x k |
3942 fix x k |
3943 assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}}" |
3943 assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}}" |
3946 with p(2)[OF xk] have "cbox u v \<noteq> {}" |
3946 with p(2)[OF xk] have "cbox u v \<noteq> {}" |
3947 by auto |
3947 by auto |
3948 then show "0 \<le> e * ((Sup k) - (Inf k))" |
3948 then show "0 \<le> e * ((Sup k) - (Inf k))" |
3949 unfolding uv using e by (auto simp add: field_simps) |
3949 unfolding uv using e by (auto simp add: field_simps) |
3950 next |
3950 next |
3951 have *: "\<And>s f t e. setsum f s = setsum f t \<Longrightarrow> norm (setsum f t) \<le> e \<Longrightarrow> norm (setsum f s) \<le> e" |
3951 have *: "\<And>s f t e. sum f s = sum f t \<Longrightarrow> norm (sum f t) \<le> e \<Longrightarrow> norm (sum f s) \<le> e" |
3952 by auto |
3952 by auto |
3953 show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - |
3953 show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - |
3954 (f ((Sup k)) - f ((Inf k)))) \<le> e * (b - a) / 2" |
3954 (f ((Sup k)) - f ((Inf k)))) \<le> e * (b - a) / 2" |
3955 apply (rule *[where t1="p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0}"]) |
3955 apply (rule *[where t1="p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0}"]) |
3956 apply (rule setsum.mono_neutral_right[OF pA(2)]) |
3956 apply (rule sum.mono_neutral_right[OF pA(2)]) |
3957 defer |
3957 defer |
3958 apply rule |
3958 apply rule |
3959 unfolding split_paired_all split_conv o_def |
3959 unfolding split_paired_all split_conv o_def |
3960 proof goal_cases |
3960 proof goal_cases |
3961 fix x k |
3961 fix x k |
3973 using xk unfolding uv by auto |
3973 using xk unfolding uv by auto |
3974 next |
3974 next |
3975 have *: "p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0} = |
3975 have *: "p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0} = |
3976 {t. t\<in>p \<and> fst t = a \<and> content(snd t) \<noteq> 0} \<union> {t. t\<in>p \<and> fst t = b \<and> content(snd t) \<noteq> 0}" |
3976 {t. t\<in>p \<and> fst t = a \<and> content(snd t) \<noteq> 0} \<union> {t. t\<in>p \<and> fst t = b \<and> content(snd t) \<noteq> 0}" |
3977 by blast |
3977 by blast |
3978 have **: "norm (setsum f s) \<le> e" |
3978 have **: "norm (sum f s) \<le> e" |
3979 if "\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y" |
3979 if "\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y" |
3980 and "\<forall>x. x \<in> s \<longrightarrow> norm (f x) \<le> e" |
3980 and "\<forall>x. x \<in> s \<longrightarrow> norm (f x) \<le> e" |
3981 and "e > 0" |
3981 and "e > 0" |
3982 for s f and e :: real |
3982 for s f and e :: real |
3983 proof (cases "s = {}") |
3983 proof (cases "s = {}") |
5001 proof |
5001 proof |
5002 fix x i |
5002 fix x i |
5003 show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm x \<le> B" and "i \<in> Basis" |
5003 show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm x \<le> B" and "i \<in> Basis" |
5004 using that and Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x] |
5004 using that and Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x] |
5005 unfolding c_def d_def |
5005 unfolding c_def d_def |
5006 by (auto simp add: field_simps setsum_negf) |
5006 by (auto simp add: field_simps sum_negf) |
5007 qed |
5007 qed |
5008 have "ball 0 C \<subseteq> cbox c d" |
5008 have "ball 0 C \<subseteq> cbox c d" |
5009 apply (rule subsetI) |
5009 apply (rule subsetI) |
5010 unfolding mem_box mem_ball dist_norm |
5010 unfolding mem_box mem_ball dist_norm |
5011 proof |
5011 proof |
5012 fix x i :: 'n |
5012 fix x i :: 'n |
5013 assume x: "norm (0 - x) < C" and i: "i \<in> Basis" |
5013 assume x: "norm (0 - x) < C" and i: "i \<in> Basis" |
5014 show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" |
5014 show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" |
5015 using Basis_le_norm[OF i, of x] and x i |
5015 using Basis_le_norm[OF i, of x] and x i |
5016 unfolding c_def d_def |
5016 unfolding c_def d_def |
5017 by (auto simp: setsum_negf) |
5017 by (auto simp: sum_negf) |
5018 qed |
5018 qed |
5019 from C(2)[OF this] have "\<exists>y. (f has_integral y) (cbox a b)" |
5019 from C(2)[OF this] have "\<exists>y. (f has_integral y) (cbox a b)" |
5020 unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,symmetric] |
5020 unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,symmetric] |
5021 unfolding s |
5021 unfolding s |
5022 by auto |
5022 by auto |
5038 fix x i :: 'n |
5038 fix x i :: 'n |
5039 assume "norm x \<le> B" and "i \<in> Basis" |
5039 assume "norm x \<le> B" and "i \<in> Basis" |
5040 then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" |
5040 then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" |
5041 using Basis_le_norm[of i x] |
5041 using Basis_le_norm[of i x] |
5042 unfolding c_def d_def |
5042 unfolding c_def d_def |
5043 by (auto simp add: field_simps setsum_negf) |
5043 by (auto simp add: field_simps sum_negf) |
5044 qed |
5044 qed |
5045 have "ball 0 C \<subseteq> cbox c d" |
5045 have "ball 0 C \<subseteq> cbox c d" |
5046 apply (rule subsetI) |
5046 apply (rule subsetI) |
5047 unfolding mem_box mem_ball dist_norm |
5047 unfolding mem_box mem_ball dist_norm |
5048 proof |
5048 proof |
5049 fix x i :: 'n |
5049 fix x i :: 'n |
5050 assume "norm (0 - x) < C" and "i \<in> Basis" |
5050 assume "norm (0 - x) < C" and "i \<in> Basis" |
5051 then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" |
5051 then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" |
5052 using Basis_le_norm[of i x] |
5052 using Basis_le_norm[of i x] |
5053 unfolding c_def d_def |
5053 unfolding c_def d_def |
5054 by (auto simp: setsum_negf) |
5054 by (auto simp: sum_negf) |
5055 qed |
5055 qed |
5056 note C(2)[OF this] then guess z .. note z = conjunctD2[OF this, unfolded s] |
5056 note C(2)[OF this] then guess z .. note z = conjunctD2[OF this, unfolded s] |
5057 note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]] |
5057 note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]] |
5058 then have "z = y" and "norm (z - i) < norm (y - i)" |
5058 then have "z = y" and "norm (z - i) < norm (y - i)" |
5059 apply - |
5059 apply - |
5539 |
5539 |
5540 have "(\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R g x) \<ge> 0" |
5540 have "(\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R g x) \<ge> 0" |
5541 and "0 \<le> (\<Sum>(x, k)\<in>p2. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)" |
5541 and "0 \<le> (\<Sum>(x, k)\<in>p2. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)" |
5542 and "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0" |
5542 and "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0" |
5543 and "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)" |
5543 and "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)" |
5544 unfolding setsum_subtractf[symmetric] |
5544 unfolding sum_subtractf[symmetric] |
5545 apply - |
5545 apply - |
5546 apply (rule_tac[!] setsum_nonneg) |
5546 apply (rule_tac[!] sum_nonneg) |
5547 apply safe |
5547 apply safe |
5548 unfolding real_scaleR_def right_diff_distrib[symmetric] |
5548 unfolding real_scaleR_def right_diff_distrib[symmetric] |
5549 apply (rule_tac[!] mult_nonneg_nonneg) |
5549 apply (rule_tac[!] mult_nonneg_nonneg) |
5550 proof - |
5550 proof - |
5551 fix a b |
5551 fix a b |
5772 lemma has_integral_unions: |
5772 lemma has_integral_unions: |
5773 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5773 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5774 assumes "finite t" |
5774 assumes "finite t" |
5775 and "\<forall>s\<in>t. (f has_integral (i s)) s" |
5775 and "\<forall>s\<in>t. (f has_integral (i s)) s" |
5776 and "\<forall>s\<in>t. \<forall>s'\<in>t. s \<noteq> s' \<longrightarrow> negligible (s \<inter> s')" |
5776 and "\<forall>s\<in>t. \<forall>s'\<in>t. s \<noteq> s' \<longrightarrow> negligible (s \<inter> s')" |
5777 shows "(f has_integral (setsum i t)) (\<Union>t)" |
5777 shows "(f has_integral (sum i t)) (\<Union>t)" |
5778 proof - |
5778 proof - |
5779 note * = has_integral_restrict_univ[symmetric, of f] |
5779 note * = has_integral_restrict_univ[symmetric, of f] |
5780 have **: "negligible (\<Union>((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> t \<and> b \<in> {y. y \<in> t \<and> a \<noteq> y}}))" |
5780 have **: "negligible (\<Union>((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> t \<and> b \<in> {y. y \<in> t \<and> a \<noteq> y}}))" |
5781 apply (rule negligible_Union) |
5781 apply (rule negligible_Union) |
5782 apply (rule finite_imageI) |
5782 apply (rule finite_imageI) |
5852 |
5852 |
5853 lemma integral_combine_division_bottomup: |
5853 lemma integral_combine_division_bottomup: |
5854 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5854 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5855 assumes "d division_of s" |
5855 assumes "d division_of s" |
5856 and "\<forall>k\<in>d. f integrable_on k" |
5856 and "\<forall>k\<in>d. f integrable_on k" |
5857 shows "integral s f = setsum (\<lambda>i. integral i f) d" |
5857 shows "integral s f = sum (\<lambda>i. integral i f) d" |
5858 apply (rule integral_unique) |
5858 apply (rule integral_unique) |
5859 apply (rule has_integral_combine_division[OF assms(1)]) |
5859 apply (rule has_integral_combine_division[OF assms(1)]) |
5860 using assms(2) |
5860 using assms(2) |
5861 unfolding has_integral_integral |
5861 unfolding has_integral_integral |
5862 apply assumption |
5862 apply assumption |
5865 lemma has_integral_combine_division_topdown: |
5865 lemma has_integral_combine_division_topdown: |
5866 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5866 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5867 assumes "f integrable_on s" |
5867 assumes "f integrable_on s" |
5868 and "d division_of k" |
5868 and "d division_of k" |
5869 and "k \<subseteq> s" |
5869 and "k \<subseteq> s" |
5870 shows "(f has_integral (setsum (\<lambda>i. integral i f) d)) k" |
5870 shows "(f has_integral (sum (\<lambda>i. integral i f) d)) k" |
5871 apply (rule has_integral_combine_division[OF assms(2)]) |
5871 apply (rule has_integral_combine_division[OF assms(2)]) |
5872 apply safe |
5872 apply safe |
5873 unfolding has_integral_integral[symmetric] |
5873 unfolding has_integral_integral[symmetric] |
5874 proof goal_cases |
5874 proof goal_cases |
5875 case (1 k) |
5875 case (1 k) |
5939 apply (intro has_integral_combine_division) |
5939 apply (intro has_integral_combine_division) |
5940 apply (auto simp: has_integral_integral[symmetric] intro: division_of_tagged_division[OF assms(1)]) |
5940 apply (auto simp: has_integral_integral[symmetric] intro: division_of_tagged_division[OF assms(1)]) |
5941 apply auto |
5941 apply auto |
5942 done |
5942 done |
5943 also have "(\<Sum>k\<in>snd`p. integral k f) = (\<Sum>(x, k)\<in>p. integral k f)" |
5943 also have "(\<Sum>k\<in>snd`p. integral k f) = (\<Sum>(x, k)\<in>p. integral k f)" |
5944 by (intro setsum.over_tagged_division_lemma[OF assms(1), symmetric] integral_null) |
5944 by (intro sum.over_tagged_division_lemma[OF assms(1), symmetric] integral_null) |
5945 (simp add: content_eq_0_interior) |
5945 (simp add: content_eq_0_interior) |
5946 finally show ?thesis |
5946 finally show ?thesis |
5947 using assms by (auto simp add: has_integral_iff intro!: setsum.cong) |
5947 using assms by (auto simp add: has_integral_iff intro!: sum.cong) |
5948 qed |
5948 qed |
5949 |
5949 |
5950 lemma integral_combine_tagged_division_bottomup: |
5950 lemma integral_combine_tagged_division_bottomup: |
5951 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5951 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5952 assumes "p tagged_division_of (cbox a b)" |
5952 assumes "p tagged_division_of (cbox a b)" |
5953 and "\<forall>(x,k)\<in>p. f integrable_on k" |
5953 and "\<forall>(x,k)\<in>p. f integrable_on k" |
5954 shows "integral (cbox a b) f = setsum (\<lambda>(x,k). integral k f) p" |
5954 shows "integral (cbox a b) f = sum (\<lambda>(x,k). integral k f) p" |
5955 apply (rule integral_unique) |
5955 apply (rule integral_unique) |
5956 apply (rule has_integral_combine_tagged_division[OF assms(1)]) |
5956 apply (rule has_integral_combine_tagged_division[OF assms(1)]) |
5957 using assms(2) |
5957 using assms(2) |
5958 apply auto |
5958 apply auto |
5959 done |
5959 done |
5960 |
5960 |
5961 lemma has_integral_combine_tagged_division_topdown: |
5961 lemma has_integral_combine_tagged_division_topdown: |
5962 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5962 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5963 assumes "f integrable_on cbox a b" |
5963 assumes "f integrable_on cbox a b" |
5964 and "p tagged_division_of (cbox a b)" |
5964 and "p tagged_division_of (cbox a b)" |
5965 shows "(f has_integral (setsum (\<lambda>(x,k). integral k f) p)) (cbox a b)" |
5965 shows "(f has_integral (sum (\<lambda>(x,k). integral k f) p)) (cbox a b)" |
5966 apply (rule has_integral_combine_tagged_division[OF assms(2)]) |
5966 apply (rule has_integral_combine_tagged_division[OF assms(2)]) |
5967 apply safe |
5967 apply safe |
5968 proof goal_cases |
5968 proof goal_cases |
5969 case 1 |
5969 case 1 |
5970 note tagged_division_ofD(3-4)[OF assms(2) this] |
5970 note tagged_division_ofD(3-4)[OF assms(2) this] |
5990 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5990 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
5991 assumes "f integrable_on cbox a b" |
5991 assumes "f integrable_on cbox a b" |
5992 and "e > 0" |
5992 and "e > 0" |
5993 and "gauge d" |
5993 and "gauge d" |
5994 and "(\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
5994 and "(\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
5995 norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral(cbox a b) f) < e)" |
5995 norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral(cbox a b) f) < e)" |
5996 and p: "p tagged_partial_division_of (cbox a b)" "d fine p" |
5996 and p: "p tagged_partial_division_of (cbox a b)" "d fine p" |
5997 shows "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" |
5997 shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" |
5998 (is "?x \<le> e") |
5998 (is "?x \<le> e") |
5999 proof - |
5999 proof - |
6000 { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" then show ?thesis by (blast intro: field_le_epsilon) } |
6000 { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" then show ?thesis by (blast intro: field_le_epsilon) } |
6001 fix k :: real |
6001 fix k :: real |
6002 assume k: "k > 0" |
6002 assume k: "k > 0" |
6122 using interior_mono[OF \<open>l \<subseteq> k\<close>] by blast |
6122 using interior_mono[OF \<open>l \<subseteq> k\<close>] by blast |
6123 then show "content l *\<^sub>R f x = 0" |
6123 then show "content l *\<^sub>R f x = 0" |
6124 unfolding uv content_eq_0_interior[symmetric] by auto |
6124 unfolding uv content_eq_0_interior[symmetric] by auto |
6125 qed auto |
6125 qed auto |
6126 |
6126 |
6127 then have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x)) |
6127 then have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + sum (sum (\<lambda>(x, k). content k *\<^sub>R f x)) |
6128 (qq ` r) - integral (cbox a b) f) < e" |
6128 (qq ` r) - integral (cbox a b) f) < e" |
6129 apply (subst (asm) setsum.Union_comp) |
6129 apply (subst (asm) sum.Union_comp) |
6130 prefer 2 |
6130 prefer 2 |
6131 unfolding split_paired_all split_conv image_iff |
6131 unfolding split_paired_all split_conv image_iff |
6132 apply (erule bexE)+ |
6132 apply (erule bexE)+ |
6133 proof - |
6133 proof - |
6134 fix x m k l T1 T2 |
6134 fix x m k l T1 T2 |
6148 then show "content m *\<^sub>R f x = 0" |
6148 then show "content m *\<^sub>R f x = 0" |
6149 unfolding uv content_eq_0_interior[symmetric] |
6149 unfolding uv content_eq_0_interior[symmetric] |
6150 by auto |
6150 by auto |
6151 qed (insert qq, auto) |
6151 qed (insert qq, auto) |
6152 |
6152 |
6153 then have **: "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r - |
6153 then have **: "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + sum (sum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r - |
6154 integral (cbox a b) f) < e" |
6154 integral (cbox a b) f) < e" |
6155 apply (subst (asm) setsum.reindex_nontrivial) |
6155 apply (subst (asm) sum.reindex_nontrivial) |
6156 apply fact |
6156 apply fact |
6157 apply (rule setsum.neutral) |
6157 apply (rule sum.neutral) |
6158 apply rule |
6158 apply rule |
6159 unfolding split_paired_all split_conv |
6159 unfolding split_paired_all split_conv |
6160 defer |
6160 defer |
6161 apply assumption |
6161 apply assumption |
6162 proof - |
6162 proof - |
6178 unfolding that(3)[symmetric] norm_minus_cancel |
6178 unfolding that(3)[symmetric] norm_minus_cancel |
6179 by (auto simp add: algebra_simps) |
6179 by (auto simp add: algebra_simps) |
6180 qed |
6180 qed |
6181 |
6181 |
6182 have "?x = norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))" |
6182 have "?x = norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))" |
6183 unfolding split_def setsum_subtractf .. |
6183 unfolding split_def sum_subtractf .. |
6184 also have "\<dots> \<le> e + k" |
6184 also have "\<dots> \<le> e + k" |
6185 apply (rule *[OF **, where ir1="setsum (\<lambda>k. integral k f) r"]) |
6185 apply (rule *[OF **, where ir1="sum (\<lambda>k. integral k f) r"]) |
6186 proof goal_cases |
6186 proof goal_cases |
6187 case 1 |
6187 case 1 |
6188 have *: "k * real (card r) / (1 + real (card r)) < k" |
6188 have *: "k * real (card r) / (1 + real (card r)) < k" |
6189 using k by (auto simp add: field_simps) |
6189 using k by (auto simp add: field_simps) |
6190 show ?case |
6190 show ?case |
6191 apply (rule le_less_trans[of _ "setsum (\<lambda>x. k / (real (card r) + 1)) r"]) |
6191 apply (rule le_less_trans[of _ "sum (\<lambda>x. k / (real (card r) + 1)) r"]) |
6192 unfolding setsum_subtractf[symmetric] |
6192 unfolding sum_subtractf[symmetric] |
6193 apply (rule setsum_norm_le) |
6193 apply (rule sum_norm_le) |
6194 apply rule |
6194 apply rule |
6195 apply (drule qq) |
6195 apply (drule qq) |
6196 defer |
6196 defer |
6197 unfolding divide_inverse setsum_distrib_right[symmetric] |
6197 unfolding divide_inverse sum_distrib_right[symmetric] |
6198 unfolding divide_inverse[symmetric] |
6198 unfolding divide_inverse[symmetric] |
6199 using * apply (auto simp add: field_simps) |
6199 using * apply (auto simp add: field_simps) |
6200 done |
6200 done |
6201 next |
6201 next |
6202 case 2 |
6202 case 2 |
6203 have *: "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)" |
6203 have *: "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)" |
6204 apply (subst setsum.reindex_nontrivial) |
6204 apply (subst sum.reindex_nontrivial) |
6205 apply fact |
6205 apply fact |
6206 unfolding split_paired_all snd_conv split_def o_def |
6206 unfolding split_paired_all snd_conv split_def o_def |
6207 proof - |
6207 proof - |
6208 fix x l y m |
6208 fix x l y m |
6209 assume as: "(x, l) \<in> p" "(y, m) \<in> p" "(x, l) \<noteq> (y, m)" "l = m" |
6209 assume as: "(x, l) \<in> p" "(y, m) \<in> p" "(x, l) \<noteq> (y, m)" "l = m" |
6231 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space" |
6231 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space" |
6232 assumes "f integrable_on cbox a b" |
6232 assumes "f integrable_on cbox a b" |
6233 and "e > 0" |
6233 and "e > 0" |
6234 and "gauge d" |
6234 and "gauge d" |
6235 and "\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
6235 and "\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
6236 norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral (cbox a b) f) < e" |
6236 norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral (cbox a b) f) < e" |
6237 and "p tagged_partial_division_of (cbox a b)" |
6237 and "p tagged_partial_division_of (cbox a b)" |
6238 and "d fine p" |
6238 and "d fine p" |
6239 shows "setsum (\<lambda>(x,k). norm (content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (DIM('n)) * e" |
6239 shows "sum (\<lambda>(x,k). norm (content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (DIM('n)) * e" |
6240 unfolding split_def |
6240 unfolding split_def |
6241 apply (rule setsum_norm_allsubsets_bound) |
6241 apply (rule sum_norm_allsubsets_bound) |
6242 defer |
6242 defer |
6243 apply (rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)]) |
6243 apply (rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)]) |
6244 apply safe |
6244 apply safe |
6245 apply (rule assms[rule_format,unfolded split_def]) |
6245 apply (rule assms[rule_format,unfolded split_def]) |
6246 defer |
6246 defer |
6258 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space" |
6258 fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space" |
6259 assumes "f integrable_on cbox a b" |
6259 assumes "f integrable_on cbox a b" |
6260 and "e > 0" |
6260 and "e > 0" |
6261 obtains d where "gauge d" |
6261 obtains d where "gauge d" |
6262 and "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
6262 and "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
6263 setsum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e" |
6263 sum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e" |
6264 proof - |
6264 proof - |
6265 have *: "e / (2 * (real DIM('n) + 1)) > 0" using assms(2) by simp |
6265 have *: "e / (2 * (real DIM('n) + 1)) > 0" using assms(2) by simp |
6266 from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this] |
6266 from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this] |
6267 guess d .. note d = conjunctD2[OF this] |
6267 guess d .. note d = conjunctD2[OF this] |
6268 show thesis |
6268 show thesis |
6285 text \<open>FIXME: Should one or more of these theorems be moved to |
6285 text \<open>FIXME: Should one or more of these theorems be moved to |
6286 \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close> |
6286 \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close> |
6287 |
6287 |
6288 lemma sum_gp_basic: |
6288 lemma sum_gp_basic: |
6289 fixes x :: "'a::ring_1" |
6289 fixes x :: "'a::ring_1" |
6290 shows "(1 - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))" |
6290 shows "(1 - x) * sum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))" |
6291 proof - |
6291 proof - |
6292 define y where "y = 1 - x" |
6292 define y where "y = 1 - x" |
6293 have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n" |
6293 have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n" |
6294 by (induct n) (simp_all add: algebra_simps) |
6294 by (induct n) (simp_all add: algebra_simps) |
6295 then show ?thesis |
6295 then show ?thesis |
6296 unfolding y_def by simp |
6296 unfolding y_def by simp |
6297 qed |
6297 qed |
6298 |
6298 |
6299 lemma sum_gp_multiplied: |
6299 lemma sum_gp_multiplied: |
6300 assumes mn: "m \<le> n" |
6300 assumes mn: "m \<le> n" |
6301 shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n" |
6301 shows "((1::'a::{field}) - x) * sum (op ^ x) {m..n} = x^m - x^ Suc n" |
6302 (is "?lhs = ?rhs") |
6302 (is "?lhs = ?rhs") |
6303 proof - |
6303 proof - |
6304 let ?S = "{0..(n - m)}" |
6304 let ?S = "{0..(n - m)}" |
6305 from mn have mn': "n - m \<ge> 0" |
6305 from mn have mn': "n - m \<ge> 0" |
6306 by arith |
6306 by arith |
6312 apply (auto simp add: image_iff Bex_def) |
6312 apply (auto simp add: image_iff Bex_def) |
6313 apply presburger |
6313 apply presburger |
6314 done |
6314 done |
6315 have th: "op ^ x \<circ> op + m = (\<lambda>i. x^m * x^i)" |
6315 have th: "op ^ x \<circ> op + m = (\<lambda>i. x^m * x^i)" |
6316 by (rule ext) (simp add: power_add power_mult) |
6316 by (rule ext) (simp add: power_add power_mult) |
6317 from setsum.reindex[OF i, of "op ^ x", unfolded f th setsum_distrib_left[symmetric]] |
6317 from sum.reindex[OF i, of "op ^ x", unfolded f th sum_distrib_left[symmetric]] |
6318 have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" |
6318 have "?lhs = x^m * ((1 - x) * sum (op ^ x) {0..n - m})" |
6319 by simp |
6319 by simp |
6320 then show ?thesis |
6320 then show ?thesis |
6321 unfolding sum_gp_basic |
6321 unfolding sum_gp_basic |
6322 using mn |
6322 using mn |
6323 by (simp add: field_simps power_add[symmetric]) |
6323 by (simp add: field_simps power_add[symmetric]) |
6324 qed |
6324 qed |
6325 |
6325 |
6326 lemma sum_gp: |
6326 lemma sum_gp: |
6327 "setsum (op ^ (x::'a::{field})) {m .. n} = |
6327 "sum (op ^ (x::'a::{field})) {m .. n} = |
6328 (if n < m then 0 |
6328 (if n < m then 0 |
6329 else if x = 1 then of_nat ((n + 1) - m) |
6329 else if x = 1 then of_nat ((n + 1) - m) |
6330 else (x^ m - x^ (Suc n)) / (1 - x))" |
6330 else (x^ m - x^ (Suc n)) / (1 - x))" |
6331 proof - |
6331 proof - |
6332 { |
6332 { |
6495 b="\<Sum>(x, k)\<in>p. content k *\<^sub>R f (m x) x" and c="\<Sum>(x, k)\<in>p. integral k (f (m x))"]) |
6495 b="\<Sum>(x, k)\<in>p. content k *\<^sub>R f (m x) x" and c="\<Sum>(x, k)\<in>p. integral k (f (m x))"]) |
6496 proof (safe, goal_cases) |
6496 proof (safe, goal_cases) |
6497 case 1 |
6497 case 1 |
6498 show ?case |
6498 show ?case |
6499 apply (rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content (cbox a b)))"]) |
6499 apply (rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content (cbox a b)))"]) |
6500 unfolding setsum_subtractf[symmetric] |
6500 unfolding sum_subtractf[symmetric] |
6501 apply (rule order_trans) |
6501 apply (rule order_trans) |
6502 apply (rule norm_setsum) |
6502 apply (rule norm_sum) |
6503 apply (rule setsum_mono) |
6503 apply (rule sum_mono) |
6504 unfolding split_paired_all split_conv |
6504 unfolding split_paired_all split_conv |
6505 unfolding split_def setsum_distrib_right[symmetric] scaleR_diff_right[symmetric] |
6505 unfolding split_def sum_distrib_right[symmetric] scaleR_diff_right[symmetric] |
6506 unfolding additive_content_tagged_division[OF p(1), unfolded split_def] |
6506 unfolding additive_content_tagged_division[OF p(1), unfolded split_def] |
6507 proof - |
6507 proof - |
6508 fix x k |
6508 fix x k |
6509 assume xk: "(x, k) \<in> p" |
6509 assume xk: "(x, k) \<in> p" |
6510 then have x: "x \<in> cbox a b" |
6510 then have x: "x \<in> cbox a b" |
6522 next |
6522 next |
6523 case 2 |
6523 case 2 |
6524 show ?case |
6524 show ?case |
6525 apply (rule le_less_trans[of _ "norm (\<Sum>j = 0..s. |
6525 apply (rule le_less_trans[of _ "norm (\<Sum>j = 0..s. |
6526 \<Sum>(x, k)\<in>{xk\<in>p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))"]) |
6526 \<Sum>(x, k)\<in>{xk\<in>p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))"]) |
6527 apply (subst setsum_group) |
6527 apply (subst sum_group) |
6528 apply fact |
6528 apply fact |
6529 apply (rule finite_atLeastAtMost) |
6529 apply (rule finite_atLeastAtMost) |
6530 defer |
6530 defer |
6531 apply (subst split_def)+ |
6531 apply (subst split_def)+ |
6532 unfolding setsum_subtractf |
6532 unfolding sum_subtractf |
6533 apply rule |
6533 apply rule |
6534 proof - |
6534 proof - |
6535 show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p. |
6535 show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p. |
6536 m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2" |
6536 m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2" |
6537 apply (rule le_less_trans[of _ "setsum (\<lambda>i. e / 2^(i+2)) {0..s}"]) |
6537 apply (rule le_less_trans[of _ "sum (\<lambda>i. e / 2^(i+2)) {0..s}"]) |
6538 apply (rule setsum_norm_le) |
6538 apply (rule sum_norm_le) |
6539 proof |
6539 proof |
6540 show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2" |
6540 show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2" |
6541 unfolding power_add divide_inverse inverse_mult_distrib |
6541 unfolding power_add divide_inverse inverse_mult_distrib |
6542 unfolding setsum_distrib_left[symmetric] setsum_distrib_right[symmetric] |
6542 unfolding sum_distrib_left[symmetric] sum_distrib_right[symmetric] |
6543 unfolding power_inverse [symmetric] sum_gp |
6543 unfolding power_inverse [symmetric] sum_gp |
6544 apply(rule mult_strict_left_mono[OF _ e]) |
6544 apply(rule mult_strict_left_mono[OF _ e]) |
6545 unfolding power2_eq_square |
6545 unfolding power2_eq_square |
6546 apply auto |
6546 apply auto |
6547 done |
6547 done |
6548 fix t |
6548 fix t |
6549 assume "t \<in> {0..s}" |
6549 assume "t \<in> {0..s}" |
6550 show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - |
6550 show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - |
6551 integral k (f (m x))) \<le> e / 2 ^ (t + 2)" |
6551 integral k (f (m x))) \<le> e / 2 ^ (t + 2)" |
6552 apply (rule order_trans |
6552 apply (rule order_trans |
6553 [of _ "norm (setsum (\<lambda>(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \<in> p. m (fst xk) = t})"]) |
6553 [of _ "norm (sum (\<lambda>(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \<in> p. m (fst xk) = t})"]) |
6554 apply (rule eq_refl) |
6554 apply (rule eq_refl) |
6555 apply (rule arg_cong[where f=norm]) |
6555 apply (rule arg_cong[where f=norm]) |
6556 apply (rule setsum.cong) |
6556 apply (rule sum.cong) |
6557 apply (rule refl) |
6557 apply (rule refl) |
6558 defer |
6558 defer |
6559 apply (rule henstock_lemma_part1) |
6559 apply (rule henstock_lemma_part1) |
6560 apply (rule assms(1)[rule_format]) |
6560 apply (rule assms(1)[rule_format]) |
6561 apply (simp add: e) |
6561 apply (simp add: e) |