638 fixes s :: "'a::euclidean_space set" |
638 fixes s :: "'a::euclidean_space set" |
639 assumes "bounded s" |
639 assumes "bounded s" |
640 shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)" (is "_ = ?rhs") |
640 shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)" (is "_ = ?rhs") |
641 proof safe |
641 proof safe |
642 assume "content s = 0" then show ?rhs |
642 assume "content s = 0" then show ?rhs |
643 apply (clarsimp simp: ex_in_conv content_def split: split_if_asm) |
643 apply (clarsimp simp: ex_in_conv content_def split: if_split_asm) |
644 apply (rule_tac x=a in bexI) |
644 apply (rule_tac x=a in bexI) |
645 apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI) |
645 apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI) |
646 apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def) |
646 apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def) |
647 apply (drule cSUP_eq_cINF_D) |
647 apply (drule cSUP_eq_cINF_D) |
648 apply (auto simp: bounded_inner_imp_bdd_above [OF assms] bounded_inner_imp_bdd_below [OF assms]) |
648 apply (auto simp: bounded_inner_imp_bdd_above [OF assms] bounded_inner_imp_bdd_below [OF assms]) |
3211 setsum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} = |
3211 setsum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} = |
3212 setsum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)" |
3212 setsum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)" |
3213 by (rule setsum.mono_neutral_left) auto |
3213 by (rule setsum.mono_neutral_left) auto |
3214 let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}" |
3214 let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}" |
3215 have d1_fine: "d1 fine ?M1" |
3215 have d1_fine: "d1 fine ?M1" |
3216 by (force intro: fineI dest: fineD[OF p(2)] simp add: split: split_if_asm) |
3216 by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm) |
3217 have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2" |
3217 have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2" |
3218 proof (rule d1norm [OF tagged_division_ofI d1_fine]) |
3218 proof (rule d1norm [OF tagged_division_ofI d1_fine]) |
3219 show "finite ?M1" |
3219 show "finite ?M1" |
3220 by (rule fin_finite p(3))+ |
3220 by (rule fin_finite p(3))+ |
3221 show "\<Union>{k. \<exists>x. (x, k) \<in> ?M1} = cbox a b \<inter> {x. x\<bullet>k \<le> c}" |
3221 show "\<Union>{k. \<exists>x. (x, k) \<in> ?M1} = cbox a b \<inter> {x. x\<bullet>k \<le> c}" |
3250 qed |
3250 qed |
3251 qed |
3251 qed |
3252 moreover |
3252 moreover |
3253 let ?M2 = "{(x,kk \<inter> {x. x\<bullet>k \<ge> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}" |
3253 let ?M2 = "{(x,kk \<inter> {x. x\<bullet>k \<ge> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}" |
3254 have d2_fine: "d2 fine ?M2" |
3254 have d2_fine: "d2 fine ?M2" |
3255 by (force intro: fineI dest: fineD[OF p(2)] simp add: split: split_if_asm) |
3255 by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm) |
3256 have "norm ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) < e/2" |
3256 have "norm ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) < e/2" |
3257 proof (rule d2norm [OF tagged_division_ofI d2_fine]) |
3257 proof (rule d2norm [OF tagged_division_ofI d2_fine]) |
3258 show "finite ?M2" |
3258 show "finite ?M2" |
3259 by (rule fin_finite p(3))+ |
3259 by (rule fin_finite p(3))+ |
3260 show "\<Union>{k. \<exists>x. (x, k) \<in> ?M2} = cbox a b \<inter> {x. x\<bullet>k \<ge> c}" |
3260 show "\<Union>{k. \<exists>x. (x, k) \<in> ?M2} = cbox a b \<inter> {x. x\<bullet>k \<ge> c}" |
3747 using l using as(6) unfolding box_ne_empty[symmetric] by auto |
3747 using l using as(6) unfolding box_ne_empty[symmetric] by auto |
3748 show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x" |
3748 show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x" |
3749 apply (rule bexI[OF _ \<open>l \<in> d\<close>]) |
3749 apply (rule bexI[OF _ \<open>l \<in> d\<close>]) |
3750 using as(1-3,5) fstx |
3750 using as(1-3,5) fstx |
3751 unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as |
3751 unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as |
3752 apply (auto split: split_if_asm) |
3752 apply (auto split: if_split_asm) |
3753 done |
3753 done |
3754 show "snd x < b \<bullet> fst x" |
3754 show "snd x < b \<bullet> fst x" |
3755 using as(2) \<open>c < b\<bullet>k\<close> by (auto split: split_if_asm) |
3755 using as(2) \<open>c < b\<bullet>k\<close> by (auto split: if_split_asm) |
3756 qed |
3756 qed |
3757 show ?t2 |
3757 show ?t2 |
3758 unfolding division_points_def interval_split[OF k, of a b] |
3758 unfolding division_points_def interval_split[OF k, of a b] |
3759 unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)] |
3759 unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)] |
3760 unfolding * |
3760 unfolding * |
3778 using l using as(6) unfolding box_ne_empty[symmetric] by auto |
3778 using l using as(6) unfolding box_ne_empty[symmetric] by auto |
3779 show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x" |
3779 show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x" |
3780 apply (rule bexI[OF _ \<open>l \<in> d\<close>]) |
3780 apply (rule bexI[OF _ \<open>l \<in> d\<close>]) |
3781 using as(1-3,5) fstx |
3781 using as(1-3,5) fstx |
3782 unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as |
3782 unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as |
3783 apply (auto split: split_if_asm) |
3783 apply (auto split: if_split_asm) |
3784 done |
3784 done |
3785 show "a \<bullet> fst x < snd x" |
3785 show "a \<bullet> fst x < snd x" |
3786 using as(1) \<open>a\<bullet>k < c\<close> by (auto split: split_if_asm) |
3786 using as(1) \<open>a\<bullet>k < c\<close> by (auto split: if_split_asm) |
3787 qed |
3787 qed |
3788 qed |
3788 qed |
3789 |
3789 |
3790 lemma division_points_psubset: |
3790 lemma division_points_psubset: |
3791 fixes a :: "'a::euclidean_space" |
3791 fixes a :: "'a::euclidean_space" |
4366 using k norm_bound_Basis_lt d1 d2 p |
4366 using k norm_bound_Basis_lt d1 d2 p |
4367 by blast+ |
4367 by blast+ |
4368 then show False |
4368 then show False |
4369 unfolding inner_simps |
4369 unfolding inner_simps |
4370 using rsum_component_le[OF p(1) le] |
4370 using rsum_component_le[OF p(1) le] |
4371 by (simp add: abs_real_def split: split_if_asm) |
4371 by (simp add: abs_real_def split: if_split_asm) |
4372 qed |
4372 qed |
4373 show ?thesis |
4373 show ?thesis |
4374 proof (cases "\<exists>a b. s = cbox a b") |
4374 proof (cases "\<exists>a b. s = cbox a b") |
4375 case True |
4375 case True |
4376 with lem assms show ?thesis |
4376 with lem assms show ?thesis |
4389 from bounded_subset_cbox[OF this] guess a b by (elim exE) |
4389 from bounded_subset_cbox[OF this] guess a b by (elim exE) |
4390 note ab = conjunctD2[OF this[unfolded Un_subset_iff]] |
4390 note ab = conjunctD2[OF this[unfolded Un_subset_iff]] |
4391 guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this] |
4391 guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this] |
4392 guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this] |
4392 guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this] |
4393 have *: "\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False" |
4393 have *: "\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False" |
4394 by (simp add: abs_real_def split: split_if_asm) |
4394 by (simp add: abs_real_def split: if_split_asm) |
4395 note le_less_trans[OF Basis_le_norm[OF k]] |
4395 note le_less_trans[OF Basis_le_norm[OF k]] |
4396 note this[OF w1(2)] this[OF w2(2)] |
4396 note this[OF w1(2)] this[OF w2(2)] |
4397 moreover |
4397 moreover |
4398 have "w1\<bullet>k \<le> w2\<bullet>k" |
4398 have "w1\<bullet>k \<le> w2\<bullet>k" |
4399 by (rule lem[OF w1(1) w2(1)]) (simp add: assms(4)) |
4399 by (rule lem[OF w1(1) w2(1)]) (simp add: assms(4)) |
6084 by (rule bounded_bilinear_scaleR) |
6084 by (rule bounded_bilinear_scaleR) |
6085 def g \<equiv> "\<lambda>s. (b - s)^(p - 1)/fact (p - 1)" |
6085 def g \<equiv> "\<lambda>s. (b - s)^(p - 1)/fact (p - 1)" |
6086 def Dg \<equiv> "\<lambda>n s. if n < p then (-1)^n * (b - s)^(p - 1 - n) / fact (p - 1 - n) else 0" |
6086 def Dg \<equiv> "\<lambda>n s. if n < p then (-1)^n * (b - s)^(p - 1 - n) / fact (p - 1 - n) else 0" |
6087 have g0: "Dg 0 = g" |
6087 have g0: "Dg 0 = g" |
6088 using \<open>p > 0\<close> |
6088 using \<open>p > 0\<close> |
6089 by (auto simp add: Dg_def divide_simps g_def split: split_if_asm) |
6089 by (auto simp add: Dg_def divide_simps g_def split: if_split_asm) |
6090 { |
6090 { |
6091 fix m |
6091 fix m |
6092 assume "p > Suc m" |
6092 assume "p > Suc m" |
6093 hence "p - Suc m = Suc (p - Suc (Suc m))" |
6093 hence "p - Suc m = Suc (p - Suc (Suc m))" |
6094 by auto |
6094 by auto |
8474 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
8474 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
8475 assumes "negligible ((s - t) \<union> (t - s))" |
8475 assumes "negligible ((s - t) \<union> (t - s))" |
8476 shows "(f has_integral y) s \<longleftrightarrow> (f has_integral y) t" |
8476 shows "(f has_integral y) s \<longleftrightarrow> (f has_integral y) t" |
8477 unfolding has_integral_restrict_univ[symmetric,of f] |
8477 unfolding has_integral_restrict_univ[symmetric,of f] |
8478 apply (rule has_integral_spike_eq[OF assms]) |
8478 apply (rule has_integral_spike_eq[OF assms]) |
8479 by (auto split: split_if_asm) |
8479 by (auto split: if_split_asm) |
8480 |
8480 |
8481 lemma has_integral_spike_set[dest]: |
8481 lemma has_integral_spike_set[dest]: |
8482 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
8482 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
8483 assumes "negligible ((s - t) \<union> (t - s))" |
8483 assumes "negligible ((s - t) \<union> (t - s))" |
8484 and "(f has_integral y) s" |
8484 and "(f has_integral y) s" |
8996 by auto |
8996 by auto |
8997 have *: "\<And>ga gc ha hc fa fc::real. |
8997 have *: "\<And>ga gc ha hc fa fc::real. |
8998 \<bar>ga - i\<bar> < e / 3 \<and> \<bar>gc - i\<bar> < e / 3 \<and> \<bar>ha - j\<bar> < e / 3 \<and> |
8998 \<bar>ga - i\<bar> < e / 3 \<and> \<bar>gc - i\<bar> < e / 3 \<and> \<bar>ha - j\<bar> < e / 3 \<and> |
8999 \<bar>hc - j\<bar> < e / 3 \<and> \<bar>i - j\<bar> < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc \<Longrightarrow> |
8999 \<bar>hc - j\<bar> < e / 3 \<and> \<bar>i - j\<bar> < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc \<Longrightarrow> |
9000 \<bar>fa - fc\<bar> < e" |
9000 \<bar>fa - fc\<bar> < e" |
9001 by (simp add: abs_real_def split: split_if_asm) |
9001 by (simp add: abs_real_def split: if_split_asm) |
9002 show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - integral (cbox c d) |
9002 show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - integral (cbox c d) |
9003 (\<lambda>x. if x \<in> s then f x else 0)) < e" |
9003 (\<lambda>x. if x \<in> s then f x else 0)) < e" |
9004 unfolding real_norm_def |
9004 unfolding real_norm_def |
9005 apply (rule *) |
9005 apply (rule *) |
9006 apply safe |
9006 apply safe |