equal
deleted
inserted
replaced
377 |
377 |
378 obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2" |
378 obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2" |
379 and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" |
379 and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" |
380 using IntegralE [OF \<open>Integral (b, c) f x2\<close> \<open>0 < \<epsilon>/2\<close>] by auto |
380 using IntegralE [OF \<open>Integral (b, c) f x2\<close> \<open>0 < \<epsilon>/2\<close>] by auto |
381 |
381 |
382 def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x) |
382 define \<delta> where "\<delta> x = |
383 else if x = b then min (\<delta>1 b) (\<delta>2 b) |
383 (if x < b then min (\<delta>1 x) (b - x) |
384 else min (\<delta>2 x) (x - b)" |
384 else if x = b then min (\<delta>1 b) (\<delta>2 b) |
|
385 else min (\<delta>2 x) (x - b))" for x |
385 |
386 |
386 have "gauge {a..c} \<delta>" |
387 have "gauge {a..c} \<delta>" |
387 using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto |
388 using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto |
388 |
389 |
389 moreover { |
390 moreover { |
408 show False by (cases "t < b") auto |
409 show False by (cases "t < b") auto |
409 qed |
410 qed |
410 |
411 |
411 let ?D1 = "take N D" |
412 let ?D1 = "take N D" |
412 let ?D2 = "drop N D" |
413 let ?D2 = "drop N D" |
413 def D1 \<equiv> "take N D @ [(d, t, b)]" |
414 define D1 where "D1 = take N D @ [(d, t, b)]" |
414 def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D" |
415 define D2 where "D2 = (if b = e then [] else [(b, t, e)]) @ drop (Suc N) D" |
415 |
416 |
416 from hd_drop_conv_nth[OF \<open>N < length D\<close>] |
417 from hd_drop_conv_nth[OF \<open>N < length D\<close>] |
417 have "fst (hd ?D2) = d" using \<open>D ! N = (d, t, e)\<close> by auto |
418 have "fst (hd ?D2) = d" using \<open>D ! N = (d, t, e)\<close> by auto |
418 with fine_append_split[OF _ _ append_take_drop_id[symmetric]] |
419 with fine_append_split[OF _ _ append_take_drop_id[symmetric]] |
419 have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2" |
420 have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2" |