# HG changeset patch # User paulson # Date 1435668976 -3600 # Node ID e5fa1d5d3952e862f4068aa2bd7b69d410b143a2 # Parent 9627a75eb32ad4042a488beec90fb8542ce18f8a Useful lemmas. The theorem concerning swapping the variables in a double integral. diff -r 9627a75eb32a -r e5fa1d5d3952 src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Mon Jun 29 13:49:21 2015 +0200 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Jun 30 13:56:16 2015 +0100 @@ -302,10 +302,10 @@ lemma cSUP_upper2: "bdd_above (f ` A) \ x \ A \ u \ f x \ u \ SUPREMUM A f" by (auto intro: cSUP_upper assms order_trans) -lemma cSUP_const: "A \ {} \ (SUP x:A. c) = c" +lemma cSUP_const [simp]: "A \ {} \ (SUP x:A. c) = c" by (intro antisym cSUP_least) (auto intro: cSUP_upper) -lemma cINF_const: "A \ {} \ (INF x:A. c) = c" +lemma cINF_const [simp]: "A \ {} \ (INF x:A. c) = c" by (intro antisym cINF_greatest) (auto intro: cINF_lower) lemma le_cINF_iff: "A \ {} \ bdd_below (f ` A) \ u \ INFIMUM A f \ (\x\A. u \ f x)" @@ -634,4 +634,16 @@ by (elim exE disjE) auto qed +lemma cSUP_eq_cINF_D: + fixes f :: "_ \ 'b::conditionally_complete_lattice" + assumes eq: "(SUP x:A. f x) = (INF x:A. f x)" + and bdd: "bdd_above (f ` A)" "bdd_below (f ` A)" + and a: "a \ A" + shows "f a = (INF x:A. f x)" +apply (rule antisym) +using a bdd +apply (auto simp: cINF_lower) +apply (metis eq cSUP_upper) +done + end diff -r 9627a75eb32a -r e5fa1d5d3952 src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Mon Jun 29 13:49:21 2015 +0200 +++ b/src/HOL/Library/Product_Vector.thy Tue Jun 30 13:56:16 2015 +0100 @@ -213,6 +213,9 @@ lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \ continuous_on s g \ continuous_on s (\x. (f x, g x))" unfolding continuous_on_def by (auto intro: tendsto_Pair) +lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap" + by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id) + lemma isCont_fst [simp]: "isCont f a \ isCont (\x. fst (f x)) a" by (fact continuous_fst) @@ -254,6 +257,9 @@ by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd) qed +lemma isCont_swap[continuous_intros]: "isCont prod.swap a" + using continuous_on_eq_continuous_within continuous_on_swap by blast + subsection \Product is a metric space\ instantiation prod :: (metric_space, metric_space) metric_space @@ -439,15 +445,6 @@ using snd_add snd_scaleR by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) -text \TODO: move to NthRoot\ -lemma sqrt_add_le_add_sqrt: - assumes x: "0 \ x" and y: "0 \ y" - shows "sqrt (x + y) \ sqrt x + sqrt y" -apply (rule power2_le_imp_le) -apply (simp add: power2_sum x y) -apply (simp add: x y) -done - lemma bounded_linear_Pair: assumes f: "bounded_linear f" assumes g: "bounded_linear g" @@ -541,5 +538,11 @@ lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a" by (cases x, simp)+ +lemma + fixes x :: "'a::real_normed_vector" + shows norm_Pair1 [simp]: "norm (0,x) = norm x" + and norm_Pair2 [simp]: "norm (x,0) = norm x" +by (auto simp: norm_Pair) + end diff -r 9627a75eb32a -r e5fa1d5d3952 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Jun 29 13:49:21 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Jun 30 13:56:16 2015 +0100 @@ -394,7 +394,7 @@ then have "x \ s \ interior (\f)" unfolding lem1[where U="\f", symmetric] using centre_in_ball e by auto - then show ?thesis + then show ?thesis using insert.hyps(3) insert.prems(1) by blast qed qed @@ -445,7 +445,7 @@ using assms unfolding box_ne_empty by auto -lemma interval_upperbound_Times: +lemma interval_upperbound_Times: assumes "A \ {}" and "B \ {}" shows "interval_upperbound (A \ B) = (interval_upperbound A, interval_upperbound B)" proof- @@ -459,7 +459,7 @@ by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod) qed -lemma interval_lowerbound_Times: +lemma interval_lowerbound_Times: assumes "A \ {}" and "B \ {}" shows "interval_lowerbound (A \ B) = (interval_lowerbound A, interval_lowerbound B)" proof- @@ -505,7 +505,7 @@ then show ?thesis by (simp add: cbox_sing) qed -lemma content_unit[intro]: "content(cbox 0 (One::'a::euclidean_space)) = 1" +lemma content_unit[iff]: "content(cbox 0 (One::'a::euclidean_space)) = 1" proof - have *: "\i\Basis. (0::'a)\i \ (One::'a)\i" by auto @@ -532,6 +532,11 @@ finally show ?thesis . qed (simp add: content_def) +corollary content_nonneg [simp]: + fixes a::"'a::euclidean_space" + shows "~ content (cbox a b) < 0" +using not_le by blast + lemma content_pos_lt: fixes a :: "'a::euclidean_space" assumes "\i\Basis. a\i < b\i" @@ -607,7 +612,7 @@ let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound" let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound" assume nonempty: "A \ B \ {}" - hence "content (A \ B) = (\i\Basis. (?ub1 A, ?ub2 B) \ i - (?lb1 A, ?lb2 B) \ i)" + hence "content (A \ B) = (\i\Basis. (?ub1 A, ?ub2 B) \ i - (?lb1 A, ?lb2 B) \ i)" unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times) also have "... = content A * content B" unfolding content_def using nonempty apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp) @@ -616,6 +621,50 @@ finally show ?thesis . qed (auto simp: content_def) +lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)" + by (simp add: cbox_Pair_eq) + +lemma content_cbox_pair_eq0_D: + "content (cbox (a,c) (b,d)) = 0 \ content (cbox a b) = 0 \ content (cbox c d) = 0" + by (simp add: content_Pair) + +lemma content_eq_0_gen: + fixes s :: "'a::euclidean_space set" + assumes "bounded s" + shows "content s = 0 \ (\i\Basis. \v. \x \ s. x \ i = v)" (is "_ = ?rhs") +proof safe + assume "content s = 0" then show ?rhs + apply (clarsimp simp: ex_in_conv content_def split: split_if_asm) + apply (rule_tac x=a in bexI) + apply (rule_tac x="interval_lowerbound s \ a" in exI) + apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def) + apply (drule cSUP_eq_cINF_D) + apply (auto simp: bounded_inner_imp_bdd_above [OF assms] bounded_inner_imp_bdd_below [OF assms]) + done +next + fix i a + assume "i \ Basis" "\x\s. x \ i = a" + then show "content s = 0" + apply (clarsimp simp: content_def) + apply (rule_tac x=i in bexI) + apply (auto simp: interval_upperbound_def interval_lowerbound_def) + done +qed + +lemma content_0_subset_gen: + fixes a :: "'a::euclidean_space" + assumes "content t = 0" "s \ t" "bounded t" shows "content s = 0" +proof - + have "bounded s" + using assms by (metis bounded_subset) + then show ?thesis + using assms + by (auto simp: content_eq_0_gen) +qed + +lemma content_0_subset: "\content(cbox a b) = 0; s \ cbox a b\ \ content s = 0" + by (simp add: content_0_subset_gen bounded_cbox) + subsection \The notion of a gauge --- simply an open set containing the point.\ @@ -1104,7 +1153,7 @@ apply (rule division_disjoint_union[OF d assms(1)]) apply (rule inter_interior_unions_intervals) apply (rule p open_interior ballI)+ - apply simp_all + apply simp_all done qed then show ?thesis @@ -1162,7 +1211,7 @@ apply auto done finally have [simp]: "interior (cbox a b) \ interior (\(p - {cbox u v})) = {}" by simp - have cbe: "cbox a b \ cbox c d = cbox a b \ \(p - {cbox u v})" + have cbe: "cbox a b \ cbox c d = cbox a b \ \(p - {cbox u v})" using p(8) unfolding uv[symmetric] by auto show ?thesis apply (rule that[of "p - {cbox u v}"]) @@ -1221,7 +1270,7 @@ next assume as: "p \ {}" "interior (cbox a b) \ {}" "cbox a b \ {}" have "\k\p. \q. (insert (cbox a b) q) division_of (cbox a b \ k)" - proof + proof case goal1 from assm(4)[OF this] obtain c d where "k = cbox c d" by blast then show ?case @@ -1230,7 +1279,7 @@ from bchoice[OF this] obtain q where "\x\p. insert (cbox a b) (q x) division_of (cbox a b) \ x" .. note q = division_ofD[OF this[rule_format]] let ?D = "\{insert (cbox a b) (q k) | k. k \ p}" - show thesis + show thesis proof (rule that[OF division_ofI]) have *: "{insert (cbox a b) (q k) |k. k \ p} = (\k. insert (cbox a b) (q k)) ` p" by auto @@ -1858,7 +1907,7 @@ have "?A \ ?B" proof case goal1 - then obtain c d + then obtain c d where x: "x = cbox c d" "\i. i \ Basis \ c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ @@ -1934,7 +1983,7 @@ "x \ cbox c d" "\i. i \ Basis \ c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ - c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" + c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" by blast show "x\cbox a b" unfolding mem_box @@ -2160,7 +2209,7 @@ done obtain e where e: "e > 0" "ball x e \ g x" using gaugeD[OF assms, of x] unfolding open_contains_ball by auto - from x(2)[OF e(1)] + from x(2)[OF e(1)] obtain c d where c_d: "x \ cbox c d" "cbox c d \ ball x e" "cbox c d \ cbox a b" @@ -2346,7 +2395,7 @@ obtain B where B: "0 < B" "\x. norm (h x) \ norm x * B" by blast have "e / B > 0" using goal1(2) B by simp - then obtain g + then obtain g where g: "gauge g" "\p. p tagged_division_of (cbox a b) \ g fine p \ norm ((\(x, k)\p. content k *\<^sub>R f x) - y) < e / B" @@ -2404,7 +2453,7 @@ qed qed -lemma has_integral_scaleR_left: +lemma has_integral_scaleR_left: "(f has_integral y) s \ ((\x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s" using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def) @@ -2413,6 +2462,11 @@ shows "(f has_integral y) s \ ((\x. f x * c) has_integral (y * c)) s" using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def) +corollary integral_mult_left: + fixes c:: "'a::real_normed_algebra" + shows "f integrable_on s \ integral s (\x. f x * c) = integral s f * c" + by (blast intro: has_integral_mult_left) + lemma has_integral_cmul: "(f has_integral k) s \ ((\x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s" unfolding o_def[symmetric] by (metis has_integral_linear bounded_linear_scaleR_right) @@ -2478,7 +2532,7 @@ unfolding * by (auto simp add: algebra_simps) also have "\ < e/2 + e/2" apply (rule le_less_trans[OF norm_triangle_ineq]) - using as d1 d2 fine + using as d1 d2 fine apply (blast intro: add_strict_mono) done finally show "norm ((\(x, k)\p. content k *\<^sub>R (f x + g x)) - (k + l)) < e" @@ -2628,7 +2682,7 @@ done lemma has_integral_eq: - assumes "\x\s. f x = g x" + assumes "\x. x \ s \ f x = g x" and "(f has_integral k) s" shows "(g has_integral k) s" using has_integral_sub[OF assms(2), of "\x. f x - g x" 0] @@ -2636,16 +2690,23 @@ using assms(1) by auto -lemma integrable_eq: "\x\s. f x = g x \ f integrable_on s \ g integrable_on s" +lemma integrable_eq: "(\x. x \ s \ f x = g x) \ f integrable_on s \ g integrable_on s" unfolding integrable_on_def - using has_integral_eq[of s f g] + using has_integral_eq[of s f g] has_integral_eq by blast + +lemma has_integral_cong: + assumes "\x. x \ s \ f x = g x" + shows "(f has_integral i) s = (g has_integral i) s" + using has_integral_eq[of s f g] has_integral_eq[of s g f] assms by auto -lemma has_integral_eq_eq: "\x\s. f x = g x \ (f has_integral k) s \ (g has_integral k) s" - using has_integral_eq[of s f g] has_integral_eq[of s g f] - by auto - -lemma has_integral_null[dest]: +lemma integral_cong: + assumes "\x. x \ s \ f x = g x" + shows "integral s f = integral s g" + unfolding integral_def + by (metis assms has_integral_cong) + +lemma has_integral_null [intro]: assumes "content(cbox a b) = 0" shows "(f has_integral 0) (cbox a b)" proof - @@ -2667,7 +2728,7 @@ by (auto simp: has_integral) qed -lemma has_integral_null_real[dest]: +lemma has_integral_null_real [intro]: assumes "content {a .. b::real} = 0" shows "(f has_integral 0) {a .. b}" by (metis assms box_real(2) has_integral_null) @@ -2675,14 +2736,11 @@ lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \ (f has_integral i) (cbox a b) \ i = 0" by (auto simp add: has_integral_null dest!: integral_unique) -lemma integral_null[dest]: "content (cbox a b) = 0 \ integral (cbox a b) f = 0" +lemma integral_null [simp]: "content (cbox a b) = 0 \ integral (cbox a b) f = 0" by (metis has_integral_null integral_unique) -lemma integrable_on_null[dest]: "content (cbox a b) = 0 \ f integrable_on (cbox a b)" - unfolding integrable_on_def - apply (drule has_integral_null) - apply auto - done +lemma integrable_on_null [intro]: "content (cbox a b) = 0 \ f integrable_on (cbox a b)" + by (simp add: has_integral_integrable) lemma has_integral_empty[intro]: "(f has_integral 0) {}" by (simp add: has_integral_is_0) @@ -2798,7 +2856,7 @@ proof (rule_tac x=y in exI, clarify) fix e :: real assume "e>0" - then have *:"e/2 > 0" by auto + then have *:"e/2 > 0" by auto then guess N1 unfolding real_arch_inv[of "e/2"] .. note N1=this then have N1': "N1 = N1 - 1 + 1" by auto @@ -2818,7 +2876,7 @@ apply (rule norm_triangle_half_r) apply (rule less_trans[OF _ *]) apply (subst N1', rule d(2)[of "p (N1+N2)"]) - using N1' as(1) as(2) dp + using N1' as(1) as(2) dp apply (simp add: `\x. p x tagged_division_of cbox a b \ (\xa. \{d i xa |i. i \ {0..x}}) fine p x`) using N2 le_add2 by blast } @@ -2992,9 +3050,9 @@ assume "k \ ?p1" then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this guess u v using p(4)[OF l(2)] by (elim exE) note uv=this - show "k \ ?I1" + show "k \ ?I1" using l p(2) uv by force - show "k \ {}" + show "k \ {}" by (simp add: l) show "\a b. k = cbox a b" apply (simp add: l uv p(2-3)[OF l(2)]) @@ -3013,9 +3071,9 @@ assume "k \ ?p2" then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this guess u v using p(4)[OF l(2)] by (elim exE) note uv=this - show "k \ ?I2" + show "k \ ?I2" using l p(2) uv by force - show "k \ {}" + show "k \ {}" by (simp add: l) show "\a b. k = cbox a b" apply (simp add: l uv p(2-3)[OF l(2)]) @@ -3041,17 +3099,17 @@ case goal1 then have e: "e/2 > 0" by auto - obtain d1 + obtain d1 where d1: "gauge d1" - and d1norm: + and d1norm: "\p. \p tagged_division_of cbox a b \ {x. x \ k \ c}; d1 fine p\ \ norm ((\(x, k) \ p. content k *\<^sub>R f x) - i) < e / 2" apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e]) apply (simp add: interval_split[symmetric] k) done - obtain d2 + obtain d2 where d2: "gauge d2" - and d2norm: + and d2norm: "\p. \p tagged_division_of cbox a b \ {x. c \ x \ k}; d2 fine p\ \ norm ((\(x, k) \ p. content k *\<^sub>R f x) - j) < e / 2" apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e]) @@ -3077,12 +3135,12 @@ using p(2)[unfolded fine_def, rule_format,OF as] by auto with kk obtain y where y: "y \ ball x \x \ k - c\" "y\k \ c" by blast - then have "\x \ k - y \ k\ < \x \ k - c\" + then have "\x \ k - y \ k\ < \x \ k - c\" using Basis_le_norm[OF k, of "x - y"] by (auto simp add: dist_norm inner_diff_left intro: le_less_trans) with y show False using ** by (auto simp add: field_simps) - qed + qed qed have xk_ge_c: "\x kk. (x, kk) \ p \ kk \ {x. x\k \ c} \ {} \ x\k \ c" proof - @@ -3095,7 +3153,7 @@ using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto with kk obtain y where y: "y \ ball x \x \ k - c\" "y\k \ c" by blast - then have "\x \ k - y \ k\ < \x \ k - c\" + then have "\x \ k - y \ k\ < \x \ k - c\" using Basis_le_norm[OF k, of "x - y"] by (auto simp add: dist_norm inner_diff_left intro: le_less_trans) with y show False @@ -3104,7 +3162,7 @@ qed have lem1: "\f P Q. (\x k. (x, k) \ {(x, f k) | x k. P x k} \ Q x k) \ - (\x k. P x k \ Q x (f k))" + (\x k. P x k \ Q x (f k))" by auto have fin_finite: "\f s P f. finite s \ finite {(x,f k) | x k. (x,k) \ s \ P x k}" proof - @@ -3342,7 +3400,7 @@ also have "\ < e" by (rule k d(2) p12 fine_union p1 p2)+ finally have "norm ((\(x, k)\p1. content k *\<^sub>R f x) + (\(x, k)\p2. content k *\<^sub>R f x) - i) < e" . - } + } then show ?thesis by (auto intro: that[of d] d elim: ) qed @@ -3602,7 +3660,7 @@ fix a b :: 'a assume "content (cbox a b) = 0" then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0" - using has_integral_null_eq + using has_integral_null_eq by (auto simp: integrable_on_null) qed @@ -3723,7 +3781,7 @@ guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this have uv: "\i\Basis. u\i \ v\i" "\i\Basis. a\i \ u\i \ v\i \ b\i" using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty - using subset_box(1) + using subset_box(1) apply auto apply blast+ done @@ -3836,7 +3894,7 @@ qed lemma iterate_op: - "\monoidal opp; finite s\ + "\monoidal opp; finite s\ \ iterate opp s (\x. opp (f x) (g x)) = opp (iterate opp s f) (iterate opp s g)" by (erule finite_induct) (auto simp: monoidal_ac(4) monoidal_ac(5)) @@ -3857,13 +3915,13 @@ def su \ "support opp f s" have fsu: "finite su" using True by (simp add: su_def) - moreover + moreover { assume "finite su" "su \ s" then have "iterate opp su f = iterate opp su g" by (induct su) (auto simp: assms) } ultimately have "iterate opp (support opp f s) f = iterate opp (support opp g s) g" - by (simp add: "*" su_def support_subset) + by (simp add: "*" su_def support_subset) then show ?thesis by simp qed @@ -3884,17 +3942,17 @@ def C \ "card (division_points (cbox a b) d)" then show ?thesis using assms - proof (induct C arbitrary: a b d rule: full_nat_induct) + proof (induct C arbitrary: a b d rule: full_nat_induct) case (1 a b d) show ?case proof (cases "content (cbox a b) = 0") case True show "iterate opp d f = f (cbox a b)" unfolding operativeD(1)[OF assms(2) True] - proof (rule iterate_eq_neutral[OF `monoidal opp`]) + proof (rule iterate_eq_neutral[OF `monoidal opp`]) fix x assume x: "x \ d" - then show "f x = neutral opp" + then show "f x = neutral opp" by (metis division_ofD(4) 1(4) division_of_content_0[OF True] operativeD(1)[OF assms(2)] x) qed next @@ -3927,7 +3985,7 @@ then have d': "\i\d. \u v. i = cbox u v \ (\j\Basis. u\j = a\j \ v\j = a\j \ u\j = b\j \ v\j = b\j \ u\j = a\j \ v\j = b\j)" unfolding forall_in_division[OF 1(4)] - by blast + by blast have "(1/2) *\<^sub>R (a+b) \ cbox a b" unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps) note this[unfolded division_ofD(6)[OF `d division_of cbox a b`,symmetric] Union_iff] @@ -4004,7 +4062,7 @@ unfolding leq interval_split[OF kc(4)] apply (rule operativeD(1) 1)+ unfolding interval_split[symmetric,OF kc(4)] - using division_split_left_inj 1 as kc leq by blast + using division_split_left_inj 1 as kc leq by blast } note fxk_le = this { fix l y assume as: "l \ d" "y \ d" "l \ {x. c \ x \ k} = y \ {x. c \ x \ k}" "l \ y" @@ -4061,14 +4119,14 @@ proof - have *: "(\(x,l). f l) = f \ snd" unfolding o_def by rule auto note tagged = tagged_division_ofD[OF assms(3)] - { fix a b a' - assume as: "(a, b) \ d" "(a', b) \ d" "(a, b) \ (a', b)" + { fix a b a' + assume as: "(a, b) \ d" "(a', b) \ d" "(a, b) \ (a', b)" have "f b = neutral opp" - using tagged(4)[OF as(1)] + using tagged(4)[OF as(1)] apply clarify apply (rule operativeD(1)[OF assms(2)]) by (metis content_eq_0_interior inf.idem tagged_division_ofD(5)[OF assms(3) as(1-3)]) - } + } then have "iterate opp d (\(x,l). f l) = iterate opp (snd ` d) f" unfolding * by (force intro!: assms iterate_image_nonzero[symmetric, OF _ tagged_division_of_finite]) @@ -4184,7 +4242,7 @@ apply (rule mult_left_mono[OF _ abs_ge_zero, of _ e]) apply (metis norm) unfolding setsum_left_distrib[symmetric] - using con setsum_le + using con setsum_le apply (auto simp: mult.commute intro: mult_left_mono [OF _ e]) done finally show ?thesis . @@ -4219,13 +4277,21 @@ using d(2)[OF conjI[OF p]] *[OF rsum_bound[OF p(1) assms(3)]] by auto qed -lemma has_integral_bound_real: +corollary has_integral_bound_real: fixes f :: "real \ 'b::real_normed_vector" assumes "0 \ B" and "(f has_integral i) {a .. b}" and "\x\{a .. b}. norm (f x) \ B" shows "norm i \ B * content {a .. b}" - by (metis assms(1) assms(2) assms(3) box_real(2) has_integral_bound) + by (metis assms box_real(2) has_integral_bound) + +corollary integrable_bound: + fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" + assumes "0 \ B" + and "f integrable_on (cbox a b)" + and "\x. x\cbox a b \ norm (f x) \ B" + shows "norm (integral (cbox a b) f) \ B * content (cbox a b)" +by (metis integrable_integral has_integral_bound assms) subsection \Similar theorems about relationship among components.\ @@ -4244,7 +4310,7 @@ show "(content b *\<^sub>R f a) \ i \ (content b *\<^sub>R g a) \ i" unfolding b inner_simps real_scaleR_def apply (rule mult_left_mono) - using assms(2) tagged + using assms(2) tagged by (auto simp add: content_pos_le) qed @@ -4263,9 +4329,9 @@ by auto guess d1 using goal1(1)[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d1=this[rule_format] guess d2 using goal1(2)[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d2=this[rule_format] - obtain p where p: "p tagged_division_of cbox a b" "d1 fine p" "d2 fine p" - using fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] unfolding fine_inter - by metis + obtain p where p: "p tagged_division_of cbox a b" "d1 fine p" "d2 fine p" + using fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] unfolding fine_inter + by metis note le_less_trans[OF Basis_le_norm[OF k]] then have "\((\(x, k)\p. content k *\<^sub>R f x) - i) \ k\ < (i \ k - j \ k) / 3" "\((\(x, k)\p. content k *\<^sub>R g x) - j) \ k\ < (i \ k - j \ k) / 3" @@ -4423,7 +4489,7 @@ have *: "\