# HG changeset patch # User wenzelm # Date 1434291722 -7200 # Node ID f316390b1c390bfeb7f78b714a0e28df786806cb # Parent e574accba10cc060684aa8b99e65455a07c33b63# Parent d0f8ff38e389cc742462a74bf43b4d086f369db9 merged diff -r d0f8ff38e389 -r f316390b1c39 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Sun Jun 14 16:18:00 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Sun Jun 14 16:22:02 2015 +0200 @@ -4137,28 +4137,27 @@ assumes "p division_of (cbox a b)" and "norm c \ e" shows "norm (setsum (\l. content l *\<^sub>R c) p) \ e * content(cbox a b)" - apply (rule order_trans) - apply (rule norm_setsum) - unfolding norm_scaleR setsum_left_distrib[symmetric] - apply (rule order_trans[OF mult_left_mono]) - apply (rule assms) - apply (rule setsum_abs_ge_zero) - apply (subst mult.commute) - apply (rule mult_left_mono) - apply (rule order_trans[of _ "setsum content p"]) - apply (rule eq_refl) - apply (rule setsum.cong) - apply (rule refl) - apply (subst abs_of_nonneg) - unfolding additive_content_division[OF assms(1)] -proof - - from order_trans[OF norm_ge_zero[of c] assms(2)] - show "0 \ e" . - fix x assume "x \ p" - from division_ofD(4)[OF assms(1) this] guess u v by (elim exE) - then show "0 \ content x" - using content_pos_le by auto -qed (insert assms, auto) +proof - + have sumeq: "(\i\p. \content i\) = setsum content p" + apply (rule setsum.cong) + using assms + apply simp + apply (metis abs_of_nonneg assms(1) content_pos_le division_ofD(4)) + done + have e: "0 \ e" + using assms(2) norm_ge_zero order_trans by blast + have "norm (setsum (\l. content l *\<^sub>R c) p) \ (\i\p. norm (content i *\<^sub>R c))" + using norm_setsum by blast + also have "... \ e * (\i\p. \content i\)" + apply (simp add: setsum_right_distrib[symmetric] mult.commute) + using assms(2) mult_right_mono by blast + also have "... \ e * content (cbox a b)" + apply (rule mult_left_mono [OF _ e]) + apply (simp add: sumeq) + using additive_content_division assms(1) eq_iff apply blast + done + finally show ?thesis . +qed lemma rsum_bound: assumes "p tagged_division_of (cbox a b)"