New results for Green's theorem
authorpaulson <lp15@cam.ac.uk>
Fri Sep 29 14:12:14 2017 +0100 (19 months ago)
changeset 66708015a95f15040
parent 66690 6953b1a29e19
child 66709 b034d2ae541c
New results for Green's theorem
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
     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