6352 and "d division_of {a..b}" |
6353 and "d division_of {a..b}" |
6353 shows "(\<forall>i\<in>d. P i) \<longleftrightarrow> P {a..b}" |
6354 shows "(\<forall>i\<in>d. P i) \<longleftrightarrow> P {a..b}" |
6354 using operative_division[OF monoidal_and assms] division_of_finite[OF assms(2)] |
6355 using operative_division[OF monoidal_and assms] division_of_finite[OF assms(2)] |
6355 by auto |
6356 by auto |
6356 |
6357 |
6357 lemma operative_approximable: assumes "0 \<le> e" fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
6358 lemma operative_approximable: |
6358 shows "operative op \<and> (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)" unfolding operative_def neutral_and |
6359 fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
|
6360 assumes "0 \<le> e" |
|
6361 shows "operative op \<and> (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)" |
|
6362 unfolding operative_def neutral_and |
6359 proof safe |
6363 proof safe |
6360 fix a b::"'b" |
6364 fix a b :: 'b |
6361 { assume "content {a..b} = 0" |
6365 { |
6362 thus "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" |
6366 assume "content {a..b} = 0" |
6363 apply(rule_tac x=f in exI) using assms by(auto intro!:integrable_on_null) } |
6367 then show "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" |
6364 { fix c g and k :: 'b |
6368 apply (rule_tac x=f in exI) |
6365 assume as:"\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e" "g integrable_on {a..b}" and k:"k\<in>Basis" |
6369 using assms |
|
6370 apply (auto intro!:integrable_on_null) |
|
6371 done |
|
6372 } |
|
6373 { |
|
6374 fix c g |
|
6375 fix k :: 'b |
|
6376 assume as: "\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e" "g integrable_on {a..b}" |
|
6377 assume k: "k \<in> Basis" |
6366 show "\<exists>g. (\<forall>x\<in>{a..b} \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" |
6378 show "\<exists>g. (\<forall>x\<in>{a..b} \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" |
6367 "\<exists>g. (\<forall>x\<in>{a..b} \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b} \<inter> {x. c \<le> x \<bullet> k}" |
6379 "\<exists>g. (\<forall>x\<in>{a..b} \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b} \<inter> {x. c \<le> x \<bullet> k}" |
6368 apply(rule_tac[!] x=g in exI) using as(1) integrable_split[OF as(2) k] by auto } |
6380 apply (rule_tac[!] x=g in exI) |
6369 fix c k g1 g2 assume as:"\<forall>x\<in>{a..b} \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" "g1 integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" |
6381 using as(1) integrable_split[OF as(2) k] |
6370 "\<forall>x\<in>{a..b} \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" "g2 integrable_on {a..b} \<inter> {x. c \<le> x \<bullet> k}" |
6382 apply auto |
6371 assume k:"k\<in>Basis" |
6383 done |
|
6384 } |
|
6385 fix c k g1 g2 |
|
6386 assume as: "\<forall>x\<in>{a..b} \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" "g1 integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" |
|
6387 "\<forall>x\<in>{a..b} \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" "g2 integrable_on {a..b} \<inter> {x. c \<le> x \<bullet> k}" |
|
6388 assume k: "k \<in> Basis" |
6372 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" |
6389 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" |
6373 show "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" apply(rule_tac x="?g" in exI) |
6390 show "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" |
6374 proof safe case goal1 thus ?case apply- apply(cases "x\<bullet>k=c", case_tac "x\<bullet>k < c") using as assms by auto |
6391 apply (rule_tac x="?g" in exI) |
6375 next case goal2 presume "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<ge> c}" |
6392 proof safe |
6376 then guess h1 h2 unfolding integrable_on_def by auto from has_integral_split[OF this k] |
6393 case goal1 |
6377 show ?case unfolding integrable_on_def by auto |
6394 then show ?case |
6378 next show "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<ge> c}" |
6395 apply - |
6379 apply(rule_tac[!] integrable_spike[OF negligible_standard_hyperplane[of k c]]) using k as(2,4) by auto qed qed |
6396 apply (cases "x\<bullet>k=c") |
6380 |
6397 apply (case_tac "x\<bullet>k < c") |
6381 lemma approximable_on_division: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
6398 using as assms |
6382 assumes "0 \<le> e" "d division_of {a..b}" "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i" |
6399 apply auto |
|
6400 done |
|
6401 next |
|
6402 case goal2 |
|
6403 presume "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" |
|
6404 and "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<ge> c}" |
|
6405 then guess h1 h2 unfolding integrable_on_def by auto |
|
6406 from has_integral_split[OF this k] show ?case |
|
6407 unfolding integrable_on_def by auto |
|
6408 next |
|
6409 show "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<ge> c}" |
|
6410 apply(rule_tac[!] integrable_spike[OF negligible_standard_hyperplane[of k c]]) |
|
6411 using k as(2,4) |
|
6412 apply auto |
|
6413 done |
|
6414 qed |
|
6415 qed |
|
6416 |
|
6417 lemma approximable_on_division: |
|
6418 fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
|
6419 assumes "0 \<le> e" |
|
6420 and "d division_of {a..b}" |
|
6421 and "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i" |
6383 obtains g where "\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e" "g integrable_on {a..b}" |
6422 obtains g where "\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e" "g integrable_on {a..b}" |
6384 proof- note * = operative_division[OF monoidal_and operative_approximable[OF assms(1)] assms(2)] |
6423 proof - |
6385 note this[unfolded iterate_and[OF division_of_finite[OF assms(2)]]] from assms(3)[unfolded this[of f]] |
6424 note * = operative_division[OF monoidal_and operative_approximable[OF assms(1)] assms(2)] |
6386 guess g .. thus thesis apply-apply(rule that[of g]) by auto qed |
6425 note this[unfolded iterate_and[OF division_of_finite[OF assms(2)]]] |
6387 |
6426 from assms(3)[unfolded this[of f]] guess g .. |
6388 lemma integrable_continuous: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
6427 then show thesis |
6389 assumes "continuous_on {a..b} f" shows "f integrable_on {a..b}" |
6428 apply - |
6390 proof(rule integrable_uniform_limit,safe) fix e::real assume e:"0 < e" |
6429 apply (rule that[of g]) |
|
6430 apply auto |
|
6431 done |
|
6432 qed |
|
6433 |
|
6434 lemma integrable_continuous: |
|
6435 fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
|
6436 assumes "continuous_on {a..b} f" |
|
6437 shows "f integrable_on {a..b}" |
|
6438 proof (rule integrable_uniform_limit, safe) |
|
6439 fix e :: real |
|
6440 assume e: "e > 0" |
6391 from compact_uniformly_continuous[OF assms compact_interval,unfolded uniformly_continuous_on_def,rule_format,OF e] guess d .. |
6441 from compact_uniformly_continuous[OF assms compact_interval,unfolded uniformly_continuous_on_def,rule_format,OF e] guess d .. |
6392 note d=conjunctD2[OF this,rule_format] |
6442 note d=conjunctD2[OF this,rule_format] |
6393 from fine_division_exists[OF gauge_ball[OF d(1)], of a b] guess p . note p=this |
6443 from fine_division_exists[OF gauge_ball[OF d(1)], of a b] guess p . note p=this |
6394 note p' = tagged_division_ofD[OF p(1)] |
6444 note p' = tagged_division_ofD[OF p(1)] |
6395 have *:"\<forall>i\<in>snd ` p. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i" |
6445 have *: "\<forall>i\<in>snd ` p. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i" |
6396 proof(safe,unfold snd_conv) fix x l assume as:"(x,l) \<in> p" |
6446 proof (safe, unfold snd_conv) |
6397 from p'(4)[OF this] guess a b apply-by(erule exE)+ note l=this |
6447 fix x l |
6398 show "\<exists>g. (\<forall>x\<in>l. norm (f x - g x) \<le> e) \<and> g integrable_on l" apply(rule_tac x="\<lambda>y. f x" in exI) |
6448 assume as: "(x, l) \<in> p" |
6399 proof safe show "(\<lambda>y. f x) integrable_on l" unfolding integrable_on_def l by(rule,rule has_integral_const) |
6449 from p'(4)[OF this] guess a b by (elim exE) note l=this |
6400 fix y assume y:"y\<in>l" note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this] |
6450 show "\<exists>g. (\<forall>x\<in>l. norm (f x - g x) \<le> e) \<and> g integrable_on l" |
|
6451 apply (rule_tac x="\<lambda>y. f x" in exI) |
|
6452 proof safe |
|
6453 show "(\<lambda>y. f x) integrable_on l" |
|
6454 unfolding integrable_on_def l |
|
6455 apply rule |
|
6456 apply (rule has_integral_const) |
|
6457 done |
|
6458 fix y |
|
6459 assume y: "y \<in> l" |
|
6460 note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this] |
6401 note d(2)[OF _ _ this[unfolded mem_ball]] |
6461 note d(2)[OF _ _ this[unfolded mem_ball]] |
6402 thus "norm (f y - f x) \<le> e" using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce qed qed |
6462 then show "norm (f y - f x) \<le> e" |
6403 from e have "0 \<le> e" by auto from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g . |
6463 using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce |
6404 thus "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" by auto qed |
6464 qed |
|
6465 qed |
|
6466 from e have "e \<ge> 0" |
|
6467 by auto |
|
6468 from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g . |
|
6469 then show "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" |
|
6470 by auto |
|
6471 qed |
|
6472 |
6405 |
6473 |
6406 subsection {* Specialization of additivity to one dimension. *} |
6474 subsection {* Specialization of additivity to one dimension. *} |
6407 |
6475 |
6408 lemma |
6476 lemma |
6409 shows real_inner_1_left: "inner 1 x = x" |
6477 shows real_inner_1_left: "inner 1 x = x" |
6410 and real_inner_1_right: "inner x 1 = x" |
6478 and real_inner_1_right: "inner x 1 = x" |
6411 by simp_all |
6479 by simp_all |
6412 |
6480 |
6413 lemma operative_1_lt: assumes "monoidal opp" |
6481 lemma operative_1_lt: |
|
6482 assumes "monoidal opp" |
6414 shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a..b::real} = neutral opp) \<and> |
6483 shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a..b::real} = neutral opp) \<and> |
6415 (\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f{a..c})(f{c..b}) = f {a..b}))" |
6484 (\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}))" |
6416 apply (simp add: operative_def content_eq_0 less_one) |
6485 apply (simp add: operative_def content_eq_0) |
6417 proof safe fix a b c::"real" assume as:"\<forall>a b c. f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c})) |
6486 proof safe |
6418 (f ({a..b} \<inter> {x. c \<le> x}))" "a < c" "c < b" |
6487 fix a b c :: real |
6419 from this(2-) have "{a..b} \<inter> {x. x \<le> c} = {a..c}" "{a..b} \<inter> {x. x \<ge> c} = {c..b}" by auto |
6488 assume as: |
6420 thus "opp (f {a..c}) (f {c..b}) = f {a..b}" unfolding as(1)[rule_format,of a b "c"] by auto |
6489 "\<forall>a b c. f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c})) (f ({a..b} \<inter> {x. c \<le> x}))" |
6421 next fix a b c::real |
6490 "a < c" |
6422 assume as:"\<forall>a b. b \<le> a \<longrightarrow> f {a..b} = neutral opp" "\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}" |
6491 "c < b" |
|
6492 from this(2-) have "{a..b} \<inter> {x. x \<le> c} = {a..c}" "{a..b} \<inter> {x. x \<ge> c} = {c..b}" |
|
6493 by auto |
|
6494 then show "opp (f {a..c}) (f {c..b}) = f {a..b}" |
|
6495 unfolding as(1)[rule_format,of a b "c"] by auto |
|
6496 next |
|
6497 fix a b c :: real |
|
6498 assume as: "\<forall>a b. b \<le> a \<longrightarrow> f {a..b} = neutral opp" |
|
6499 "\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}" |
6423 show "f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c})) (f ({a..b} \<inter> {x. c \<le> x}))" |
6500 show "f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c})) (f ({a..b} \<inter> {x. c \<le> x}))" |
6424 proof(cases "c \<in> {a .. b}") |
6501 proof (cases "c \<in> {a..b}") |
6425 case False hence "c<a \<or> c>b" by auto |
6502 case False |
6426 thus ?thesis apply-apply(erule disjE) |
6503 then have "c < a \<or> c > b" by auto |
6427 proof- assume "c<a" hence *:"{a..b} \<inter> {x. x \<le> c} = {1..0}" "{a..b} \<inter> {x. c \<le> x} = {a..b}" by auto |
6504 then show ?thesis |
6428 show ?thesis unfolding * apply(subst as(1)[rule_format,of 0 1]) using assms by auto |
6505 proof |
6429 next assume "b<c" hence *:"{a..b} \<inter> {x. x \<le> c} = {a..b}" "{a..b} \<inter> {x. c \<le> x} = {1..0}" by auto |
6506 assume "c < a" |
6430 show ?thesis unfolding * apply(subst as(1)[rule_format,of 0 1]) using assms by auto |
6507 then have *: "{a..b} \<inter> {x. x \<le> c} = {1..0}" "{a..b} \<inter> {x. c \<le> x} = {a..b}" |
|
6508 by auto |
|
6509 show ?thesis |
|
6510 unfolding * |
|
6511 apply (subst as(1)[rule_format,of 0 1]) |
|
6512 using assms |
|
6513 apply auto |
|
6514 done |
|
6515 next |
|
6516 assume "b < c" |
|
6517 then have *: "{a..b} \<inter> {x. x \<le> c} = {a..b}" "{a..b} \<inter> {x. c \<le> x} = {1..0}" |
|
6518 by auto |
|
6519 show ?thesis |
|
6520 unfolding * |
|
6521 apply (subst as(1)[rule_format,of 0 1]) |
|
6522 using assms |
|
6523 apply auto |
|
6524 done |
6431 qed |
6525 qed |
6432 next case True hence *:"min (b) c = c" "max a c = c" by auto |
6526 next |
6433 have **: "(1::real) \<in> Basis" by simp |
6527 case True |
6434 have ***:"\<And>P Q. (\<Sum>i\<in>Basis. (if i = 1 then P i else Q i) *\<^sub>R i) = (P 1::real)" |
6528 then have *: "min (b) c = c" "max a c = c" |
|
6529 by auto |
|
6530 have **: "(1::real) \<in> Basis" |
|
6531 by simp |
|
6532 have ***: "\<And>P Q. (\<Sum>i\<in>Basis. (if i = 1 then P i else Q i) *\<^sub>R i) = (P 1::real)" |
6435 by simp |
6533 by simp |
6436 show ?thesis |
6534 show ?thesis |
6437 unfolding interval_split[OF **, unfolded real_inner_1_right] unfolding *** * |
6535 unfolding interval_split[OF **, unfolded real_inner_1_right] unfolding *** * |
6438 proof(cases "c = a \<or> c = b") |
6536 proof (cases "c = a \<or> c = b") |
6439 case False thus "f {a..b} = opp (f {a..c}) (f {c..b})" |
6537 case False |
6440 apply-apply(subst as(2)[rule_format]) using True by auto |
6538 then show "f {a..b} = opp (f {a..c}) (f {c..b})" |
6441 next case True thus "f {a..b} = opp (f {a..c}) (f {c..b})" apply- |
6539 apply - |
6442 proof(erule disjE) assume *:"c=a" |
6540 apply (subst as(2)[rule_format]) |
6443 hence "f {a..c} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto |
6541 using True |
6444 thus ?thesis using assms unfolding * by auto |
6542 apply auto |
6445 next assume *:"c=b" hence "f {c..b} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto |
6543 done |
6446 thus ?thesis using assms unfolding * by auto qed qed qed qed |
6544 next |
6447 |
6545 case True |
6448 lemma operative_1_le: assumes "monoidal opp" |
6546 then show "f {a..b} = opp (f {a..c}) (f {c..b})" |
|
6547 proof |
|
6548 assume *: "c = a" |
|
6549 then have "f {a..c} = neutral opp" |
|
6550 apply - |
|
6551 apply (rule as(1)[rule_format]) |
|
6552 apply auto |
|
6553 done |
|
6554 then show ?thesis |
|
6555 using assms unfolding * by auto |
|
6556 next |
|
6557 assume *: "c = b" |
|
6558 then have "f {c..b} = neutral opp" |
|
6559 apply - |
|
6560 apply (rule as(1)[rule_format]) |
|
6561 apply auto |
|
6562 done |
|
6563 then show ?thesis |
|
6564 using assms unfolding * by auto |
|
6565 qed |
|
6566 qed |
|
6567 qed |
|
6568 qed |
|
6569 |
|
6570 lemma operative_1_le: |
|
6571 assumes "monoidal opp" |
6449 shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a..b::real} = neutral opp) \<and> |
6572 shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a..b::real} = neutral opp) \<and> |
6450 (\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> opp (f{a..c})(f{c..b}) = f {a..b}))" |
6573 (\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}))" |
6451 unfolding operative_1_lt[OF assms] |
6574 unfolding operative_1_lt[OF assms] |
6452 proof safe fix a b c::"real" assume as:"\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}" "a < c" "c < b" |
6575 proof safe |
6453 show "opp (f {a..c}) (f {c..b}) = f {a..b}" apply(rule as(1)[rule_format]) using as(2-) by auto |
6576 fix a b c :: real |
6454 next fix a b c ::"real" assume "\<forall>a b. b \<le> a \<longrightarrow> f {a..b} = neutral opp" |
6577 assume as: |
6455 "\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}" "a \<le> c" "c \<le> b" |
6578 "\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}" |
|
6579 "a < c" |
|
6580 "c < b" |
|
6581 show "opp (f {a..c}) (f {c..b}) = f {a..b}" |
|
6582 apply (rule as(1)[rule_format]) |
|
6583 using as(2-) |
|
6584 apply auto |
|
6585 done |
|
6586 next |
|
6587 fix a b c :: real |
|
6588 assume "\<forall>a b. b \<le> a \<longrightarrow> f {a..b} = neutral opp" |
|
6589 and "\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}" |
|
6590 and "a \<le> c" |
|
6591 and "c \<le> b" |
6456 note as = this[rule_format] |
6592 note as = this[rule_format] |
6457 show "opp (f {a..c}) (f {c..b}) = f {a..b}" |
6593 show "opp (f {a..c}) (f {c..b}) = f {a..b}" |
6458 proof(cases "c = a \<or> c = b") |
6594 proof (cases "c = a \<or> c = b") |
6459 case False thus ?thesis apply-apply(subst as(2)) using as(3-) by(auto) |
6595 case False |
6460 next case True thus ?thesis apply- |
6596 then show ?thesis |
6461 proof(erule disjE) assume *:"c=a" hence "f {a..c} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto |
6597 apply - |
6462 thus ?thesis using assms unfolding * by auto |
6598 apply (subst as(2)) |
6463 next assume *:"c=b" hence "f {c..b} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto |
6599 using as(3-) |
6464 thus ?thesis using assms unfolding * by auto qed qed qed |
6600 apply auto |
|
6601 done |
|
6602 next |
|
6603 case True |
|
6604 then show ?thesis |
|
6605 proof |
|
6606 assume *: "c = a" |
|
6607 then have "f {a..c} = neutral opp" |
|
6608 apply - |
|
6609 apply (rule as(1)[rule_format]) |
|
6610 apply auto |
|
6611 done |
|
6612 then show ?thesis |
|
6613 using assms unfolding * by auto |
|
6614 next |
|
6615 assume *: "c = b" |
|
6616 then have "f {c..b} = neutral opp" |
|
6617 apply - |
|
6618 apply (rule as(1)[rule_format]) |
|
6619 apply auto |
|
6620 done |
|
6621 then show ?thesis |
|
6622 using assms unfolding * by auto |
|
6623 qed |
|
6624 qed |
|
6625 qed |
|
6626 |
6465 |
6627 |
6466 subsection {* Special case of additivity we need for the FCT. *} |
6628 subsection {* Special case of additivity we need for the FCT. *} |
6467 |
6629 |
6468 lemma interval_bound_sing[simp]: "interval_upperbound {a} = a" "interval_lowerbound {a} = a" |
6630 lemma interval_bound_sing[simp]: |
6469 unfolding interval_upperbound_def interval_lowerbound_def by (auto simp: euclidean_representation) |
6631 "interval_upperbound {a} = a" |
6470 |
6632 "interval_lowerbound {a} = a" |
6471 lemma additive_tagged_division_1: fixes f::"real \<Rightarrow> 'a::real_normed_vector" |
6633 unfolding interval_upperbound_def interval_lowerbound_def |
6472 assumes "a \<le> b" "p tagged_division_of {a..b}" |
6634 by (auto simp: euclidean_representation) |
|
6635 |
|
6636 lemma additive_tagged_division_1: |
|
6637 fixes f :: "real \<Rightarrow> 'a::real_normed_vector" |
|
6638 assumes "a \<le> b" |
|
6639 and "p tagged_division_of {a..b}" |
6473 shows "setsum (\<lambda>(x,k). f(interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a" |
6640 shows "setsum (\<lambda>(x,k). f(interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a" |
6474 proof- let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))" |
6641 proof - |
6475 have ***:"\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i" using assms by auto |
6642 let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))" |
6476 have *:"operative op + ?f" unfolding operative_1_lt[OF monoidal_monoid] interval_eq_empty by auto |
6643 have ***: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i" |
6477 have **:"{a..b} \<noteq> {}" using assms(1) by auto note operative_tagged_division[OF monoidal_monoid * assms(2)] |
6644 using assms by auto |
|
6645 have *: "operative op + ?f" |
|
6646 unfolding operative_1_lt[OF monoidal_monoid] interval_eq_empty by auto |
|
6647 have **: "{a..b} \<noteq> {}" |
|
6648 using assms(1) by auto note operative_tagged_division[OF monoidal_monoid * assms(2)] |
6478 note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric] |
6649 note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric] |
6479 show ?thesis unfolding * apply(subst setsum_iterate[symmetric]) defer |
6650 show ?thesis |
6480 apply(rule setsum_cong2) unfolding split_paired_all split_conv using assms(2) by auto qed |
6651 unfolding * |
|
6652 apply (subst setsum_iterate[symmetric]) |
|
6653 defer |
|
6654 apply (rule setsum_cong2) |
|
6655 unfolding split_paired_all split_conv |
|
6656 using assms(2) |
|
6657 apply auto |
|
6658 done |
|
6659 qed |
|
6660 |
6481 |
6661 |
6482 subsection {* A useful lemma allowing us to factor out the content size. *} |
6662 subsection {* A useful lemma allowing us to factor out the content size. *} |
6483 |
6663 |
6484 lemma has_integral_factor_content: |
6664 lemma has_integral_factor_content: |
6485 "(f has_integral i) {a..b} \<longleftrightarrow> (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p |
6665 "(f has_integral i) {a..b} \<longleftrightarrow> |
6486 \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content {a..b}))" |
6666 (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> |
6487 proof(cases "content {a..b} = 0") |
6667 norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content {a..b}))" |
6488 case True show ?thesis unfolding has_integral_null_eq[OF True] apply safe |
6668 proof (cases "content {a..b} = 0") |
6489 apply(rule,rule,rule gauge_trivial,safe) unfolding setsum_content_null[OF True] True defer |
6669 case True |
6490 apply(erule_tac x=1 in allE,safe) defer apply(rule fine_division_exists[of _ a b],assumption) |
6670 show ?thesis |
6491 apply(erule_tac x=p in allE) unfolding setsum_content_null[OF True] by auto |
6671 unfolding has_integral_null_eq[OF True] |
6492 next case False note F = this[unfolded content_lt_nz[symmetric]] |
6672 apply safe |
6493 let ?P = "\<lambda>e opp. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> opp (norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i)) e)" |
6673 apply (rule, rule, rule gauge_trivial, safe) |
6494 show ?thesis apply(subst has_integral) |
6674 unfolding setsum_content_null[OF True] True |
6495 proof safe fix e::real assume e:"e>0" |
6675 defer |
6496 { assume "\<forall>e>0. ?P e op <" thus "?P (e * content {a..b}) op \<le>" apply(erule_tac x="e * content {a..b}" in allE) |
6676 apply (erule_tac x=1 in allE) |
6497 apply(erule impE) defer apply(erule exE,rule_tac x=d in exI) |
6677 apply safe |
6498 using F e by(auto simp add:field_simps intro:mult_pos_pos) } |
6678 defer |
6499 { assume "\<forall>e>0. ?P (e * content {a..b}) op \<le>" thus "?P e op <" apply(erule_tac x="e / 2 / content {a..b}" in allE) |
6679 apply (rule fine_division_exists[of _ a b]) |
6500 apply(erule impE) defer apply(erule exE,rule_tac x=d in exI) |
6680 apply assumption |
6501 using F e by(auto simp add:field_simps intro:mult_pos_pos) } qed qed |
6681 apply (erule_tac x=p in allE) |
|
6682 unfolding setsum_content_null[OF True] |
|
6683 apply auto |
|
6684 done |
|
6685 next |
|
6686 case False |
|
6687 note F = this[unfolded content_lt_nz[symmetric]] |
|
6688 let ?P = "\<lambda>e opp. \<exists>d. gauge d \<and> |
|
6689 (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> opp (norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i)) e)" |
|
6690 show ?thesis |
|
6691 apply (subst has_integral) |
|
6692 proof safe |
|
6693 fix e :: real |
|
6694 assume e: "e > 0" |
|
6695 { |
|
6696 assume "\<forall>e>0. ?P e op <" |
|
6697 then show "?P (e * content {a..b}) op \<le>" |
|
6698 apply (erule_tac x="e * content {a..b}" in allE) |
|
6699 apply (erule impE) |
|
6700 defer |
|
6701 apply (erule exE,rule_tac x=d in exI) |
|
6702 using F e |
|
6703 apply (auto simp add:field_simps intro:mult_pos_pos) |
|
6704 done |
|
6705 } |
|
6706 { |
|
6707 assume "\<forall>e>0. ?P (e * content {a..b}) op \<le>" |
|
6708 then show "?P e op <" |
|
6709 apply (erule_tac x="e / 2 / content {a..b}" in allE) |
|
6710 apply (erule impE) |
|
6711 defer |
|
6712 apply (erule exE,rule_tac x=d in exI) |
|
6713 using F e |
|
6714 apply (auto simp add: field_simps intro: mult_pos_pos) |
|
6715 done |
|
6716 } |
|
6717 qed |
|
6718 qed |
|
6719 |
6502 |
6720 |
6503 subsection {* Fundamental theorem of calculus. *} |
6721 subsection {* Fundamental theorem of calculus. *} |
6504 |
6722 |
6505 lemma interval_bounds_real: assumes "a\<le>(b::real)" |
6723 lemma interval_bounds_real: |
6506 shows "interval_upperbound {a..b} = b" "interval_lowerbound {a..b} = a" |
6724 fixes q b :: real |
6507 apply(rule_tac[!] interval_bounds) using assms by auto |
6725 assumes "a \<le> b" |
6508 |
6726 shows "interval_upperbound {a..b} = b" |
6509 lemma fundamental_theorem_of_calculus: fixes f::"real \<Rightarrow> 'a::banach" |
6727 and "interval_lowerbound {a..b} = a" |
6510 assumes "a \<le> b" "\<forall>x\<in>{a..b}. (f has_vector_derivative f' x) (at x within {a..b})" |
6728 apply (rule_tac[!] interval_bounds) |
6511 shows "(f' has_integral (f b - f a)) ({a..b})" |
6729 using assms |
6512 unfolding has_integral_factor_content |
6730 apply auto |
6513 proof safe fix e::real assume e:"e>0" |
6731 done |
|
6732 |
|
6733 lemma fundamental_theorem_of_calculus: |
|
6734 fixes f :: "real \<Rightarrow> 'a::banach" |
|
6735 assumes "a \<le> b" |
|
6736 and "\<forall>x\<in>{a..b}. (f has_vector_derivative f' x) (at x within {a..b})" |
|
6737 shows "(f' has_integral (f b - f a)) {a..b}" |
|
6738 unfolding has_integral_factor_content |
|
6739 proof safe |
|
6740 fix e :: real |
|
6741 assume e: "e > 0" |
6514 note assm = assms(2)[unfolded has_vector_derivative_def has_derivative_within_alt] |
6742 note assm = assms(2)[unfolded has_vector_derivative_def has_derivative_within_alt] |
6515 have *:"\<And>P Q. \<forall>x\<in>{a..b}. P x \<and> (\<forall>e>0. \<exists>d>0. Q x e d) \<Longrightarrow> \<forall>x. \<exists>(d::real)>0. x\<in>{a..b} \<longrightarrow> Q x e d" using e by blast |
6743 have *: "\<And>P Q. \<forall>x\<in>{a..b}. P x \<and> (\<forall>e>0. \<exists>d>0. Q x e d) \<Longrightarrow> \<forall>x. \<exists>(d::real)>0. x\<in>{a..b} \<longrightarrow> Q x e d" |
6516 note this[OF assm,unfolded gauge_existence_lemma] from choice[OF this,unfolded Ball_def[symmetric]] |
6744 using e by blast |
6517 guess d .. note d=conjunctD2[OF this[rule_format],rule_format] |
6745 note this[OF assm,unfolded gauge_existence_lemma] |
|
6746 from choice[OF this,unfolded Ball_def[symmetric]] guess d .. |
|
6747 note d=conjunctD2[OF this[rule_format],rule_format] |
6518 show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> |
6748 show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> |
6519 norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b})" |
6749 norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b})" |
6520 apply(rule_tac x="\<lambda>x. ball x (d x)" in exI,safe) |
6750 apply (rule_tac x="\<lambda>x. ball x (d x)" in exI) |
6521 apply(rule gauge_ball_dependent,rule,rule d(1)) |
6751 apply safe |
6522 proof- fix p assume as:"p tagged_division_of {a..b}" "(\<lambda>x. ball x (d x)) fine p" |
6752 apply (rule gauge_ball_dependent) |
|
6753 apply rule |
|
6754 apply (rule d(1)) |
|
6755 proof - |
|
6756 fix p |
|
6757 assume as: "p tagged_division_of {a..b}" "(\<lambda>x. ball x (d x)) fine p" |
6523 show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}" |
6758 show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}" |
6524 unfolding content_real[OF assms(1)] additive_tagged_division_1[OF assms(1) as(1),of f,symmetric] |
6759 unfolding content_real[OF assms(1)] additive_tagged_division_1[OF assms(1) as(1),of f,symmetric] |
6525 unfolding additive_tagged_division_1[OF assms(1) as(1),of "\<lambda>x. x",symmetric] |
6760 unfolding additive_tagged_division_1[OF assms(1) as(1),of "\<lambda>x. x",symmetric] |
6526 unfolding setsum_right_distrib defer unfolding setsum_subtractf[symmetric] |
6761 unfolding setsum_right_distrib |
6527 proof(rule setsum_norm_le,safe) fix x k assume "(x,k)\<in>p" |
6762 defer |
6528 note xk = tagged_division_ofD(2-4)[OF as(1) this] from this(3) guess u v apply-by(erule exE)+ note k=this |
6763 unfolding setsum_subtractf[symmetric] |
6529 have *:"u \<le> v" using xk unfolding k by auto |
6764 proof (rule setsum_norm_le,safe) |
6530 have ball:"\<forall>xa\<in>k. xa \<in> ball x (d x)" using as(2)[unfolded fine_def,rule_format,OF `(x,k)\<in>p`, |
6765 fix x k |
6531 unfolded split_conv subset_eq] . |
6766 assume "(x, k) \<in> p" |
|
6767 note xk = tagged_division_ofD(2-4)[OF as(1) this] |
|
6768 from this(3) guess u v by (elim exE) note k=this |
|
6769 have *: "u \<le> v" |
|
6770 using xk unfolding k by auto |
|
6771 have ball: "\<forall>xa\<in>k. xa \<in> ball x (d x)" |
|
6772 using as(2)[unfolded fine_def,rule_format,OF `(x,k)\<in>p`,unfolded split_conv subset_eq] . |
6532 have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le> |
6773 have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le> |
6533 norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)" |
6774 norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)" |
6534 apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm]) |
6775 apply (rule order_trans[OF _ norm_triangle_ineq4]) |
6535 unfolding scaleR_diff_left by(auto simp add:algebra_simps) |
6776 apply (rule eq_refl) |
6536 also have "... \<le> e * norm (u - x) + e * norm (v - x)" |
6777 apply (rule arg_cong[where f=norm]) |
6537 apply(rule add_mono) apply(rule d(2)[of "x" "u",unfolded o_def]) prefer 4 |
6778 unfolding scaleR_diff_left |
6538 apply(rule d(2)[of "x" "v",unfolded o_def]) |
6779 apply (auto simp add:algebra_simps) |
|
6780 done |
|
6781 also have "\<dots> \<le> e * norm (u - x) + e * norm (v - x)" |
|
6782 apply (rule add_mono) |
|
6783 apply (rule d(2)[of "x" "u",unfolded o_def]) |
|
6784 prefer 4 |
|
6785 apply (rule d(2)[of "x" "v",unfolded o_def]) |
6539 using ball[rule_format,of u] ball[rule_format,of v] |
6786 using ball[rule_format,of u] ball[rule_format,of v] |
6540 using xk(1-2) unfolding k subset_eq by(auto simp add:dist_real_def) |
6787 using xk(1-2) |
6541 also have "... \<le> e * (interval_upperbound k - interval_lowerbound k)" |
6788 unfolding k subset_eq |
6542 unfolding k interval_bounds_real[OF *] using xk(1) unfolding k by(auto simp add:dist_real_def field_simps) |
6789 apply (auto simp add:dist_real_def) |
|
6790 done |
|
6791 also have "\<dots> \<le> e * (interval_upperbound k - interval_lowerbound k)" |
|
6792 unfolding k interval_bounds_real[OF *] |
|
6793 using xk(1) |
|
6794 unfolding k |
|
6795 by (auto simp add: dist_real_def field_simps) |
6543 finally show "norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k))) \<le> |
6796 finally show "norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k))) \<le> |
6544 e * (interval_upperbound k - interval_lowerbound k)" unfolding k interval_bounds_real[OF *] content_real[OF *] . |
6797 e * (interval_upperbound k - interval_lowerbound k)" |
6545 qed qed qed |
6798 unfolding k interval_bounds_real[OF *] content_real[OF *] . |
|
6799 qed |
|
6800 qed |
|
6801 qed |
|
6802 |
6546 |
6803 |
6547 subsection {* Attempt a systematic general set of "offset" results for components. *} |
6804 subsection {* Attempt a systematic general set of "offset" results for components. *} |
6548 |
6805 |
6549 lemma gauge_modify: |
6806 lemma gauge_modify: |
6550 assumes "(\<forall>s. open s \<longrightarrow> open {x. f(x) \<in> s})" "gauge d" |
6807 assumes "(\<forall>s. open s \<longrightarrow> open {x. f(x) \<in> s})" "gauge d" |
6551 shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})" |
6808 shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})" |
6552 using assms unfolding gauge_def apply safe defer apply(erule_tac x="f x" in allE) |
6809 using assms |
6553 apply(erule_tac x="d (f x)" in allE) by auto |
6810 unfolding gauge_def |
|
6811 apply safe |
|
6812 defer |
|
6813 apply (erule_tac x="f x" in allE) |
|
6814 apply (erule_tac x="d (f x)" in allE) |
|
6815 apply auto |
|
6816 done |
|
6817 |
6554 |
6818 |
6555 subsection {* Only need trivial subintervals if the interval itself is trivial. *} |
6819 subsection {* Only need trivial subintervals if the interval itself is trivial. *} |
6556 |
6820 |
6557 lemma division_of_nontrivial: fixes s::"('a::ordered_euclidean_space) set set" |
6821 lemma division_of_nontrivial: |
6558 assumes "s division_of {a..b}" "content({a..b}) \<noteq> 0" |
6822 fixes s :: "'a::ordered_euclidean_space set set" |
6559 shows "{k. k \<in> s \<and> content k \<noteq> 0} division_of {a..b}" using assms(1) apply- |
6823 assumes "s division_of {a..b}" |
6560 proof(induct "card s" arbitrary:s rule:nat_less_induct) |
6824 and "content {a..b} \<noteq> 0" |
6561 fix s::"'a set set" assume assm:"s division_of {a..b}" |
6825 shows "{k. k \<in> s \<and> content k \<noteq> 0} division_of {a..b}" |
6562 "\<forall>m<card s. \<forall>x. m = card x \<longrightarrow> x division_of {a..b} \<longrightarrow> {k \<in> x. content k \<noteq> 0} division_of {a..b}" |
6826 using assms(1) |
6563 note s = division_ofD[OF assm(1)] let ?thesis = "{k \<in> s. content k \<noteq> 0} division_of {a..b}" |
6827 apply - |
6564 { presume *:"{k \<in> s. content k \<noteq> 0} \<noteq> s \<Longrightarrow> ?thesis" |
6828 proof (induct "card s" arbitrary: s rule: nat_less_induct) |
6565 show ?thesis apply cases defer apply(rule *,assumption) using assm(1) by auto } |
6829 fix s::"'a set set" |
6566 assume noteq:"{k \<in> s. content k \<noteq> 0} \<noteq> s" |
6830 assume assm: "s division_of {a..b}" |
6567 then obtain k where k:"k\<in>s" "content k = 0" by auto |
6831 "\<forall>m<card s. \<forall>x. m = card x \<longrightarrow> |
6568 from s(4)[OF k(1)] guess c d apply-by(erule exE)+ note k=k this |
6832 x division_of {a..b} \<longrightarrow> {k \<in> x. content k \<noteq> 0} division_of {a..b}" |
6569 from k have "card s > 0" unfolding card_gt_0_iff using assm(1) by auto |
6833 note s = division_ofD[OF assm(1)] |
6570 hence card:"card (s - {k}) < card s" using assm(1) k(1) apply(subst card_Diff_singleton_if) by auto |
6834 let ?thesis = "{k \<in> s. content k \<noteq> 0} division_of {a..b}" |
6571 have *:"closed (\<Union>(s - {k}))" apply(rule closed_Union) defer apply rule apply(drule DiffD1,drule s(4)) |
6835 { |
6572 apply safe apply(rule closed_interval) using assm(1) by auto |
6836 presume *: "{k \<in> s. content k \<noteq> 0} \<noteq> s \<Longrightarrow> ?thesis" |
6573 have "k \<subseteq> \<Union>(s - {k})" apply safe apply(rule *[unfolded closed_limpt,rule_format]) unfolding islimpt_approachable |
6837 show ?thesis |
6574 proof safe fix x and e::real assume as:"x\<in>k" "e>0" |
6838 apply cases |
|
6839 defer |
|
6840 apply (rule *) |
|
6841 apply assumption |
|
6842 using assm(1) |
|
6843 apply auto |
|
6844 done |
|
6845 } |
|
6846 assume noteq: "{k \<in> s. content k \<noteq> 0} \<noteq> s" |
|
6847 then obtain k where k: "k \<in> s" "content k = 0" |
|
6848 by auto |
|
6849 from s(4)[OF k(1)] guess c d by (elim exE) note k=k this |
|
6850 from k have "card s > 0" |
|
6851 unfolding card_gt_0_iff using assm(1) by auto |
|
6852 then have card: "card (s - {k}) < card s" |
|
6853 using assm(1) k(1) |
|
6854 apply (subst card_Diff_singleton_if) |
|
6855 apply auto |
|
6856 done |
|
6857 have *: "closed (\<Union>(s - {k}))" |
|
6858 apply (rule closed_Union) |
|
6859 defer |
|
6860 apply rule |
|
6861 apply (drule DiffD1,drule s(4)) |
|
6862 apply safe |
|
6863 apply (rule closed_interval) |
|
6864 using assm(1) |
|
6865 apply auto |
|
6866 done |
|
6867 have "k \<subseteq> \<Union>(s - {k})" |
|
6868 apply safe |
|
6869 apply (rule *[unfolded closed_limpt,rule_format]) |
|
6870 unfolding islimpt_approachable |
|
6871 proof safe |
|
6872 fix x |
|
6873 fix e :: real |
|
6874 assume as: "x \<in> k" "e > 0" |
6575 from k(2)[unfolded k content_eq_0] guess i .. |
6875 from k(2)[unfolded k content_eq_0] guess i .. |
6576 hence i:"c\<bullet>i = d\<bullet>i" "i\<in>Basis" using s(3)[OF k(1),unfolded k] unfolding interval_ne_empty by auto |
6876 then have i:"c\<bullet>i = d\<bullet>i" "i\<in>Basis" |
6577 hence xi:"x\<bullet>i = d\<bullet>i" using as unfolding k mem_interval by (metis antisym) |
6877 using s(3)[OF k(1),unfolded k] unfolding interval_ne_empty by auto |
6578 def y \<equiv> "(\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i + |
6878 then have xi: "x\<bullet>i = d\<bullet>i" |
6579 min e (b\<bullet>i - c\<bullet>i) / 2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i) / 2 else x\<bullet>j) *\<^sub>R j)::'a" |
6879 using as unfolding k mem_interval by (metis antisym) |
6580 show "\<exists>x'\<in>\<Union>(s - {k}). x' \<noteq> x \<and> dist x' x < e" apply(rule_tac x=y in bexI) |
6880 def y \<equiv> "\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i + |
6581 proof have "d \<in> {c..d}" using s(3)[OF k(1)] unfolding k interval_eq_empty mem_interval by(fastforce simp add: not_less) |
6881 min e (b\<bullet>i - c\<bullet>i) / 2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i) / 2 else x\<bullet>j) *\<^sub>R j" |
6582 hence "d \<in> {a..b}" using s(2)[OF k(1)] unfolding k by auto note di = this[unfolded mem_interval,THEN bspec[where x=i]] |
6882 show "\<exists>x'\<in>\<Union>(s - {k}). x' \<noteq> x \<and> dist x' x < e" |
6583 hence xyi:"y\<bullet>i \<noteq> x\<bullet>i" |
6883 apply (rule_tac x=y in bexI) |
6584 unfolding y_def i xi using as(2) assms(2)[unfolded content_eq_0] i(2) |
6884 proof |
|
6885 have "d \<in> {c..d}" |
|
6886 using s(3)[OF k(1)] |
|
6887 unfolding k interval_eq_empty mem_interval |
|
6888 by (fastforce simp add: not_less) |
|
6889 then have "d \<in> {a..b}" |
|
6890 using s(2)[OF k(1)] |
|
6891 unfolding k |
|
6892 by auto |
|
6893 note di = this[unfolded mem_interval,THEN bspec[where x=i]] |
|
6894 then have xyi: "y\<bullet>i \<noteq> x\<bullet>i" |
|
6895 unfolding y_def i xi |
|
6896 using as(2) assms(2)[unfolded content_eq_0] i(2) |
6585 by (auto elim!: ballE[of _ _ i]) |
6897 by (auto elim!: ballE[of _ _ i]) |
6586 thus "y \<noteq> x" unfolding euclidean_eq_iff[where 'a='a] using i by auto |
6898 then show "y \<noteq> x" |
6587 have *:"Basis = insert i (Basis - {i})" using i by auto |
6899 unfolding euclidean_eq_iff[where 'a='a] using i by auto |
6588 have "norm (y - x) < e + setsum (\<lambda>i. 0) Basis" apply(rule le_less_trans[OF norm_le_l1]) |
6900 have *: "Basis = insert i (Basis - {i})" |
6589 apply(subst *,subst setsum_insert) prefer 3 apply(rule add_less_le_mono) |
6901 using i by auto |
6590 proof- |
6902 have "norm (y - x) < e + setsum (\<lambda>i. 0) Basis" |
|
6903 apply (rule le_less_trans[OF norm_le_l1]) |
|
6904 apply (subst *) |
|
6905 apply (subst setsum_insert) |
|
6906 prefer 3 |
|
6907 apply (rule add_less_le_mono) |
|
6908 proof - |
6591 show "\<bar>(y - x) \<bullet> i\<bar> < e" |
6909 show "\<bar>(y - x) \<bullet> i\<bar> < e" |
6592 using di as(2) y_def i xi by (auto simp: inner_simps) |
6910 using di as(2) y_def i xi by (auto simp: inner_simps) |
6593 show "(\<Sum>i\<in>Basis - {i}. \<bar>(y - x) \<bullet> i\<bar>) \<le> (\<Sum>i\<in>Basis. 0)" |
6911 show "(\<Sum>i\<in>Basis - {i}. \<bar>(y - x) \<bullet> i\<bar>) \<le> (\<Sum>i\<in>Basis. 0)" |
6594 unfolding y_def by (auto simp: inner_simps) |
6912 unfolding y_def by (auto simp: inner_simps) |
6595 qed auto thus "dist y x < e" unfolding dist_norm by auto |
6913 qed auto |
6596 have "y\<notin>k" unfolding k mem_interval apply rule apply(erule_tac x=i in ballE) using xyi k i xi by auto |
6914 then show "dist y x < e" |
6597 moreover have "y \<in> \<Union>s" |
6915 unfolding dist_norm by auto |
6598 using set_rev_mp[OF as(1) s(2)[OF k(1)]] as(2) di i unfolding s mem_interval y_def |
6916 have "y \<notin> k" |
|
6917 unfolding k mem_interval |
|
6918 apply rule |
|
6919 apply (erule_tac x=i in ballE) |
|
6920 using xyi k i xi |
|
6921 apply auto |
|
6922 done |
|
6923 moreover |
|
6924 have "y \<in> \<Union>s" |
|
6925 using set_rev_mp[OF as(1) s(2)[OF k(1)]] as(2) di i |
|
6926 unfolding s mem_interval y_def |
6599 by (auto simp: field_simps elim!: ballE[of _ _ i]) |
6927 by (auto simp: field_simps elim!: ballE[of _ _ i]) |
6600 ultimately show "y \<in> \<Union>(s - {k})" by auto |
6928 ultimately |
6601 qed qed hence "\<Union>(s - {k}) = {a..b}" unfolding s(6)[symmetric] by auto |
6929 show "y \<in> \<Union>(s - {k})" by auto |
6602 hence "{ka \<in> s - {k}. content ka \<noteq> 0} division_of {a..b}" apply-apply(rule assm(2)[rule_format,OF card refl]) |
6930 qed |
6603 apply(rule division_ofI) defer apply(rule_tac[1-4] s) using assm(1) by auto |
6931 qed |
6604 moreover have "{ka \<in> s - {k}. content ka \<noteq> 0} = {k \<in> s. content k \<noteq> 0}" using k by auto ultimately show ?thesis by auto qed |
6932 then have "\<Union>(s - {k}) = {a..b}" |
|
6933 unfolding s(6)[symmetric] by auto |
|
6934 then have "{ka \<in> s - {k}. content ka \<noteq> 0} division_of {a..b}" |
|
6935 apply - |
|
6936 apply (rule assm(2)[rule_format,OF card refl]) |
|
6937 apply (rule division_ofI) |
|
6938 defer |
|
6939 apply (rule_tac[1-4] s) |
|
6940 using assm(1) |
|
6941 apply auto |
|
6942 done |
|
6943 moreover |
|
6944 have "{ka \<in> s - {k}. content ka \<noteq> 0} = {k \<in> s. content k \<noteq> 0}" |
|
6945 using k by auto |
|
6946 ultimately show ?thesis by auto |
|
6947 qed |
|
6948 |
6605 |
6949 |
6606 subsection {* Integrability on subintervals. *} |
6950 subsection {* Integrability on subintervals. *} |
6607 |
6951 |
6608 lemma operative_integrable: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach" shows |
6952 lemma operative_integrable: |
6609 "operative op \<and> (\<lambda>i. f integrable_on i)" |
6953 fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
6610 unfolding operative_def neutral_and apply safe apply(subst integrable_on_def) |
6954 shows "operative op \<and> (\<lambda>i. f integrable_on i)" |
6611 unfolding has_integral_null_eq apply(rule,rule refl) apply(rule,assumption,assumption)+ |
6955 unfolding operative_def neutral_and |
6612 unfolding integrable_on_def by(auto intro!: has_integral_split) |
6956 apply safe |
6613 |
6957 apply (subst integrable_on_def) |
6614 lemma integrable_subinterval: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
6958 unfolding has_integral_null_eq |
6615 assumes "f integrable_on {a..b}" "{c..d} \<subseteq> {a..b}" shows "f integrable_on {c..d}" |
6959 apply (rule, rule refl) |
6616 apply(cases "{c..d} = {}") defer apply(rule partial_division_extend_1[OF assms(2)],assumption) |
6960 apply (rule, assumption, assumption)+ |
6617 using operative_division_and[OF operative_integrable,symmetric,of _ _ _ f] assms(1) by auto |
6961 unfolding integrable_on_def |
|
6962 by (auto intro!: has_integral_split) |
|
6963 |
|
6964 lemma integrable_subinterval: |
|
6965 fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
|
6966 assumes "f integrable_on {a..b}" |
|
6967 and "{c..d} \<subseteq> {a..b}" |
|
6968 shows "f integrable_on {c..d}" |
|
6969 apply (cases "{c..d} = {}") |
|
6970 defer |
|
6971 apply (rule partial_division_extend_1[OF assms(2)],assumption) |
|
6972 using operative_division_and[OF operative_integrable,symmetric,of _ _ _ f] assms(1) |
|
6973 apply auto |
|
6974 done |
|
6975 |
6618 |
6976 |
6619 subsection {* Combining adjacent intervals in 1 dimension. *} |
6977 subsection {* Combining adjacent intervals in 1 dimension. *} |
6620 |
6978 |
6621 lemma has_integral_combine: assumes "(a::real) \<le> c" "c \<le> b" |
6979 lemma has_integral_combine: |
6622 "(f has_integral i) {a..c}" "(f has_integral (j::'a::banach)) {c..b}" |
6980 fixes a b c :: real |
|
6981 assumes "a \<le> c" |
|
6982 and "c \<le> b" |
|
6983 and "(f has_integral i) {a..c}" |
|
6984 and "(f has_integral (j::'a::banach)) {c..b}" |
6623 shows "(f has_integral (i + j)) {a..b}" |
6985 shows "(f has_integral (i + j)) {a..b}" |
6624 proof- note operative_integral[of f, unfolded operative_1_le[OF monoidal_lifted[OF monoidal_monoid]]] |
6986 proof - |
6625 note conjunctD2[OF this,rule_format] note * = this(2)[OF conjI[OF assms(1-2)],unfolded if_P[OF assms(3)]] |
6987 note operative_integral[of f, unfolded operative_1_le[OF monoidal_lifted[OF monoidal_monoid]]] |
6626 hence "f integrable_on {a..b}" apply- apply(rule ccontr) apply(subst(asm) if_P) defer |
6988 note conjunctD2[OF this,rule_format] |
6627 apply(subst(asm) if_P) using assms(3-) by auto |
6989 note * = this(2)[OF conjI[OF assms(1-2)],unfolded if_P[OF assms(3)]] |
6628 with * show ?thesis apply-apply(subst(asm) if_P) defer apply(subst(asm) if_P) defer apply(subst(asm) if_P) |
6990 then have "f integrable_on {a..b}" |
6629 unfolding lifted.simps using assms(3-) by(auto simp add: integrable_on_def integral_unique) qed |
6991 apply - |
6630 |
6992 apply (rule ccontr) |
6631 lemma integral_combine: fixes f::"real \<Rightarrow> 'a::banach" |
6993 apply (subst(asm) if_P) |
6632 assumes "a \<le> c" "c \<le> b" "f integrable_on ({a..b})" |
6994 defer |
6633 shows "integral {a..c} f + integral {c..b} f = integral({a..b}) f" |
6995 apply (subst(asm) if_P) |
6634 apply(rule integral_unique[symmetric]) apply(rule has_integral_combine[OF assms(1-2)]) |
6996 using assms(3-) |
6635 apply(rule_tac[!] integrable_integral integrable_subinterval[OF assms(3)])+ using assms(1-2) by auto |
6997 apply auto |
6636 |
6998 done |
6637 lemma integrable_combine: fixes f::"real \<Rightarrow> 'a::banach" |
6999 with * |
6638 assumes "a \<le> c" "c \<le> b" "f integrable_on {a..c}" "f integrable_on {c..b}" |
7000 show ?thesis |
6639 shows "f integrable_on {a..b}" using assms unfolding integrable_on_def by(fastforce intro!:has_integral_combine) |
7001 apply - |
|
7002 apply (subst(asm) if_P) |
|
7003 defer |
|
7004 apply (subst(asm) if_P) |
|
7005 defer |
|
7006 apply (subst(asm) if_P) |
|
7007 unfolding lifted.simps |
|
7008 using assms(3-) |
|
7009 apply (auto simp add: integrable_on_def integral_unique) |
|
7010 done |
|
7011 qed |
|
7012 |
|
7013 lemma integral_combine: |
|
7014 fixes f :: "real \<Rightarrow> 'a::banach" |
|
7015 assumes "a \<le> c" |
|
7016 and "c \<le> b" |
|
7017 and "f integrable_on {a..b}" |
|
7018 shows "integral {a..c} f + integral {c..b} f = integral {a..b} f" |
|
7019 apply (rule integral_unique[symmetric]) |
|
7020 apply (rule has_integral_combine[OF assms(1-2)]) |
|
7021 apply (rule_tac[!] integrable_integral integrable_subinterval[OF assms(3)])+ |
|
7022 using assms(1-2) |
|
7023 apply auto |
|
7024 done |
|
7025 |
|
7026 lemma integrable_combine: |
|
7027 fixes f :: "real \<Rightarrow> 'a::banach" |
|
7028 assumes "a \<le> c" |
|
7029 and "c \<le> b" |
|
7030 and "f integrable_on {a..c}" |
|
7031 and "f integrable_on {c..b}" |
|
7032 shows "f integrable_on {a..b}" |
|
7033 using assms |
|
7034 unfolding integrable_on_def |
|
7035 by (fastforce intro!:has_integral_combine) |
|
7036 |
6640 |
7037 |
6641 subsection {* Reduce integrability to "local" integrability. *} |
7038 subsection {* Reduce integrability to "local" integrability. *} |
6642 |
7039 |
6643 lemma integrable_on_little_subintervals: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
7040 lemma integrable_on_little_subintervals: |
6644 assumes "\<forall>x\<in>{a..b}. \<exists>d>0. \<forall>u v. x \<in> {u..v} \<and> {u..v} \<subseteq> ball x d \<and> {u..v} \<subseteq> {a..b} \<longrightarrow> f integrable_on {u..v}" |
7041 fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach" |
|
7042 assumes "\<forall>x\<in>{a..b}. \<exists>d>0. \<forall>u v. x \<in> {u..v} \<and> {u..v} \<subseteq> ball x d \<and> {u..v} \<subseteq> {a..b} \<longrightarrow> |
|
7043 f integrable_on {u..v}" |
6645 shows "f integrable_on {a..b}" |
7044 shows "f integrable_on {a..b}" |
6646 proof- have "\<forall>x. \<exists>d. x\<in>{a..b} \<longrightarrow> d>0 \<and> (\<forall>u v. x \<in> {u..v} \<and> {u..v} \<subseteq> ball x d \<and> {u..v} \<subseteq> {a..b} \<longrightarrow> f integrable_on {u..v})" |
7045 proof - |
6647 using assms by auto note this[unfolded gauge_existence_lemma] from choice[OF this] guess d .. note d=this[rule_format] |
7046 have "\<forall>x. \<exists>d. x\<in>{a..b} \<longrightarrow> d>0 \<and> (\<forall>u v. x \<in> {u..v} \<and> {u..v} \<subseteq> ball x d \<and> {u..v} \<subseteq> {a..b} \<longrightarrow> |
6648 guess p apply(rule fine_division_exists[OF gauge_ball_dependent,of d a b]) using d by auto note p=this(1-2) |
7047 f integrable_on {u..v})" |
6649 note division_of_tagged_division[OF this(1)] note * = operative_division_and[OF operative_integrable,OF this,symmetric,of f] |
7048 using assms by auto |
6650 show ?thesis unfolding * apply safe unfolding snd_conv |
7049 note this[unfolded gauge_existence_lemma] |
6651 proof- fix x k assume "(x,k) \<in> p" note tagged_division_ofD(2-4)[OF p(1) this] fineD[OF p(2) this] |
7050 from choice[OF this] guess d .. note d=this[rule_format] |
6652 thus "f integrable_on k" apply safe apply(rule d[THEN conjunct2,rule_format,of x]) by auto qed qed |
7051 guess p |
|
7052 apply (rule fine_division_exists[OF gauge_ball_dependent,of d a b]) |
|
7053 using d |
|
7054 by auto |
|
7055 note p=this(1-2) |
|
7056 note division_of_tagged_division[OF this(1)] |
|
7057 note * = operative_division_and[OF operative_integrable,OF this,symmetric,of f] |
|
7058 show ?thesis |
|
7059 unfolding * |
|
7060 apply safe |
|
7061 unfolding snd_conv |
|
7062 proof - |
|
7063 fix x k |
|
7064 assume "(x, k) \<in> p" |
|
7065 note tagged_division_ofD(2-4)[OF p(1) this] fineD[OF p(2) this] |
|
7066 then show "f integrable_on k" |
|
7067 apply safe |
|
7068 apply (rule d[THEN conjunct2,rule_format,of x]) |
|
7069 apply auto |
|
7070 done |
|
7071 qed |
|
7072 qed |
|
7073 |
6653 |
7074 |
6654 subsection {* Second FCT or existence of antiderivative. *} |
7075 subsection {* Second FCT or existence of antiderivative. *} |
6655 |
7076 |
6656 lemma integrable_const[intro]:"(\<lambda>x. c) integrable_on {a..b}" |
7077 lemma integrable_const[intro]: "(\<lambda>x. c) integrable_on {a..b}" |
6657 unfolding integrable_on_def by(rule,rule has_integral_const) |
7078 unfolding integrable_on_def |
6658 |
7079 apply rule |
6659 lemma integral_has_vector_derivative: fixes f::"real \<Rightarrow> 'a::banach" |
7080 apply (rule has_integral_const) |
6660 assumes "continuous_on {a..b} f" "x \<in> {a..b}" |
7081 done |
|
7082 |
|
7083 lemma integral_has_vector_derivative: |
|
7084 fixes f :: "real \<Rightarrow> 'a::banach" |
|
7085 assumes "continuous_on {a..b} f" |
|
7086 and "x \<in> {a..b}" |
6661 shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})" |
7087 shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})" |
6662 unfolding has_vector_derivative_def has_derivative_within_alt |
7088 unfolding has_vector_derivative_def has_derivative_within_alt |
6663 apply safe apply(rule bounded_linear_scaleR_left) |
7089 apply safe |
6664 proof- fix e::real assume e:"e>0" |
7090 apply (rule bounded_linear_scaleR_left) |
|
7091 proof - |
|
7092 fix e :: real |
|
7093 assume e: "e > 0" |
6665 note compact_uniformly_continuous[OF assms(1) compact_interval,unfolded uniformly_continuous_on_def] |
7094 note compact_uniformly_continuous[OF assms(1) compact_interval,unfolded uniformly_continuous_on_def] |
6666 from this[rule_format,OF e] guess d apply-by(erule conjE exE)+ note d=this[rule_format] |
7095 from this[rule_format,OF e] guess d by (elim conjE exE) note d=this[rule_format] |
6667 let ?I = "\<lambda>a b. integral {a..b} f" |
7096 let ?I = "\<lambda>a b. integral {a..b} f" |
6668 show "\<exists>d>0. \<forall>y\<in>{a..b}. norm (y - x) < d \<longrightarrow> norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \<le> e * norm (y - x)" |
7097 show "\<exists>d>0. \<forall>y\<in>{a..b}. norm (y - x) < d \<longrightarrow> |
6669 proof(rule,rule,rule d,safe) case goal1 show ?case proof(cases "y < x") |
7098 norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \<le> e * norm (y - x)" |
6670 case False have "f integrable_on {a..y}" apply(rule integrable_subinterval,rule integrable_continuous) |
7099 proof (rule, rule, rule d, safe) |
6671 apply(rule assms) unfolding not_less using assms(2) goal1 by auto |
7100 case goal1 |
6672 hence *:"?I a y - ?I a x = ?I x y" unfolding algebra_simps apply(subst eq_commute) apply(rule integral_combine) |
7101 show ?case |
6673 using False unfolding not_less using assms(2) goal1 by auto |
7102 proof (cases "y < x") |
6674 have **:"norm (y - x) = content {x..y}" apply(subst content_real) using False unfolding not_less by auto |
7103 case False |
6675 show ?thesis unfolding ** apply(rule has_integral_bound[where f="(\<lambda>u. f u - f x)"]) unfolding * unfolding o_def |
7104 have "f integrable_on {a..y}" |
6676 defer apply(rule has_integral_sub) apply(rule integrable_integral) |
7105 apply (rule integrable_subinterval,rule integrable_continuous) |
6677 apply(rule integrable_subinterval,rule integrable_continuous) apply(rule assms)+ |
7106 apply (rule assms) |
6678 proof- show "{x..y} \<subseteq> {a..b}" using goal1 assms(2) by auto |
7107 unfolding not_less |
6679 have *:"y - x = norm(y - x)" using False by auto |
7108 using assms(2) goal1 |
6680 show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {x.. y}" apply(subst *) unfolding ** by auto |
7109 apply auto |
6681 show "\<forall>xa\<in>{x..y}. norm (f xa - f x) \<le> e" apply safe apply(rule less_imp_le) |
7110 done |
6682 apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto |
7111 then have *: "?I a y - ?I a x = ?I x y" |
6683 qed(insert e,auto) |
7112 unfolding algebra_simps |
6684 next case True have "f integrable_on {a..x}" apply(rule integrable_subinterval,rule integrable_continuous) |
7113 apply (subst eq_commute) |
6685 apply(rule assms)+ unfolding not_less using assms(2) goal1 by auto |
7114 apply (rule integral_combine) |
6686 hence *:"?I a x - ?I a y = ?I y x" unfolding algebra_simps apply(subst eq_commute) apply(rule integral_combine) |
7115 using False |
6687 using True using assms(2) goal1 by auto |
7116 unfolding not_less |
6688 have **:"norm (y - x) = content {y..x}" apply(subst content_real) using True unfolding not_less by auto |
7117 using assms(2) goal1 |
6689 have ***:"\<And>fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)" unfolding scaleR_left.diff by auto |
7118 apply auto |
6690 show ?thesis apply(subst ***) unfolding norm_minus_cancel ** |
7119 done |
6691 apply(rule has_integral_bound[where f="(\<lambda>u. f u - f x)"]) unfolding * unfolding o_def |
7120 have **: "norm (y - x) = content {x..y}" |
6692 defer apply(rule has_integral_sub) apply(subst minus_minus[symmetric]) unfolding minus_minus |
7121 apply (subst content_real) |
6693 apply(rule integrable_integral) apply(rule integrable_subinterval,rule integrable_continuous) apply(rule assms)+ |
7122 using False |
6694 proof- show "{y..x} \<subseteq> {a..b}" using goal1 assms(2) by auto |
7123 unfolding not_less |
6695 have *:"x - y = norm(y - x)" using True by auto |
7124 apply auto |
6696 show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {y..x}" apply(subst *) unfolding ** by auto |
7125 done |
6697 show "\<forall>xa\<in>{y..x}. norm (f xa - f x) \<le> e" apply safe apply(rule less_imp_le) |
7126 show ?thesis |
6698 apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto |
7127 unfolding ** |
6699 qed(insert e,auto) qed qed qed |
7128 apply (rule has_integral_bound[where f="(\<lambda>u. f u - f x)"]) |
6700 |
7129 unfolding * |
6701 lemma antiderivative_continuous: assumes "continuous_on {a..b::real} f" |
7130 unfolding o_def |
6702 obtains g where "\<forall>x\<in> {a..b}. (g has_vector_derivative (f(x)::_::banach)) (at x within {a..b})" |
7131 defer |
6703 apply(rule that,rule) using integral_has_vector_derivative[OF assms] by auto |
7132 apply (rule has_integral_sub) |
|
7133 apply (rule integrable_integral) |
|
7134 apply (rule integrable_subinterval) |
|
7135 apply (rule integrable_continuous) |
|
7136 apply (rule assms)+ |
|
7137 proof - |
|
7138 show "{x..y} \<subseteq> {a..b}" |
|
7139 using goal1 assms(2) by auto |
|
7140 have *: "y - x = norm (y - x)" |
|
7141 using False by auto |
|
7142 show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {x.. y}" |
|
7143 apply (subst *) |
|
7144 unfolding ** |
|
7145 apply auto |
|
7146 done |
|
7147 show "\<forall>xa\<in>{x..y}. norm (f xa - f x) \<le> e" |
|
7148 apply safe |
|
7149 apply (rule less_imp_le) |
|
7150 apply (rule d(2)[unfolded dist_norm]) |
|
7151 using assms(2) |
|
7152 using goal1 |
|
7153 apply auto |
|
7154 done |
|
7155 qed (insert e, auto) |
|
7156 next |
|
7157 case True |
|
7158 have "f integrable_on {a..x}" |
|
7159 apply (rule integrable_subinterval,rule integrable_continuous) |
|
7160 apply (rule assms)+ |
|
7161 unfolding not_less |
|
7162 using assms(2) goal1 |
|
7163 apply auto |
|
7164 done |
|
7165 then have *: "?I a x - ?I a y = ?I y x" |
|
7166 unfolding algebra_simps |
|
7167 apply (subst eq_commute) |
|
7168 apply (rule integral_combine) |
|
7169 using True using assms(2) goal1 |
|
7170 apply auto |
|
7171 done |
|
7172 have **: "norm (y - x) = content {y..x}" |
|
7173 apply (subst content_real) |
|
7174 using True |
|
7175 unfolding not_less |
|
7176 apply auto |
|
7177 done |
|
7178 have ***: "\<And>fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)" |
|
7179 unfolding scaleR_left.diff by auto |
|
7180 show ?thesis |
|
7181 apply (subst ***) |
|
7182 unfolding norm_minus_cancel ** |
|
7183 apply (rule has_integral_bound[where f="(\<lambda>u. f u - f x)"]) |
|
7184 unfolding * |
|
7185 unfolding o_def |
|
7186 defer |
|
7187 apply (rule has_integral_sub) |
|
7188 apply (subst minus_minus[symmetric]) |
|
7189 unfolding minus_minus |
|
7190 apply (rule integrable_integral) |
|
7191 apply (rule integrable_subinterval,rule integrable_continuous) |
|
7192 apply (rule assms)+ |
|
7193 proof - |
|
7194 show "{y..x} \<subseteq> {a..b}" |
|
7195 using goal1 assms(2) by auto |
|
7196 have *: "x - y = norm (y - x)" |
|
7197 using True by auto |
|
7198 show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {y..x}" |
|
7199 apply (subst *) |
|
7200 unfolding ** |
|
7201 apply auto |
|
7202 done |
|
7203 show "\<forall>xa\<in>{y..x}. norm (f xa - f x) \<le> e" |
|
7204 apply safe |
|
7205 apply (rule less_imp_le) |
|
7206 apply (rule d(2)[unfolded dist_norm]) |
|
7207 using assms(2) |
|
7208 using goal1 |
|
7209 apply auto |
|
7210 done |
|
7211 qed (insert e, auto) |
|
7212 qed |
|
7213 qed |
|
7214 qed |
|
7215 |
|
7216 lemma antiderivative_continuous: |
|
7217 fixes q b :: real |
|
7218 assumes "continuous_on {a..b} f" |
|
7219 obtains g where "\<forall>x\<in> {a..b}. (g has_vector_derivative (f x::_::banach)) (at x within {a..b})" |
|
7220 apply (rule that) |
|
7221 apply rule |
|
7222 using integral_has_vector_derivative[OF assms] |
|
7223 apply auto |
|
7224 done |
|
7225 |
6704 |
7226 |
6705 subsection {* Combined fundamental theorem of calculus. *} |
7227 subsection {* Combined fundamental theorem of calculus. *} |
6706 |
7228 |
6707 lemma antiderivative_integral_continuous: fixes f::"real \<Rightarrow> 'a::banach" assumes "continuous_on {a..b} f" |
7229 lemma antiderivative_integral_continuous: |
|
7230 fixes f :: "real \<Rightarrow> 'a::banach" |
|
7231 assumes "continuous_on {a..b} f" |
6708 obtains g where "\<forall>u\<in>{a..b}. \<forall>v \<in> {a..b}. u \<le> v \<longrightarrow> (f has_integral (g v - g u)) {u..v}" |
7232 obtains g where "\<forall>u\<in>{a..b}. \<forall>v \<in> {a..b}. u \<le> v \<longrightarrow> (f has_integral (g v - g u)) {u..v}" |
6709 proof- from antiderivative_continuous[OF assms] guess g . note g=this |
7233 proof - |
6710 show ?thesis apply(rule that[of g]) |
7234 from antiderivative_continuous[OF assms] guess g . note g=this |
6711 proof safe case goal1 have "\<forall>x\<in>{u..v}. (g has_vector_derivative f x) (at x within {u..v})" |
7235 show ?thesis |
6712 apply(rule,rule has_vector_derivative_within_subset) apply(rule g[rule_format]) using goal1(1-2) by auto |
7236 apply (rule that[of g]) |
6713 thus ?case using fundamental_theorem_of_calculus[OF goal1(3),of "g" "f"] by auto qed qed |
7237 proof safe |
|
7238 case goal1 |
|
7239 have "\<forall>x\<in>{u..v}. (g has_vector_derivative f x) (at x within {u..v})" |
|
7240 apply rule |
|
7241 apply (rule has_vector_derivative_within_subset) |
|
7242 apply (rule g[rule_format]) |
|
7243 using goal1(1-2) |
|
7244 apply auto |
|
7245 done |
|
7246 then show ?case |
|
7247 using fundamental_theorem_of_calculus[OF goal1(3),of "g" "f"] by auto |
|
7248 qed |
|
7249 qed |
|
7250 |
6714 |
7251 |
6715 subsection {* General "twiddling" for interval-to-interval function image. *} |
7252 subsection {* General "twiddling" for interval-to-interval function image. *} |
6716 |
7253 |
6717 lemma has_integral_twiddle: |
7254 lemma has_integral_twiddle: |
6718 assumes "0 < r" "\<forall>x. h(g x) = x" "\<forall>x. g(h x) = x" "\<forall>x. continuous (at x) g" |
7255 assumes "0 < r" |
6719 "\<forall>u v. \<exists>w z. g ` {u..v} = {w..z}" |
7256 and "\<forall>x. h(g x) = x" |
6720 "\<forall>u v. \<exists>w z. h ` {u..v} = {w..z}" |
7257 and "\<forall>x. g(h x) = x" |
6721 "\<forall>u v. content(g ` {u..v}) = r * content {u..v}" |
7258 and "\<forall>x. continuous (at x) g" |
6722 "(f has_integral i) {a..b}" |
7259 and "\<forall>u v. \<exists>w z. g ` {u..v} = {w..z}" |
|
7260 and "\<forall>u v. \<exists>w z. h ` {u..v} = {w..z}" |
|
7261 and "\<forall>u v. content(g ` {u..v}) = r * content {u..v}" |
|
7262 and "(f has_integral i) {a..b}" |
6723 shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` {a..b})" |
7263 shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` {a..b})" |
6724 proof- { presume *:"{a..b} \<noteq> {} \<Longrightarrow> ?thesis" |
7264 proof - |
6725 show ?thesis apply cases defer apply(rule *,assumption) |
7265 { |
6726 proof- case goal1 thus ?thesis unfolding goal1 assms(8)[unfolded goal1 has_integral_empty_eq] by auto qed } |
7266 presume *: "{a..b} \<noteq> {} \<Longrightarrow> ?thesis" |
6727 assume "{a..b} \<noteq> {}" from assms(6)[rule_format,of a b] guess w z apply-by(erule exE)+ note wz=this |
7267 show ?thesis |
6728 have inj:"inj g" "inj h" unfolding inj_on_def apply safe apply(rule_tac[!] ccontr) |
7268 apply cases |
6729 using assms(2) apply(erule_tac x=x in allE) using assms(2) apply(erule_tac x=y in allE) defer |
7269 defer |
6730 using assms(3) apply(erule_tac x=x in allE) using assms(3) apply(erule_tac x=y in allE) by auto |
7270 apply (rule *) |
6731 show ?thesis unfolding has_integral_def has_integral_compact_interval_def apply(subst if_P) apply(rule,rule,rule wz) |
7271 apply assumption |
6732 proof safe fix e::real assume e:"e>0" hence "e * r > 0" using assms(1) by(rule mult_pos_pos) |
7272 proof - |
6733 from assms(8)[unfolded has_integral,rule_format,OF this] guess d apply-by(erule exE conjE)+ note d=this[rule_format] |
7273 case goal1 |
6734 def d' \<equiv> "\<lambda>x. {y. g y \<in> d (g x)}" have d':"\<And>x. d' x = {y. g y \<in> (d (g x))}" unfolding d'_def .. |
7274 then show ?thesis |
|
7275 unfolding goal1 assms(8)[unfolded goal1 has_integral_empty_eq] by auto qed |
|
7276 } |
|
7277 assume "{a..b} \<noteq> {}" |
|
7278 from assms(6)[rule_format,of a b] guess w z by (elim exE) note wz=this |
|
7279 have inj: "inj g" "inj h" |
|
7280 unfolding inj_on_def |
|
7281 apply safe |
|
7282 apply(rule_tac[!] ccontr) |
|
7283 using assms(2) |
|
7284 apply(erule_tac x=x in allE) |
|
7285 using assms(2) |
|
7286 apply(erule_tac x=y in allE) |
|
7287 defer |
|
7288 using assms(3) |
|
7289 apply (erule_tac x=x in allE) |
|
7290 using assms(3) |
|
7291 apply(erule_tac x=y in allE) |
|
7292 apply auto |
|
7293 done |
|
7294 show ?thesis |
|
7295 unfolding has_integral_def has_integral_compact_interval_def |
|
7296 apply (subst if_P) |
|
7297 apply rule |
|
7298 apply rule |
|
7299 apply (rule wz) |
|
7300 proof safe |
|
7301 fix e :: real |
|
7302 assume e: "e > 0" |
|
7303 then have "e * r > 0" |
|
7304 using assms(1) by (rule mult_pos_pos) |
|
7305 from assms(8)[unfolded has_integral,rule_format,OF this] guess d by (elim exE conjE) note d=this[rule_format] |
|
7306 def d' \<equiv> "\<lambda>x. {y. g y \<in> d (g x)}" |
|
7307 have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}" |
|
7308 unfolding d'_def .. |
6735 show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` {a..b} \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)" |
7309 show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` {a..b} \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)" |
6736 proof(rule_tac x=d' in exI,safe) show "gauge d'" using d(1) unfolding gauge_def d' using continuous_open_preimage_univ[OF assms(4)] by auto |
7310 proof (rule_tac x=d' in exI, safe) |
6737 fix p assume as:"p tagged_division_of h ` {a..b}" "d' fine p" note p = tagged_division_ofD[OF as(1)] |
7311 show "gauge d'" |
6738 have "(\<lambda>(x, k). (g x, g ` k)) ` p tagged_division_of {a..b} \<and> d fine (\<lambda>(x, k). (g x, g ` k)) ` p" unfolding tagged_division_of |
7312 using d(1) |
6739 proof safe show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)" using as by auto |
7313 unfolding gauge_def d' |
6740 show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p" using as(2) unfolding fine_def d' by auto |
7314 using continuous_open_preimage_univ[OF assms(4)] |
6741 fix x k assume xk[intro]:"(x,k) \<in> p" show "g x \<in> g ` k" using p(2)[OF xk] by auto |
7315 by auto |
6742 show "\<exists>u v. g ` k = {u..v}" using p(4)[OF xk] using assms(5-6) by auto |
7316 fix p |
6743 { fix y assume "y \<in> k" thus "g y \<in> {a..b}" "g y \<in> {a..b}" using p(3)[OF xk,unfolded subset_eq,rule_format,of "h (g y)"] |
7317 assume as: "p tagged_division_of h ` {a..b}" "d' fine p" |
6744 using assms(2)[rule_format,of y] unfolding inj_image_mem_iff[OF inj(2)] by auto } |
7318 note p = tagged_division_ofD[OF as(1)] |
6745 fix x' k' assume xk':"(x',k') \<in> p" fix z assume "z \<in> interior (g ` k)" "z \<in> interior (g ` k')" |
7319 have "(\<lambda>(x, k). (g x, g ` k)) ` p tagged_division_of {a..b} \<and> d fine (\<lambda>(x, k). (g x, g ` k)) ` p" |
6746 hence *:"interior (g ` k) \<inter> interior (g ` k') \<noteq> {}" by auto |
7320 unfolding tagged_division_of |
6747 have same:"(x, k) = (x', k')" apply-apply(rule ccontr,drule p(5)[OF xk xk']) |
7321 proof safe |
6748 proof- assume as:"interior k \<inter> interior k' = {}" from nonempty_witness[OF *] guess z . |
7322 show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)" |
6749 hence "z \<in> g ` (interior k \<inter> interior k')" using interior_image_subset[OF assms(4) inj(1)] |
7323 using as by auto |
6750 unfolding image_Int[OF inj(1)] by auto thus False using as by blast |
7324 show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p" |
6751 qed thus "g x = g x'" by auto |
7325 using as(2) unfolding fine_def d' by auto |
6752 { fix z assume "z \<in> k" thus "g z \<in> g ` k'" using same by auto } |
7326 fix x k |
6753 { fix z assume "z \<in> k'" thus "g z \<in> g ` k" using same by auto } |
7327 assume xk[intro]: "(x, k) \<in> p" |
6754 next fix x assume "x \<in> {a..b}" hence "h x \<in> \<Union>{k. \<exists>x. (x, k) \<in> p}" using p(6) by auto |
7328 show "g x \<in> g ` k" |
6755 then guess X unfolding Union_iff .. note X=this from this(1) guess y unfolding mem_Collect_eq .. |
7329 using p(2)[OF xk] by auto |
6756 thus "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}" apply- |
7330 show "\<exists>u v. g ` k = {u..v}" |
6757 apply(rule_tac X="g ` X" in UnionI) defer apply(rule_tac x="h x" in image_eqI) |
7331 using p(4)[OF xk] using assms(5-6) by auto |
6758 using X(2) assms(3)[rule_format,of x] by auto |
7332 { |
6759 qed note ** = d(2)[OF this] have *:"inj_on (\<lambda>(x, k). (g x, g ` k)) p" using inj(1) unfolding inj_on_def by fastforce |
7333 fix y |
6760 have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding algebra_simps add_left_cancel |
7334 assume "y \<in> k" |
6761 unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv |
7335 then show "g y \<in> {a..b}" "g y \<in> {a..b}" |
6762 apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto |
7336 using p(3)[OF xk,unfolded subset_eq,rule_format,of "h (g y)"] |
6763 also have "... = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR_diff_right scaleR_scaleR |
7337 using assms(2)[rule_format,of y] |
6764 using assms(1) by auto finally have *:"?l = ?r" . |
7338 unfolding inj_image_mem_iff[OF inj(2)] |
6765 show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" using ** unfolding * unfolding norm_scaleR |
7339 by auto |
6766 using assms(1) by(auto simp add:field_simps) qed qed qed |
7340 } |
|
7341 fix x' k' |
|
7342 assume xk': "(x', k') \<in> p" |
|
7343 fix z |
|
7344 assume "z \<in> interior (g ` k)" and "z \<in> interior (g ` k')" |
|
7345 then have *: "interior (g ` k) \<inter> interior (g ` k') \<noteq> {}" |
|
7346 by auto |
|
7347 have same: "(x, k) = (x', k')" |
|
7348 apply - |
|
7349 apply (rule ccontr,drule p(5)[OF xk xk']) |
|
7350 proof - |
|
7351 assume as: "interior k \<inter> interior k' = {}" |
|
7352 from nonempty_witness[OF *] guess z . |
|
7353 then have "z \<in> g ` (interior k \<inter> interior k')" |
|
7354 using interior_image_subset[OF assms(4) inj(1)] |
|
7355 unfolding image_Int[OF inj(1)] |
|
7356 by auto |
|
7357 then show False |
|
7358 using as by blast |
|
7359 qed |
|
7360 then show "g x = g x'" |
|
7361 by auto |
|
7362 { |
|
7363 fix z |
|
7364 assume "z \<in> k" |
|
7365 then show "g z \<in> g ` k'" |
|
7366 using same by auto |
|
7367 } |
|
7368 { |
|
7369 fix z |
|
7370 assume "z \<in> k'" |
|
7371 then show "g z \<in> g ` k" |
|
7372 using same by auto |
|
7373 } |
|
7374 next |
|
7375 fix x |
|
7376 assume "x \<in> {a..b}" |
|
7377 then have "h x \<in> \<Union>{k. \<exists>x. (x, k) \<in> p}" |
|
7378 using p(6) by auto |
|
7379 then guess X unfolding Union_iff .. note X=this |
|
7380 from this(1) guess y unfolding mem_Collect_eq .. |
|
7381 then show "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}" |
|
7382 apply - |
|
7383 apply (rule_tac X="g ` X" in UnionI) |
|
7384 defer |
|
7385 apply (rule_tac x="h x" in image_eqI) |
|
7386 using X(2) assms(3)[rule_format,of x] |
|
7387 apply auto |
|
7388 done |
|
7389 qed |
|
7390 note ** = d(2)[OF this] |
|
7391 have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p" |
|
7392 using inj(1) unfolding inj_on_def by fastforce |
|
7393 have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") |
|
7394 unfolding algebra_simps add_left_cancel |
|
7395 unfolding setsum_reindex[OF *] |
|
7396 apply (subst scaleR_right.setsum) |
|
7397 defer |
|
7398 apply (rule setsum_cong2) |
|
7399 unfolding o_def split_paired_all split_conv |
|
7400 apply (drule p(4)) |
|
7401 apply safe |
|
7402 unfolding assms(7)[rule_format] |
|
7403 using p |
|
7404 apply auto |
|
7405 done |
|
7406 also have "\<dots> = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") |
|
7407 unfolding scaleR_diff_right scaleR_scaleR |
|
7408 using assms(1) |
|
7409 by auto |
|
7410 finally have *: "?l = ?r" . |
|
7411 show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" |
|
7412 using ** |
|
7413 unfolding * |
|
7414 unfolding norm_scaleR |
|
7415 using assms(1) |
|
7416 by (auto simp add:field_simps) |
|
7417 qed |
|
7418 qed |
|
7419 qed |
|
7420 |
6767 |
7421 |
6768 subsection {* Special case of a basic affine transformation. *} |
7422 subsection {* Special case of a basic affine transformation. *} |
6769 |
7423 |
6770 lemma interval_image_affinity_interval: shows "\<exists>u v. (\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space) + c) ` {a..b} = {u..v}" |
7424 lemma interval_image_affinity_interval: |
6771 unfolding image_affinity_interval by auto |
7425 "\<exists>u v. (\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space) + c) ` {a..b} = {u..v}" |
6772 |
7426 unfolding image_affinity_interval |
6773 lemma setprod_cong2: assumes "\<And>x. x \<in> A \<Longrightarrow> f x = g x" shows "setprod f A = setprod g A" |
7427 by auto |
6774 apply(rule setprod_cong) using assms by auto |
7428 |
|
7429 lemma setprod_cong2: |
|
7430 assumes "\<And>x. x \<in> A \<Longrightarrow> f x = g x" |
|
7431 shows "setprod f A = setprod g A" |
|
7432 apply (rule setprod_cong) |
|
7433 using assms |
|
7434 apply auto |
|
7435 done |
6775 |
7436 |
6776 lemma content_image_affinity_interval: |
7437 lemma content_image_affinity_interval: |
6777 "content((\<lambda>x::'a::ordered_euclidean_space. m *\<^sub>R x + c) ` {a..b}) = (abs m) ^ DIM('a) * content {a..b}" (is "?l = ?r") |
7438 "content((\<lambda>x::'a::ordered_euclidean_space. m *\<^sub>R x + c) ` {a..b}) = |
6778 proof- { presume *:"{a..b}\<noteq>{} \<Longrightarrow> ?thesis" show ?thesis apply(cases,rule *,assumption) |
7439 abs m ^ DIM('a) * content {a..b}" (is "?l = ?r") |
6779 unfolding not_not using content_empty by auto } |
7440 proof - |
6780 assume as: "{a..b}\<noteq>{}" |
7441 { |
|
7442 presume *: "{a..b} \<noteq> {} \<Longrightarrow> ?thesis" |
|
7443 show ?thesis |
|
7444 apply cases |
|
7445 apply (rule *) |
|
7446 apply assumption |
|
7447 unfolding not_not |
|
7448 using content_empty |
|
7449 apply auto |
|
7450 done |
|
7451 } |
|
7452 assume as: "{a..b} \<noteq> {}" |
6781 show ?thesis |
7453 show ?thesis |
6782 proof (cases "m \<ge> 0") |
7454 proof (cases "m \<ge> 0") |
6783 case True |
7455 case True |
6784 with as have "{m *\<^sub>R a + c..m *\<^sub>R b + c} \<noteq> {}" |
7456 with as have "{m *\<^sub>R a + c..m *\<^sub>R b + c} \<noteq> {}" |
6785 unfolding interval_ne_empty |
7457 unfolding interval_ne_empty |