186 also have "\<dots> = 0" |
186 also have "\<dots> = 0" |
187 using assms(1) content_0_subset k(2) by auto |
187 using assms(1) content_0_subset k(2) by auto |
188 finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" . |
188 finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" . |
189 qed |
189 qed |
190 |
190 |
191 lemma operative_content[intro]: "add.operative content" |
191 global_interpretation sum_content: operative plus 0 content |
192 by (force simp add: add.operative_def content_split[symmetric] content_eq_0_interior) |
192 rewrites "comm_monoid_set.F plus 0 = sum" |
|
193 proof - |
|
194 interpret operative plus 0 content |
|
195 by standard (auto simp add: content_split [symmetric] content_eq_0_interior) |
|
196 show "operative plus 0 content" |
|
197 by standard |
|
198 show "comm_monoid_set.F plus 0 = sum" |
|
199 by (simp add: sum_def) |
|
200 qed |
193 |
201 |
194 lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> sum 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)" |
195 by (metis operative_content sum.operative_division) |
203 by (fact sum_content.division) |
196 |
204 |
197 lemma additive_content_tagged_division: |
205 lemma additive_content_tagged_division: |
198 "d tagged_division_of (cbox a b) \<Longrightarrow> sum (\<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)" |
199 unfolding sum.operative_tagged_division[OF operative_content, symmetric] by blast |
207 by (fact sum_content.tagged_division) |
200 |
208 |
201 lemma subadditive_content_division: |
209 lemma subadditive_content_division: |
202 assumes "\<D> division_of S" "S \<subseteq> cbox a b" |
210 assumes "\<D> division_of S" "S \<subseteq> cbox a b" |
203 shows "sum content \<D> \<le> content(cbox a b)" |
211 shows "sum content \<D> \<le> content(cbox a b)" |
204 proof - |
212 proof - |
1403 qed |
1411 qed |
1404 with f show ?thesis2 |
1412 with f show ?thesis2 |
1405 by (simp add: interval_split[OF k] integrable_Cauchy) |
1413 by (simp add: interval_split[OF k] integrable_Cauchy) |
1406 qed |
1414 qed |
1407 |
1415 |
1408 lemma operative_integral: |
1416 lemma operative_integralI: |
1409 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach" |
1417 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach" |
1410 shows "comm_monoid.operative (lift_option op +) (Some 0) |
1418 shows "operative (lift_option op +) (Some 0) |
1411 (\<lambda>i. if f integrable_on i then Some (integral i f) else None)" |
1419 (\<lambda>i. if f integrable_on i then Some (integral i f) else None)" |
1412 proof - |
1420 proof - |
1413 interpret comm_monoid "lift_option plus" "Some (0::'b)" |
1421 interpret comm_monoid "lift_option plus" "Some (0::'b)" |
1414 by (rule comm_monoid_lift_option) |
1422 by (rule comm_monoid_lift_option) |
1415 (rule add.comm_monoid_axioms) |
1423 (rule add.comm_monoid_axioms) |
1416 show ?thesis |
1424 show ?thesis |
1417 proof (unfold operative_def, safe) |
1425 proof |
1418 fix a b c |
1426 fix a b c |
1419 fix k :: 'a |
1427 fix k :: 'a |
1420 assume k: "k \<in> Basis" |
1428 assume k: "k \<in> Basis" |
1421 show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = |
1429 show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = |
1422 lift_option op + (if f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None) |
1430 lift_option op + (if f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None) |
2456 by auto |
2464 by auto |
2457 |
2465 |
2458 |
2466 |
2459 subsection \<open>Integrability of continuous functions.\<close> |
2467 subsection \<open>Integrability of continuous functions.\<close> |
2460 |
2468 |
2461 lemma operative_approximable: |
2469 lemma operative_approximableI: |
2462 fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach" |
2470 fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach" |
2463 assumes "0 \<le> e" |
2471 assumes "0 \<le> e" |
2464 shows "comm_monoid.operative op \<and> True (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)" |
2472 shows "operative conj True (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)" |
2465 unfolding comm_monoid.operative_def[OF comm_monoid_and] |
2473 proof - |
2466 proof safe |
2474 interpret comm_monoid conj True |
2467 fix a b :: 'b |
2475 by standard auto |
2468 show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b" |
2476 show ?thesis |
2469 if "box a b = {}" for a b |
2477 proof (standard, safe) |
2470 apply (rule_tac x=f in exI) |
2478 fix a b :: 'b |
2471 using assms that by (auto simp: content_eq_0_interior) |
|
2472 { |
|
2473 fix c g and k :: 'b |
|
2474 assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b" |
|
2475 assume k: "k \<in> Basis" |
|
2476 show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" |
|
2477 "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}" |
|
2478 apply (rule_tac[!] x=g in exI) |
|
2479 using fg integrable_split[OF g k] by auto |
|
2480 } |
|
2481 show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b" |
|
2482 if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" |
|
2483 and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" |
|
2484 and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" |
|
2485 and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}" |
|
2486 and k: "k \<in> Basis" |
|
2487 for c k g1 g2 |
|
2488 proof - |
|
2489 let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x" |
|
2490 show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b" |
2479 show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b" |
2491 proof (intro exI conjI ballI) |
2480 if "box a b = {}" for a b |
2492 show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x |
2481 apply (rule_tac x=f in exI) |
2493 by (auto simp: that assms fg1 fg2) |
2482 using assms that by (auto simp: content_eq_0_interior) |
2494 show "?g integrable_on cbox a b" |
2483 { |
2495 proof - |
2484 fix c g and k :: 'b |
2496 have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}" |
2485 assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b" |
2497 by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+ |
2486 assume k: "k \<in> Basis" |
2498 with has_integral_split[OF _ _ k] show ?thesis |
2487 show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" |
2499 unfolding integrable_on_def by blast |
2488 "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}" |
|
2489 apply (rule_tac[!] x=g in exI) |
|
2490 using fg integrable_split[OF g k] by auto |
|
2491 } |
|
2492 show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b" |
|
2493 if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" |
|
2494 and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" |
|
2495 and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" |
|
2496 and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}" |
|
2497 and k: "k \<in> Basis" |
|
2498 for c k g1 g2 |
|
2499 proof - |
|
2500 let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x" |
|
2501 show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b" |
|
2502 proof (intro exI conjI ballI) |
|
2503 show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x |
|
2504 by (auto simp: that assms fg1 fg2) |
|
2505 show "?g integrable_on cbox a b" |
|
2506 proof - |
|
2507 have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}" |
|
2508 by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+ |
|
2509 with has_integral_split[OF _ _ k] show ?thesis |
|
2510 unfolding integrable_on_def by blast |
|
2511 qed |
2500 qed |
2512 qed |
2501 qed |
2513 qed |
2502 qed |
2514 qed |
2503 qed |
2515 qed |
2504 |
2516 |
2998 qed |
3008 qed |
2999 |
3009 |
3000 |
3010 |
3001 subsection \<open>Integrability on subintervals.\<close> |
3011 subsection \<open>Integrability on subintervals.\<close> |
3002 |
3012 |
3003 lemma operative_integrable: |
3013 lemma operative_integrableI: |
3004 fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach" |
3014 fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach" |
3005 shows "comm_monoid.operative op \<and> True (\<lambda>i. f integrable_on i)" |
3015 assumes "0 \<le> e" |
3006 unfolding comm_monoid.operative_def[OF comm_monoid_and] |
3016 shows "operative conj True (\<lambda>i. f integrable_on i)" |
3007 apply safe |
3017 proof - |
3008 apply (subst integrable_on_def) |
3018 interpret comm_monoid conj True |
3009 apply rule |
3019 by standard auto |
3010 apply (rule has_integral_null_eq[where i=0, THEN iffD2]) |
3020 show ?thesis |
3011 apply (simp add: content_eq_0_interior) |
3021 apply standard |
3012 apply rule |
3022 apply safe |
3013 apply (rule, assumption, assumption)+ |
3023 apply (subst integrable_on_def) |
3014 unfolding integrable_on_def |
3024 apply rule |
3015 by (auto intro!: has_integral_split) |
3025 apply (rule has_integral_null_eq[where i=0, THEN iffD2]) |
|
3026 apply (simp add: content_eq_0_interior) |
|
3027 apply rule |
|
3028 apply (rule, assumption, assumption)+ |
|
3029 unfolding integrable_on_def |
|
3030 apply (auto intro!: has_integral_split) |
|
3031 done |
|
3032 qed |
3016 |
3033 |
3017 lemma integrable_subinterval: |
3034 lemma integrable_subinterval: |
3018 fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach" |
3035 fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach" |
3019 assumes "f integrable_on cbox a b" |
3036 assumes "f integrable_on cbox a b" |
3020 and "cbox c d \<subseteq> cbox a b" |
3037 and "cbox c d \<subseteq> cbox a b" |
3021 shows "f integrable_on cbox c d" |
3038 shows "f integrable_on cbox c d" |
3022 apply (cases "cbox c d = {}") |
3039 proof - |
3023 defer |
3040 interpret operative conj True "\<lambda>i. f integrable_on i" |
3024 apply (rule partial_division_extend_1[OF assms(2)],assumption) |
3041 using order_refl by (rule operative_integrableI) |
3025 using comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable,symmetric,of _ _ _ f] assms(1) |
3042 show ?thesis |
3026 apply (auto simp: comm_monoid_set_F_and) |
3043 apply (cases "cbox c d = {}") |
3027 done |
3044 defer |
|
3045 apply (rule partial_division_extend_1[OF assms(2)],assumption) |
|
3046 using division [symmetric] assms(1) |
|
3047 apply (auto simp: comm_monoid_set_F_and) |
|
3048 done |
|
3049 qed |
3028 |
3050 |
3029 lemma integrable_subinterval_real: |
3051 lemma integrable_subinterval_real: |
3030 fixes f :: "real \<Rightarrow> 'a::banach" |
3052 fixes f :: "real \<Rightarrow> 'a::banach" |
3031 assumes "f integrable_on {a..b}" |
3053 assumes "f integrable_on {a..b}" |
3032 and "{c..d} \<subseteq> {a..b}" |
3054 and "{c..d} \<subseteq> {a..b}" |
3042 and "c \<le> b" |
3064 and "c \<le> b" |
3043 and ac: "(f has_integral i) {a..c}" |
3065 and ac: "(f has_integral i) {a..c}" |
3044 and cb: "(f has_integral j) {c..b}" |
3066 and cb: "(f has_integral j) {c..b}" |
3045 shows "(f has_integral (i + j)) {a..b}" |
3067 shows "(f has_integral (i + j)) {a..b}" |
3046 proof - |
3068 proof - |
3047 interpret comm_monoid "lift_option plus" "Some (0::'a)" |
3069 interpret operative_real "lift_option plus" "Some 0" |
3048 by (rule comm_monoid_lift_option) |
3070 "\<lambda>i. if f integrable_on i then Some (integral i f) else None" |
3049 (rule add.comm_monoid_axioms) |
3071 using operative_integralI by (rule operative_realI) |
3050 from operative_integral [of f, unfolded operative_1_le] \<open>a \<le> c\<close> \<open>c \<le> b\<close> |
3072 from \<open>a \<le> c\<close> \<open>c \<le> b\<close> ac cb coalesce_less_eq |
3051 have *: "lift_option op + |
3073 have *: "lift_option op + |
3052 (if f integrable_on {a..c} then Some (integral {a..c} f) else None) |
3074 (if f integrable_on {a..c} then Some (integral {a..c} f) else None) |
3053 (if f integrable_on {c..b} then Some (integral {c..b} f) else None) = |
3075 (if f integrable_on {c..b} then Some (integral {c..b} f) else None) = |
3054 (if f integrable_on {a..b} then Some (integral {a..b} f) else None)" |
3076 (if f integrable_on {a..b} then Some (integral {a..b} f) else None)" |
3055 by (auto simp: split: if_split_asm) |
3077 by (auto simp: split: if_split_asm) |
3096 fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach" |
3118 fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach" |
3097 assumes "\<forall>x\<in>cbox a b. \<exists>d>0. \<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow> |
3119 assumes "\<forall>x\<in>cbox a b. \<exists>d>0. \<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow> |
3098 f integrable_on cbox u v" |
3120 f integrable_on cbox u v" |
3099 shows "f integrable_on cbox a b" |
3121 shows "f integrable_on cbox a b" |
3100 proof - |
3122 proof - |
|
3123 interpret operative conj True "\<lambda>i. f integrable_on i" |
|
3124 using order_refl by (rule operative_integrableI) |
3101 have "\<forall>x. \<exists>d>0. x\<in>cbox a b \<longrightarrow> (\<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow> |
3125 have "\<forall>x. \<exists>d>0. x\<in>cbox a b \<longrightarrow> (\<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow> |
3102 f integrable_on cbox u v)" |
3126 f integrable_on cbox u v)" |
3103 using assms by (metis zero_less_one) |
3127 using assms by (metis zero_less_one) |
3104 then obtain d where d: "\<And>x. 0 < d x" |
3128 then obtain d where d: "\<And>x. 0 < d x" |
3105 "\<And>x u v. \<lbrakk>x \<in> cbox a b; x \<in> cbox u v; cbox u v \<subseteq> ball x (d x); cbox u v \<subseteq> cbox a b\<rbrakk> |
3129 "\<And>x u v. \<lbrakk>x \<in> cbox a b; x \<in> cbox u v; cbox u v \<subseteq> ball x (d x); cbox u v \<subseteq> cbox a b\<rbrakk> |
7010 apply (rule integral_unique [OF has_integral_split [where c=c]]) |
7031 apply (rule integral_unique [OF has_integral_split [where c=c]]) |
7011 using k f |
7032 using k f |
7012 apply (auto simp: has_integral_integral [symmetric]) |
7033 apply (auto simp: has_integral_integral [symmetric]) |
7013 done |
7034 done |
7014 |
7035 |
7015 lemma integral_swap_operative: |
7036 lemma integral_swap_operativeI: |
7016 fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach" |
7037 fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach" |
7017 assumes f: "continuous_on s f" and e: "0 < e" |
7038 assumes f: "continuous_on s f" and e: "0 < e" |
7018 shows "comm_monoid.operative (op \<and>) True |
7039 shows "operative conj True |
7019 (\<lambda>k. \<forall>a b c d. |
7040 (\<lambda>k. \<forall>a b c d. |
7020 cbox (a,c) (b,d) \<subseteq> k \<and> cbox (a,c) (b,d) \<subseteq> s |
7041 cbox (a,c) (b,d) \<subseteq> k \<and> cbox (a,c) (b,d) \<subseteq> s |
7021 \<longrightarrow> norm(integral (cbox (a,c) (b,d)) f - |
7042 \<longrightarrow> norm(integral (cbox (a,c) (b,d)) f - |
7022 integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f((x,y))))) |
7043 integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f((x,y))))) |
7023 \<le> e * content (cbox (a,c) (b,d)))" |
7044 \<le> e * content (cbox (a,c) (b,d)))" |
7024 proof (auto simp: comm_monoid.operative_def[OF comm_monoid_and]) |
7045 proof (standard, auto) |
7025 fix a::'a and c::'b and b::'a and d::'b and u::'a and v::'a and w::'b and z::'b |
7046 fix a::'a and c::'b and b::'a and d::'b and u::'a and v::'a and w::'b and z::'b |
7026 assume *: "box (a, c) (b, d) = {}" |
7047 assume *: "box (a, c) (b, d) = {}" |
7027 and cb1: "cbox (u, w) (v, z) \<subseteq> cbox (a, c) (b, d)" |
7048 and cb1: "cbox (u, w) (v, z) \<subseteq> cbox (a, c) (b, d)" |
7028 and cb2: "cbox (u, w) (v, z) \<subseteq> s" |
7049 and cb2: "cbox (u, w) (v, z) \<subseteq> s" |
7029 then have c0: "content (cbox (a, c) (b, d)) = 0" |
7050 then have c0: "content (cbox (a, c) (b, d)) = 0" |
7113 integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. k))" |
7134 integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. k))" |
7114 by (simp add: content_Pair) |
7135 by (simp add: content_Pair) |
7115 |
7136 |
7116 lemma integral_prod_continuous: |
7137 lemma integral_prod_continuous: |
7117 fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach" |
7138 fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach" |
7118 assumes "continuous_on (cbox (a,c) (b,d)) f" (is "continuous_on ?CBOX f") |
7139 assumes "continuous_on (cbox (a, c) (b, d)) f" (is "continuous_on ?CBOX f") |
7119 shows "integral (cbox (a,c) (b,d)) f = integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f(x,y)))" |
7140 shows "integral (cbox (a, c) (b, d)) f = integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y)))" |
7120 proof (cases "content ?CBOX = 0") |
7141 proof (cases "content ?CBOX = 0") |
7121 case True |
7142 case True |
7122 then show ?thesis |
7143 then show ?thesis |
7123 by (auto simp: content_Pair) |
7144 by (auto simp: content_Pair) |
7124 next |
7145 next |
7125 case False |
7146 case False |
7126 then have cbp: "content ?CBOX > 0" |
7147 then have cbp: "content ?CBOX > 0" |
7127 using content_lt_nz by blast |
7148 using content_lt_nz by blast |
7128 have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) = 0" |
7149 have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) = 0" |
7129 proof (rule dense_eq0_I, simp) |
7150 proof (rule dense_eq0_I, simp) |
7130 fix e::real assume "0 < e" |
7151 fix e :: real |
7131 with cbp have e': "0 < e/content ?CBOX" |
7152 assume "0 < e" |
|
7153 with \<open>content ?CBOX > 0\<close> have "0 < e / content ?CBOX" |
7132 by simp |
7154 by simp |
7133 have f_int_acbd: "f integrable_on cbox (a,c) (b,d)" |
7155 have f_int_acbd: "f integrable_on ?CBOX" |
7134 by (rule integrable_continuous [OF assms]) |
7156 by (rule integrable_continuous [OF assms]) |
7135 { fix p |
7157 { fix p |
7136 assume p: "p division_of cbox (a,c) (b,d)" |
7158 assume p: "p division_of ?CBOX" |
7137 note opd1 = comm_monoid_set.operative_division [OF comm_monoid_set_and integral_swap_operative [OF assms e'], THEN iffD1, |
7159 then have "finite p" |
7138 THEN spec, THEN spec, THEN spec, THEN spec, of p "(a,c)" "(b,d)" a c b d] |
7160 by blast |
7139 have "(\<And>t u v w z. |
7161 define e' where "e' = e / content ?CBOX" |
7140 \<lbrakk>t \<in> p; cbox (u,w) (v,z) \<subseteq> t; cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)\<rbrakk> \<Longrightarrow> |
7162 with \<open>0 < e\<close> \<open>0 < e / content ?CBOX\<close> |
7141 norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)))) |
7163 have "0 < e'" |
7142 \<le> e * content (cbox (u,w) (v,z)) / content?CBOX) |
7164 by simp |
7143 \<Longrightarrow> |
7165 interpret operative conj True |
7144 norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e" |
7166 "\<lambda>k. \<forall>a' b' c' d'. |
7145 using opd1 [OF p] False by (simp add: comm_monoid_set_F_and) |
7167 cbox (a', c') (b', d') \<subseteq> k \<and> cbox (a', c') (b', d') \<subseteq> ?CBOX |
|
7168 \<longrightarrow> norm (integral (cbox (a', c') (b', d')) f - |
|
7169 integral (cbox a' b') (\<lambda>x. integral (cbox c' d') (\<lambda>y. f ((x, y))))) |
|
7170 \<le> e' * content (cbox (a', c') (b', d'))" |
|
7171 using assms \<open>0 < e'\<close> by (rule integral_swap_operativeI) |
|
7172 have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y)))) |
|
7173 \<le> e' * content ?CBOX" |
|
7174 if "\<And>t u v w z. t \<in> p \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> t \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> ?CBOX |
|
7175 \<Longrightarrow> norm (integral (cbox (u, w) (v, z)) f - |
|
7176 integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y)))) |
|
7177 \<le> e' * content (cbox (u, w) (v, z))" |
|
7178 using that division [of p "(a, c)" "(b, d)"] p \<open>finite p\<close> by (auto simp add: comm_monoid_set_F_and) |
|
7179 with False have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y)))) |
|
7180 \<le> e" |
|
7181 if "\<And>t u v w z. t \<in> p \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> t \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> ?CBOX |
|
7182 \<Longrightarrow> norm (integral (cbox (u, w) (v, z)) f - |
|
7183 integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y)))) |
|
7184 \<le> e * content (cbox (u, w) (v, z)) / content ?CBOX" |
|
7185 using that by (simp add: e'_def) |
7146 } note op_acbd = this |
7186 } note op_acbd = this |
7147 { fix k::real and p and u::'a and v w and z::'b and t1 t2 l |
7187 { fix k::real and p and u::'a and v w and z::'b and t1 t2 l |
7148 assume k: "0 < k" |
7188 assume k: "0 < k" |
7149 and nf: "\<And>x y u v. |
7189 and nf: "\<And>x y u v. |
7150 \<lbrakk>x \<in> cbox a b; y \<in> cbox c d; u \<in> cbox a b; v\<in>cbox c d; norm (u-x, v-y) < k\<rbrakk> |
7190 \<lbrakk>x \<in> cbox a b; y \<in> cbox c d; u \<in> cbox a b; v\<in>cbox c d; norm (u-x, v-y) < k\<rbrakk> |
7175 by (blast intro: continuous_on_imp_integrable_on_Pair1) |
7215 by (blast intro: continuous_on_imp_integrable_on_Pair1) |
7176 have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\<lambda>x. f (t1,t2))) |
7216 have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\<lambda>x. f (t1,t2))) |
7177 \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2" |
7217 \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2" |
7178 apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const) |
7218 apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const) |
7179 apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]]) |
7219 apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]]) |
7180 using cbp e' nf' |
7220 using cbp \<open>0 < e / content ?CBOX\<close> nf' |
7181 apply (auto simp: integrable_diff f_int_uwvz integrable_const) |
7221 apply (auto simp: integrable_diff f_int_uwvz integrable_const) |
7182 done |
7222 done |
7183 have int_integrable: "(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) integrable_on cbox u v" |
7223 have int_integrable: "(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) integrable_on cbox u v" |
7184 using assms integral_integrable_2dim continuous_on_subset uwvz_sub(2) by blast |
7224 using assms integral_integrable_2dim continuous_on_subset uwvz_sub(2) by blast |
7185 have normint_wz: |
7225 have normint_wz: |
7186 "\<And>x. x \<in> cbox u v \<Longrightarrow> |
7226 "\<And>x. x \<in> cbox u v \<Longrightarrow> |
7187 norm (integral (cbox w z) (\<lambda>y. f (x, y)) - integral (cbox w z) (\<lambda>y. f (t1, t2))) |
7227 norm (integral (cbox w z) (\<lambda>y. f (x, y)) - integral (cbox w z) (\<lambda>y. f (t1, t2))) |
7188 \<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2" |
7228 \<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2" |
7189 apply (simp only: integral_diff [symmetric] f_int_uv integrable_const) |
7229 apply (simp only: integral_diff [symmetric] f_int_uv integrable_const) |
7190 apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]]) |
7230 apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]]) |
7191 using cbp e' nf' |
7231 using cbp \<open>0 < e / content ?CBOX\<close> nf' |
7192 apply (auto simp: integrable_diff f_int_uv integrable_const) |
7232 apply (auto simp: integrable_diff f_int_uv integrable_const) |
7193 done |
7233 done |
7194 have "norm (integral (cbox u v) |
7234 have "norm (integral (cbox u v) |
7195 (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2)))) |
7235 (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2)))) |
7196 \<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)" |
7236 \<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)" |
7197 apply (rule integrable_bound [OF _ _ normint_wz]) |
7237 apply (rule integrable_bound [OF _ _ normint_wz]) |
7198 using cbp e' |
7238 using cbp \<open>0 < e / content ?CBOX\<close> |
7199 apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const) |
7239 apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const) |
7200 done |
7240 done |
7201 also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2" |
7241 also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2" |
7202 by (simp add: content_Pair divide_simps) |
7242 by (simp add: content_Pair divide_simps) |
7203 finally have 2: "norm (integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))) - |
7243 finally have 2: "norm (integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))) - |