equal
deleted
inserted
replaced
791 have "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) |
791 have "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) |
792 \<le> 2 * content (cbox a b)" |
792 \<le> 2 * content (cbox a b)" |
793 proof (rule sum_content_area_over_thin_division) |
793 proof (rule sum_content_area_over_thin_division) |
794 show "snd ` S division_of \<Union>(snd ` S)" |
794 show "snd ` S division_of \<Union>(snd ` S)" |
795 by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division) |
795 by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division) |
796 show "UNION S snd \<subseteq> cbox a b" |
796 show "\<Union>(snd ` S) \<subseteq> cbox a b" |
797 using S by force |
797 using S by force |
798 show "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> b \<bullet> i" |
798 show "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> b \<bullet> i" |
799 using mem_box(2) that by blast+ |
799 using mem_box(2) that by blast+ |
800 qed (use that in auto) |
800 qed (use that in auto) |
801 then show "(b \<bullet> i - a \<bullet> i) / (2 * content (cbox a b)) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<le> 1" |
801 then show "(b \<bullet> i - a \<bullet> i) / (2 * content (cbox a b)) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) \<le> 1" |
985 and eq: "K \<inter> {x. x \<bullet> i \<le> c} = L \<inter> {x. x \<bullet> i \<le> c}" |
985 and eq: "K \<inter> {x. x \<bullet> i \<le> c} = L \<inter> {x. x \<bullet> i \<le> c}" |
986 have False if "K \<noteq> L" |
986 have False if "K \<noteq> L" |
987 proof - |
987 proof - |
988 obtain u v where uv: "L = cbox u v" |
988 obtain u v where uv: "L = cbox u v" |
989 using T'_tagged \<open>(x, L) \<in> A\<close> \<open>A \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast |
989 using T'_tagged \<open>(x, L) \<in> A\<close> \<open>A \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast |
990 have "A tagged_division_of UNION A snd" |
990 have "A tagged_division_of \<Union>(snd ` A)" |
991 using A_tagged tagged_partial_division_of_Union_self by auto |
991 using A_tagged tagged_partial_division_of_Union_self by auto |
992 then have "interior (K \<inter> {x. x \<bullet> i \<le> c}) = {}" |
992 then have "interior (K \<inter> {x. x \<bullet> i \<le> c}) = {}" |
993 apply (rule tagged_division_split_left_inj [OF _ \<open>(x,K) \<in> A\<close> \<open>(x,L) \<in> A\<close>]) |
993 apply (rule tagged_division_split_left_inj [OF _ \<open>(x,K) \<in> A\<close> \<open>(x,L) \<in> A\<close>]) |
994 using that eq \<open>i \<in> Basis\<close> by auto |
994 using that eq \<open>i \<in> Basis\<close> by auto |
995 then show False |
995 then show False |
1014 and eq: "K \<inter> {x. c \<le> x \<bullet> i} = L \<inter> {x. c \<le> x \<bullet> i}" |
1014 and eq: "K \<inter> {x. c \<le> x \<bullet> i} = L \<inter> {x. c \<le> x \<bullet> i}" |
1015 have False if "K \<noteq> L" |
1015 have False if "K \<noteq> L" |
1016 proof - |
1016 proof - |
1017 obtain u v where uv: "L = cbox u v" |
1017 obtain u v where uv: "L = cbox u v" |
1018 using T'_tagged \<open>(x, L) \<in> B\<close> \<open>B \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast |
1018 using T'_tagged \<open>(x, L) \<in> B\<close> \<open>B \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast |
1019 have "B tagged_division_of UNION B snd" |
1019 have "B tagged_division_of \<Union>(snd ` B)" |
1020 using B_tagged tagged_partial_division_of_Union_self by auto |
1020 using B_tagged tagged_partial_division_of_Union_self by auto |
1021 then have "interior (K \<inter> {x. c \<le> x \<bullet> i}) = {}" |
1021 then have "interior (K \<inter> {x. c \<le> x \<bullet> i}) = {}" |
1022 apply (rule tagged_division_split_right_inj [OF _ \<open>(x,K) \<in> B\<close> \<open>(x,L) \<in> B\<close>]) |
1022 apply (rule tagged_division_split_right_inj [OF _ \<open>(x,K) \<in> B\<close> \<open>(x,L) \<in> B\<close>]) |
1023 using that eq \<open>i \<in> Basis\<close> by auto |
1023 using that eq \<open>i \<in> Basis\<close> by auto |
1024 then show False |
1024 then show False |