author paulson Fri Sep 29 14:12:14 2017 +0100 (19 months ago) changeset 66708 015a95f15040 parent 66690 6953b1a29e19 child 66709 b034d2ae541c
New results for Green's theorem
```     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Sep 25 15:49:27 2017 +0100
1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Sep 29 14:12:14 2017 +0100
1.3 @@ -3749,12 +3749,14 @@
1.4      by meson
1.5    have exy: "\<exists>y. ((\<lambda>x. inverse (\<gamma> x - z) * ?D\<gamma> x) has_integral y) {a..b}"
1.6      unfolding integrable_on_def [symmetric]
1.7 -    apply (rule contour_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \<gamma>], of "-{z}"])
1.8 -    apply (rename_tac w)
1.9 -    apply (rule_tac x="norm(w - z)" in exI)
1.10 -    apply (simp_all add: inverse_eq_divide)
1.11 -    apply (metis has_field_derivative_at_within h)
1.12 -    done
1.13 +  proof (rule contour_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \<gamma>]])
1.14 +    show "\<exists>d h. 0 < d \<and>
1.15 +               (\<forall>y. cmod (y - w) < d \<longrightarrow> (h has_field_derivative inverse (y - z))(at y within - {z}))"
1.16 +          if "w \<in> - {z}" for w
1.17 +      apply (rule_tac x="norm(w - z)" in exI)
1.18 +      using that inverse_eq_divide has_field_derivative_at_within h
1.19 +      by (metis Compl_insert DiffD2 insertCI right_minus_eq zero_less_norm_iff)
1.20 +  qed simp
1.21    have vg_int: "(\<lambda>x. ?D\<gamma> x / (\<gamma> x - z)) integrable_on {a..b}"
1.22      unfolding box_real [symmetric] divide_inverse_commute
1.23      by (auto intro!: exy integrable_subinterval simp add: integrable_on_def ab)
1.24 @@ -3774,20 +3776,29 @@
1.25        assume x: "x \<notin> k" "a < x" "x < b"
1.26        then have "x \<in> interior ({a..b} - k)"
1.27          using open_subset_interior [OF o] by fastforce
1.28 -      then have con: "isCont (\<lambda>x. ?D\<gamma> x) x"
1.29 +      then have con: "isCont ?D\<gamma> x"
1.30          using g_C1_diff x by (auto simp: C1_differentiable_on_eq intro: continuous_on_interior)
1.31        then have con_vd: "continuous (at x within {a..b}) (\<lambda>x. ?D\<gamma> x)"
1.32          by (rule continuous_at_imp_continuous_within)
1.33        have gdx: "\<gamma> differentiable at x"
1.34          using x by (simp add: g_diff_at)
1.35 -      have "((\<lambda>c. exp (- integral {a..c} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0))
1.36 +      have "\<And>d. \<lbrakk>x \<notin> k; a < x; x < b;
1.37 +          (\<gamma> has_vector_derivative d) (at x); a \<le> t; t \<le> b\<rbrakk>
1.38 +         \<Longrightarrow> ((\<lambda>x. integral {a..x}
1.39 +                     (\<lambda>x. ?D\<gamma> x /
1.40 +                           (\<gamma> x - z))) has_vector_derivative
1.41 +              d / (\<gamma> x - z))
1.42 +              (at x within {a..b})"
1.43 +        apply (rule has_vector_derivative_eq_rhs)
1.44 +         apply (rule integral_has_vector_derivative_continuous_at [where S = "{}", simplified])
1.45 +        apply (rule con_vd continuous_intros cong vg_int | simp add: continuous_at_imp_continuous_within has_vector_derivative_continuous vector_derivative_at)+
1.46 +        done
1.47 +      then have "((\<lambda>c. exp (- integral {a..c} (\<lambda>x. ?D\<gamma> x / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0))
1.48            (at x within {a..b})"
1.49          using x gdx t
1.50          apply (clarsimp simp add: differentiable_iff_scaleR)
1.51          apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_within)
1.52          apply (simp_all add: has_vector_derivative_def [symmetric])
1.53 -        apply (rule has_vector_derivative_eq_rhs [OF integral_has_vector_derivative_continuous_at])
1.54 -        apply (rule con_vd continuous_intros cong vg_int | simp add: continuous_at_imp_continuous_within has_vector_derivative_continuous vector_derivative_at)+
1.55          done
1.56        } note * = this
1.57      have "exp (- (integral {a..t} (\<lambda>x. ?D\<gamma> x / (\<gamma> x - z)))) * (\<gamma> t - z) =\<gamma> a - z"
```
```     2.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Sep 25 15:49:27 2017 +0100
2.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 29 14:12:14 2017 +0100
2.3 @@ -10,10 +10,6 @@
2.4    Lebesgue_Measure Tagged_Division
2.5  begin
2.6
2.7 -(*FIXME DELETE*)
2.8 -lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
2.9 -(* try instead structured proofs below *)
2.10 -
2.11  lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
2.12    \<Longrightarrow> norm(y-x) \<le> e"
2.13    using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
2.14 @@ -1541,14 +1537,6 @@
2.15      using \<gamma> [OF p \<open>\<gamma> fine p\<close>] rsum_bound[OF p] assms by metis
2.16  qed
2.17
2.18 -corollary has_integral_bound_real:
2.19 -  fixes f :: "real \<Rightarrow> 'b::real_normed_vector"
2.20 -  assumes "0 \<le> B"
2.21 -      and "(f has_integral i) {a..b}"
2.22 -      and "\<forall>x\<in>{a..b}. norm (f x) \<le> B"
2.23 -    shows "norm i \<le> B * content {a..b}"
2.24 -  by (metis assms box_real(2) has_integral_bound)
2.25 -
2.26  corollary integrable_bound:
2.27    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
2.28    assumes "0 \<le> B"
2.29 @@ -2384,6 +2372,31 @@
2.30    shows "g integrable_on T"
2.31    using assms has_integral_spike_finite by blast
2.32
2.33 +lemma has_integral_bound_spike_finite:
2.34 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
2.35 +  assumes "0 \<le> B" "finite S"
2.36 +      and f: "(f has_integral i) (cbox a b)"
2.37 +      and leB: "\<And>x. x \<in> cbox a b - S \<Longrightarrow> norm (f x) \<le> B"
2.38 +    shows "norm i \<le> B * content (cbox a b)"
2.39 +proof -
2.40 +  define g where "g \<equiv> (\<lambda>x. if x \<in> S then 0 else f x)"
2.41 +  then have "\<And>x. x \<in> cbox a b - S \<Longrightarrow> norm (g x) \<le> B"
2.42 +    using leB by simp
2.43 +  moreover have "(g has_integral i) (cbox a b)"
2.44 +    using has_integral_spike_finite [OF \<open>finite S\<close> _ f]
2.45 +    by (simp add: g_def)
2.46 +  ultimately show ?thesis
2.47 +    by (simp add: \<open>0 \<le> B\<close> g_def has_integral_bound)
2.48 +qed
2.49 +
2.50 +corollary has_integral_bound_real:
2.51 +  fixes f :: "real \<Rightarrow> 'b::real_normed_vector"
2.52 +  assumes "0 \<le> B" "finite S"
2.53 +      and "(f has_integral i) {a..b}"
2.54 +      and "\<And>x. x \<in> {a..b} - S \<Longrightarrow> norm (f x) \<le> B"
2.55 +    shows "norm i \<le> B * content {a..b}"
2.56 +  by (metis assms box_real(2) has_integral_bound_spike_finite)
2.57 +
2.58
2.59  subsection \<open>In particular, the boundary of an interval is negligible.\<close>
2.60
2.61 @@ -3047,19 +3060,20 @@
2.62    unfolding integrable_on_def by blast
2.63
2.64  lemma integral_has_vector_derivative_continuous_at:
2.65 -  fixes f :: "real \<Rightarrow> 'a::banach"
2.66 -  assumes f: "f integrable_on {a..b}"
2.67 -      and x: "x \<in> {a..b}"
2.68 -      and fx: "continuous (at x within {a..b}) f"
2.69 -  shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
2.70 + fixes f :: "real \<Rightarrow> 'a::banach"
2.71 + assumes f: "f integrable_on {a..b}"
2.72 +     and x: "x \<in> {a..b} - S"
2.73 +     and "finite S"
2.74 +     and fx: "continuous (at x within ({a..b} - S)) f"
2.75 + shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within ({a..b} - S))"
2.76  proof -
2.77    let ?I = "\<lambda>a b. integral {a..b} f"
2.78    { fix e::real
2.79      assume "e > 0"
2.80 -    obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {a..b}; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
2.81 +    obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {a..b} - S; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
2.82        using \<open>e>0\<close> fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
2.83      have "norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
2.84 -           if y: "y \<in> {a..b}" and yx: "\<bar>y - x\<bar> < d" for y
2.85 +           if y: "y \<in> {a..b} - S" and yx: "\<bar>y - x\<bar> < d" for y
2.86      proof (cases "y < x")
2.87        case False
2.88        have "f integrable_on {a..y}"
2.89 @@ -3070,14 +3084,15 @@
2.90          apply (rule has_integral_diff)
2.91          using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
2.92          using has_integral_const_real [of "f x" x y] False
2.93 -        apply (simp add: )
2.94 +        apply simp
2.95          done
2.96 +      have "\<And>xa. y - x < d \<Longrightarrow> (\<And>x'. a \<le> x' \<and> x' \<le> b \<and> x' \<notin> S \<Longrightarrow> \<bar>x' - x\<bar> < d \<Longrightarrow> norm (f x' - f x) \<le> e) \<Longrightarrow> 0 < e \<Longrightarrow> xa \<notin> S \<Longrightarrow> a \<le> x \<Longrightarrow> x \<notin> S \<Longrightarrow> y \<le> b \<Longrightarrow> y \<notin> S \<Longrightarrow> x \<le> xa \<Longrightarrow> xa \<le> y \<Longrightarrow> norm (f xa - f x) \<le> e"
2.97 +        using assms by auto
2.98        show ?thesis
2.99          using False
2.100          apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
2.101 -        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
2.102 -        using yx False d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
2.103 -        done
2.104 +        apply (rule has_integral_bound_real [where f="(\<lambda>u. f u - f x)"])
2.105 +        using yx False d x y \<open>e>0\<close> assms by (auto simp: Idiff fux_int)
2.106      next
2.107        case True
2.108        have "f integrable_on {a..x}"
2.109 @@ -3088,33 +3103,31 @@
2.110          apply (rule has_integral_diff)
2.111          using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
2.112          using has_integral_const_real [of "f x" y x] True
2.113 -        apply (simp add: )
2.114 +        apply simp
2.115          done
2.116        have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
2.117          using True
2.118          apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
2.119          apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
2.120 -        using yx True d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
2.121 -        done
2.122 +        using yx True d x y \<open>e>0\<close> assms by (auto simp: Idiff fux_int)
2.123        then show ?thesis
2.124          by (simp add: algebra_simps norm_minus_commute)
2.125      qed
2.126 -    then have "\<exists>d>0. \<forall>y\<in>{a..b}. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
2.127 +    then have "\<exists>d>0. \<forall>y\<in>{a..b} - S. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
2.128        using \<open>d>0\<close> by blast
2.129    }
2.130    then show ?thesis
2.131      by (simp add: has_vector_derivative_def has_derivative_within_alt bounded_linear_scaleR_left)
2.132  qed
2.133
2.134 +
2.135  lemma integral_has_vector_derivative:
2.136    fixes f :: "real \<Rightarrow> 'a::banach"
2.137    assumes "continuous_on {a..b} f"
2.138      and "x \<in> {a..b}"
2.139    shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})"
2.140 -apply (rule integral_has_vector_derivative_continuous_at [OF integrable_continuous_real])
2.141 -using assms
2.142 -apply (auto simp: continuous_on_eq_continuous_within)
2.143 -done
2.144 +using assms integral_has_vector_derivative_continuous_at [OF integrable_continuous_real]
2.145 +  by (fastforce simp: continuous_on_eq_continuous_within)
2.146
2.147  lemma antiderivative_continuous:
2.148    fixes q b :: real
2.149 @@ -6432,7 +6445,6 @@
2.150
2.151  subsection \<open>Integration by substitution\<close>
2.152
2.153 -
2.154  lemma has_integral_substitution_general:
2.155    fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
2.156    assumes s: "finite s" and le: "a \<le> b"
2.157 @@ -6462,7 +6474,6 @@
2.158                    (at x)" if "x \<in> {a..b} - (s \<union> {a,b})" for x
2.159      using deriv[of x] that by (simp add: at_within_closed_interval o_def)
2.160
2.161 -
2.162    have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
2.163      using le cont_int s deriv cont_int
2.164      by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all
```