3587 apply (subst(asm)(2) norm_minus_cancel[symmetric]) |
3587 apply (subst(asm)(2) norm_minus_cancel[symmetric]) |
3588 apply (drule norm_triangle_le) |
3588 apply (drule norm_triangle_le) |
3589 apply (auto simp add: algebra_simps) |
3589 apply (auto simp add: algebra_simps) |
3590 done |
3590 done |
3591 |
3591 |
3592 lemma fundamental_theorem_of_calculus_interior: |
3592 theorem fundamental_theorem_of_calculus_interior: |
3593 fixes f :: "real \<Rightarrow> 'a::real_normed_vector" |
3593 fixes f :: "real \<Rightarrow> 'a::real_normed_vector" |
3594 assumes "a \<le> b" |
3594 assumes "a \<le> b" |
3595 and contf: "continuous_on {a .. b} f" |
3595 and contf: "continuous_on {a .. b} f" |
3596 and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)" |
3596 and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)" |
3597 shows "(f' has_integral (f b - f a)) {a .. b}" |
3597 shows "(f' has_integral (f b - f a)) {a .. b}" |
3598 proof - |
3598 proof (cases "a = b") |
3599 { |
3599 case True |
3600 presume *: "a < b \<Longrightarrow> ?thesis" |
3600 then have *: "cbox a b = {b}" "f b - f a = 0" |
3601 show ?thesis |
3601 by (auto simp add: order_antisym) |
3602 proof (cases "a < b") |
3602 with True show ?thesis by auto |
3603 case True |
3603 next |
3604 then show ?thesis by (rule *) |
3604 case False |
3605 next |
3605 with \<open>a \<le> b\<close> have ab: "a < b" by arith |
3606 case False |
3606 let ?P = "\<lambda>e. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a .. b} \<longrightarrow> d fine p \<longrightarrow> |
3607 then have "a = b" |
|
3608 using assms(1) by auto |
|
3609 then have *: "cbox a b = {b}" "f b - f a = 0" |
|
3610 by (auto simp add: order_antisym) |
|
3611 show ?thesis |
|
3612 unfolding *(2) |
|
3613 unfolding content_eq_0 |
|
3614 using * \<open>a = b\<close> |
|
3615 by (auto simp: ex_in_conv) |
|
3616 qed |
|
3617 } |
|
3618 assume ab: "a < b" |
|
3619 let ?P = "\<lambda>e. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow> |
|
3620 norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a .. b})" |
3607 norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a .. b})" |
3621 { presume "\<And>e. e > 0 \<Longrightarrow> ?P e" then show ?thesis unfolding has_integral_factor_content_real by auto } |
3608 { presume "\<And>e. e > 0 \<Longrightarrow> ?P e" then show ?thesis unfolding has_integral_factor_content_real by force } |
3622 fix e :: real |
3609 fix e :: real |
3623 assume e: "e > 0" |
3610 assume e: "e > 0" |
|
3611 then have eba8: "(e * (b - a)) / 8 > 0" |
|
3612 using ab by (auto simp add: field_simps) |
3624 note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt] |
3613 note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt] |
3625 have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)" |
3614 have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)" |
3626 using derf_exp by simp |
3615 using derf_exp by simp |
3627 have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)" |
3616 have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)" |
3628 (is "\<forall>x \<in> box a b. ?Q x") |
3617 (is "\<forall>x \<in> box a b. ?Q x") |
3637 "\<And>x y. \<lbrakk>x \<in> box a b; norm (y - x) < d x\<rbrakk> |
3626 "\<And>x y. \<lbrakk>x \<in> box a b; norm (y - x) < d x\<rbrakk> |
3638 \<Longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e / 2 * norm (y - x)" |
3627 \<Longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e / 2 * norm (y - x)" |
3639 by metis |
3628 by metis |
3640 have "bounded (f ` cbox a b)" |
3629 have "bounded (f ` cbox a b)" |
3641 apply (rule compact_imp_bounded compact_continuous_image)+ |
3630 apply (rule compact_imp_bounded compact_continuous_image)+ |
3642 using compact_cbox assms |
3631 using compact_cbox assms by auto |
3643 apply auto |
3632 then obtain B |
3644 done |
|
3645 from this[unfolded bounded_pos] obtain B |
|
3646 where "0 < B" and B: "\<And>x. x \<in> f ` cbox a b \<Longrightarrow> norm x \<le> B" |
3633 where "0 < B" and B: "\<And>x. x \<in> f ` cbox a b \<Longrightarrow> norm x \<le> B" |
3647 by metis |
3634 unfolding bounded_pos by metis |
3648 have "\<exists>da. 0 < da \<and> (\<forall>c. a \<le> c \<and> {a .. c} \<subseteq> {a .. b} \<and> {a .. c} \<subseteq> ball a da \<longrightarrow> |
3635 obtain da where "0 < da" |
3649 norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b - a)) / 4)" |
3636 and da: "\<And>c. \<lbrakk>a \<le> c; {a .. c} \<subseteq> {a .. b}; {a .. c} \<subseteq> ball a da\<rbrakk> |
|
3637 \<Longrightarrow> norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b - a)) / 4" |
3650 proof - |
3638 proof - |
3651 have "a \<in> {a .. b}" |
3639 have "continuous (at a within {a..b}) f" |
3652 using ab by auto |
3640 using contf continuous_on_eq_continuous_within by force |
3653 note assms(2)[unfolded continuous_on_eq_continuous_within,rule_format,OF this] |
3641 with eba8 obtain k where "0 < k" |
3654 note * = this[unfolded continuous_within Lim_within,rule_format] |
3642 and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm (x-a); norm (x-a) < k\<rbrakk> |
3655 have "(e * (b - a)) / 8 > 0" |
3643 \<Longrightarrow> norm (f x - f a) < e * (b - a) / 8" |
3656 using e ab by (auto simp add: field_simps) |
3644 unfolding continuous_within Lim_within dist_norm by metis |
3657 from *[OF this] guess k .. note k = conjunctD2[OF this,rule_format] |
3645 obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b - a) / 8" |
3658 have "\<exists>l. 0 < l \<and> norm(l *\<^sub>R f' a) \<le> (e * (b - a)) / 8" |
|
3659 proof (cases "f' a = 0") |
3646 proof (cases "f' a = 0") |
3660 case True |
3647 case True |
3661 thus ?thesis using ab e by auto |
3648 thus ?thesis using ab e that by auto |
3662 next |
3649 next |
3663 case False |
3650 case False |
3664 then show ?thesis |
3651 then show ?thesis |
3665 apply (rule_tac x="(e * (b - a)) / 8 / norm (f' a)" in exI) |
3652 apply (rule_tac l="(e * (b - a)) / 8 / norm (f' a)" in that) |
3666 using ab e |
3653 using ab e apply (auto simp add: field_simps) |
3667 apply (auto simp add: field_simps) |
|
3668 done |
3654 done |
3669 qed |
3655 qed |
3670 then obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b - a) / 8" by metis |
3656 have "norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4" |
3671 show ?thesis |
3657 if "a \<le> c" "{a .. c} \<subseteq> {a .. b}" and bmin: "{a .. c} \<subseteq> ball a (min k l)" for c |
3672 apply (rule_tac x="min k l" in exI) |
|
3673 apply safe |
|
3674 unfolding min_less_iff_conj |
|
3675 apply rule |
|
3676 apply (rule l k)+ |
|
3677 proof - |
3658 proof - |
3678 fix c |
3659 have minkl: "\<bar>a - x\<bar> < min k l" if "x \<in> {a..c}" for x |
3679 assume as: "a \<le> c" "{a .. c} \<subseteq> {a .. b}" "{a .. c} \<subseteq> ball a (min k l)" |
3660 using bmin dist_real_def that by auto |
3680 note as' = this[unfolded subset_eq Ball_def mem_ball dist_real_def mem_box] |
3661 then have lel: "\<bar>c - a\<bar> \<le> \<bar>l\<bar>" |
|
3662 using that by force |
3681 have "norm ((c - a) *\<^sub>R f' a - (f c - f a)) \<le> norm ((c - a) *\<^sub>R f' a) + norm (f c - f a)" |
3663 have "norm ((c - a) *\<^sub>R f' a - (f c - f a)) \<le> norm ((c - a) *\<^sub>R f' a) + norm (f c - f a)" |
3682 by (rule norm_triangle_ineq4) |
3664 by (rule norm_triangle_ineq4) |
3683 also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8" |
3665 also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8" |
3684 proof (rule add_mono) |
3666 proof (rule add_mono) |
3685 have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)" |
3667 have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)" |
3686 unfolding norm_scaleR |
3668 by (auto intro: mult_right_mono [OF lel]) |
3687 apply (rule mult_right_mono) |
|
3688 using as' by auto |
|
3689 also have "... \<le> e * (b - a) / 8" |
3669 also have "... \<le> e * (b - a) / 8" |
3690 by (rule l) |
3670 by (rule l) |
3691 finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8" . |
3671 finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8" . |
3692 next |
3672 next |
3693 have "norm (f c - f a) < e * (b - a) / 8" |
3673 have "norm (f c - f a) < e * (b - a) / 8" |
3694 proof (cases "a = c") |
3674 proof (cases "a = c") |
3695 case True |
3675 case True then show ?thesis |
3696 then show ?thesis |
3676 using eba8 by auto |
3697 using \<open>0 < e * (b - a) / 8\<close> by auto |
|
3698 next |
3677 next |
3699 case False |
3678 case False show ?thesis |
3700 show ?thesis |
3679 by (rule k) (use minkl \<open>a \<le> c\<close> that False in auto) |
3701 apply (rule k(2)[unfolded dist_norm]) |
|
3702 using as' False |
|
3703 apply (auto simp add: field_simps) |
|
3704 done |
|
3705 qed |
3680 qed |
3706 then show "norm (f c - f a) \<le> e * (b - a) / 8" by simp |
3681 then show "norm (f c - f a) \<le> e * (b - a) / 8" by simp |
3707 qed |
3682 qed |
3708 finally show "norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4" |
3683 finally show "norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4" |
3709 unfolding content_real[OF as(1)] by auto |
3684 unfolding content_real[OF \<open>a \<le> c\<close>] by auto |
3710 qed |
3685 qed |
|
3686 then show ?thesis |
|
3687 by (rule_tac da="min k l" in that) (auto simp: l \<open>0 < k\<close>) |
3711 qed |
3688 qed |
3712 then guess da .. note da=conjunctD2[OF this,rule_format] |
3689 |
3713 |
3690 obtain db where "0 < db" |
3714 have "\<exists>db>0. \<forall>c\<le>b. {c .. b} \<subseteq> {a .. b} \<and> {c .. b} \<subseteq> ball b db \<longrightarrow> |
3691 and db: "\<And>c. \<lbrakk>c \<le> b; {c .. b} \<subseteq> {a .. b}; {c .. b} \<subseteq> ball b db\<rbrakk> |
3715 norm (content {c .. b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b - a)) / 4" |
3692 \<Longrightarrow> norm (content {c .. b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b - a)) / 4" |
3716 proof - |
3693 proof - |
3717 have "b \<in> {a .. b}" |
3694 have "continuous (at b within {a..b}) f" |
3718 using ab by auto |
3695 using contf continuous_on_eq_continuous_within by force |
3719 note assms(2)[unfolded continuous_on_eq_continuous_within,rule_format,OF this] |
3696 with eba8 obtain k |
3720 note * = this[unfolded continuous_within Lim_within,rule_format] have "(e * (b - a)) / 8 > 0" |
3697 where "0 < k" |
3721 using e ab by (auto simp add: field_simps) |
3698 and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm(x-b); norm(x-b) < k\<rbrakk> |
3722 from *[OF this] obtain k |
3699 \<Longrightarrow> norm (f b - f x) < e * (b - a) / 8" |
3723 where k: "0 < k" |
3700 unfolding continuous_within Lim_within dist_norm norm_minus_commute by metis |
3724 "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < dist x b \<and> dist x b < k\<rbrakk> |
|
3725 \<Longrightarrow> dist (f x) (f b) < e * (b - a) / 8" |
|
3726 by blast |
|
3727 obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8" |
3701 obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8" |
3728 proof (cases "f' b = 0") |
3702 proof (cases "f' b = 0") |
3729 case True |
3703 case True thus ?thesis |
3730 thus ?thesis using ab e that by auto |
3704 using ab e that by auto |
3731 next |
3705 next |
3732 case False |
3706 case False then show ?thesis |
3733 then show ?thesis |
|
3734 apply (rule_tac l="(e * (b - a)) / 8 / norm (f' b)" in that) |
3707 apply (rule_tac l="(e * (b - a)) / 8 / norm (f' b)" in that) |
3735 using ab e |
3708 using ab e by (auto simp add: field_simps) |
3736 apply (auto simp add: field_simps) |
|
3737 done |
|
3738 qed |
3709 qed |
3739 show ?thesis |
3710 have "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4" |
3740 apply (rule_tac x="min k l" in exI) |
3711 if "c \<le> b" "{c..b} \<subseteq> {a..b}" and bmin: "{c..b} \<subseteq> ball b (min k l)" for c |
3741 apply safe |
|
3742 unfolding min_less_iff_conj |
|
3743 apply rule |
|
3744 apply (rule l k)+ |
|
3745 proof - |
3712 proof - |
3746 fix c |
3713 have minkl: "\<bar>b - x\<bar> < min k l" if "x \<in> {c..b}" for x |
3747 assume as: "c \<le> b" "{c..b} \<subseteq> {a..b}" "{c..b} \<subseteq> ball b (min k l)" |
3714 using bmin dist_real_def that by auto |
3748 note as' = this[unfolded subset_eq Ball_def mem_ball dist_real_def mem_box] |
3715 then have lel: "\<bar>b - c\<bar> \<le> \<bar>l\<bar>" |
|
3716 using that by force |
3749 have "norm ((b - c) *\<^sub>R f' b - (f b - f c)) \<le> norm ((b - c) *\<^sub>R f' b) + norm (f b - f c)" |
3717 have "norm ((b - c) *\<^sub>R f' b - (f b - f c)) \<le> norm ((b - c) *\<^sub>R f' b) + norm (f b - f c)" |
3750 by (rule norm_triangle_ineq4) |
3718 by (rule norm_triangle_ineq4) |
3751 also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8" |
3719 also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8" |
3752 proof (rule add_mono) |
3720 proof (rule add_mono) |
3753 have "\<bar>c - b\<bar> \<le> \<bar>l\<bar>" |
3721 have "norm ((b - c) *\<^sub>R f' b) \<le> norm (l *\<^sub>R f' b)" |
3754 using as' by auto |
3722 by (auto intro: mult_right_mono [OF lel]) |
3755 then show "norm ((b - c) *\<^sub>R f' b) \<le> e * (b - a) / 8" |
3723 also have "... \<le> e * (b - a) / 8" |
3756 apply - |
3724 by (rule l) |
3757 apply (rule order_trans[OF _ l(2)]) |
3725 finally show "norm ((b - c) *\<^sub>R f' b) \<le> e * (b - a) / 8" . |
3758 unfolding norm_scaleR |
|
3759 apply (rule mult_right_mono) |
|
3760 apply auto |
|
3761 done |
|
3762 next |
3726 next |
3763 show "norm (f b - f c) \<le> e * (b - a) / 8" |
3727 have "norm (f b - f c) < e * (b - a) / 8" |
3764 apply (rule less_imp_le) |
3728 proof (cases "b = c") |
3765 apply (cases "b = c") |
3729 case True |
3766 defer |
3730 then show ?thesis |
3767 apply (subst norm_minus_commute) |
3731 using eba8 by auto |
3768 apply (rule k(2)[unfolded dist_norm]) |
3732 next |
3769 using as' e ab |
3733 case False show ?thesis |
3770 apply (auto simp add: field_simps) |
3734 by (rule k) (use minkl \<open>c \<le> b\<close> that False in auto) |
3771 done |
3735 qed |
|
3736 then show "norm (f b - f c) \<le> e * (b - a) / 8" by simp |
3772 qed |
3737 qed |
3773 finally show "norm (content {c .. b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4" |
3738 finally show "norm (content {c .. b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4" |
3774 unfolding content_real[OF as(1)] by auto |
3739 unfolding content_real[OF \<open>c \<le> b\<close>] by auto |
3775 qed |
3740 qed |
|
3741 then show ?thesis |
|
3742 by (rule_tac db="min k l" in that) (auto simp: l \<open>0 < k\<close>) |
3776 qed |
3743 qed |
3777 then guess db .. note db=conjunctD2[OF this,rule_format] |
|
3778 |
3744 |
3779 let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))" |
3745 let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))" |
3780 show "?P e" |
3746 show "?P e" |
3781 apply (rule_tac x="?d" in exI) |
3747 proof (intro exI conjI allI impI) |
3782 proof (safe, goal_cases) |
3748 show "gauge ?d" |
3783 case 1 |
3749 using ab \<open>db > 0\<close> \<open>da > 0\<close> d(1) by (auto intro: gauge_ball_dependent) |
3784 show ?case |
|
3785 apply (rule gauge_ball_dependent) |
|
3786 using ab db(1) da(1) d(1) |
|
3787 apply auto |
|
3788 done |
|
3789 next |
3750 next |
3790 case as: (2 p) |
3751 fix p |
|
3752 assume as: "p tagged_division_of {a..b}" "?d fine p" |
3791 let ?A = "{t. fst t \<in> {a, b}}" |
3753 let ?A = "{t. fst t \<in> {a, b}}" |
3792 note p = tagged_division_ofD[OF as(1)] |
3754 note p = tagged_division_ofD[OF as(1)] |
3793 have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}" |
3755 have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}" |
3794 using as by auto |
3756 using as by auto |
3795 note * = additive_tagged_division_1[OF assms(1) as(1), symmetric] |
3757 note * = additive_tagged_division_1[OF assms(1) as(1), symmetric] |
3796 have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2" |
3758 have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2" |
3797 by arith |
3759 by arith |
3798 show ?case |
3760 show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}" |
3799 unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] sum_subtractf[symmetric] split_minus |
3761 unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] sum_subtractf[symmetric] split_minus |
3800 unfolding sum_distrib_left |
3762 unfolding sum_distrib_left |
3801 apply (subst(2) pA) |
3763 apply (subst(2) pA) |
3802 apply (subst pA) |
3764 apply (subst pA) |
3803 unfolding sum.union_disjoint[OF pA(2-)] |
3765 unfolding sum.union_disjoint[OF pA(2-)] |