New material for Cauchy's integral theorem
authorpaulson <lp15@cam.ac.uk>
Mon Jul 27 16:52:57 2015 +0100 (2015-07-27)
changeset 608007d04351c795a
parent 60799 57dd0b45fc21
child 60803 e11f47dd0786
New material for Cauchy's integral theorem
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 27 16:35:12 2015 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 27 16:52:57 2015 +0100
     1.3 @@ -1387,7 +1387,7 @@
     1.4      by auto
     1.5  qed
     1.6  
     1.7 -lemma convex_ball:
     1.8 +lemma convex_ball [iff]:
     1.9    fixes x :: "'a::real_normed_vector"
    1.10    shows "convex (ball x e)"
    1.11  proof (auto simp add: convex_def)
    1.12 @@ -1404,7 +1404,7 @@
    1.13      using convex_bound_lt[OF yz uv] by auto
    1.14  qed
    1.15  
    1.16 -lemma convex_cball:
    1.17 +lemma convex_cball [iff]:
    1.18    fixes x :: "'a::real_normed_vector"
    1.19    shows "convex (cball x e)"
    1.20  proof -
    1.21 @@ -3239,6 +3239,9 @@
    1.22    shows "rel_interior S = S"
    1.23    by (metis assms interior_eq interior_subset_rel_interior rel_interior_subset set_eq_subset)
    1.24  
    1.25 +lemma interior_ball [simp]: "interior (ball x e) = ball x e"
    1.26 +  by (simp add: interior_open)
    1.27 +
    1.28  lemma interior_rel_interior_gen:
    1.29    fixes S :: "'n::euclidean_space set"
    1.30    shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})"
    1.31 @@ -3551,7 +3554,7 @@
    1.32        using mem_rel_interior[of "a+x" "((\<lambda>x. a + x) ` S)"] by auto
    1.33    }
    1.34    then show ?thesis by auto
    1.35 -qed
    1.36 +qed                   
    1.37  
    1.38  lemma rel_interior_translation:
    1.39    fixes a :: "'n::euclidean_space"
    1.40 @@ -9317,9 +9320,9 @@
    1.41      done
    1.42  qed
    1.43  
    1.44 +
    1.45  subsection \<open>Coplanarity, and collinearity in terms of affine hull\<close>
    1.46  
    1.47 -
    1.48  definition coplanar  where
    1.49     "coplanar s \<equiv> \<exists>u v w. s \<subseteq> affine hull {u,v,w}"
    1.50  
    1.51 @@ -9425,26 +9428,46 @@
    1.52      by auto (meson assms(1) coplanar_def)
    1.53  qed
    1.54  
    1.55 -(*?  Still not ported
    1.56 -lemma COPLANAR_TRANSLATION_EQ: "coplanar((\<lambda>x. a + x) ` s) \<longleftrightarrow> coplanar s"
    1.57 -  apply (simp add: coplanar_def)
    1.58 -  apply (simp add: Set.image_subset_iff_subset_vimage)
    1.59 -  apply (auto simp:)
    1.60 -  apply (rule_tac x="u-a" in exI)
    1.61 -  apply (rule_tac x="v-a" in exI)
    1.62 -  apply (rule_tac x="w-a" in exI)
    1.63 -  apply (auto simp:)
    1.64 -  apply (drule_tac c="x+a" in subsetD)
    1.65 -  apply (simp add: affine_alt)
    1.66 -
    1.67 -lemma COPLANAR_TRANSLATION:
    1.68 -  !a:real^N s. coplanar s ==> coplanar(IMAGE (\x. a + x) s)"
    1.69 -  REWRITE_TAC[COPLANAR_TRANSLATION_EQ]);;
    1.70 +lemma coplanar_translation_imp: "coplanar s \<Longrightarrow> coplanar ((\<lambda>x. a + x) ` s)"
    1.71 +  unfolding coplanar_def
    1.72 +  apply clarify
    1.73 +  apply (rule_tac x="u+a" in exI)
    1.74 +  apply (rule_tac x="v+a" in exI)
    1.75 +  apply (rule_tac x="w+a" in exI)
    1.76 +  using affine_hull_translation [of a "{u,v,w}" for u v w]
    1.77 +  apply (force simp: add.commute)
    1.78 +  done
    1.79 +
    1.80 +lemma coplanar_translation_eq: "coplanar((\<lambda>x. a + x) ` s) \<longleftrightarrow> coplanar s"
    1.81 +    by (metis (no_types) coplanar_translation_imp translation_galois)
    1.82  
    1.83  lemma coplanar_linear_image_eq:
    1.84    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    1.85    assumes "linear f" "inj f" shows "coplanar(f ` s) = coplanar s"
    1.86 -  MATCH_ACCEPT_TAC(LINEAR_INVARIANT_RULE COPLANAR_LINEAR_IMAGE));;
    1.87 +proof 
    1.88 +  assume "coplanar s"
    1.89 +  then show "coplanar (f ` s)"
    1.90 +    unfolding coplanar_def
    1.91 +    using affine_hull_linear_image [of f "{u,v,w}" for u v w]  assms
    1.92 +    by (meson coplanar_def coplanar_linear_image)
    1.93 +next
    1.94 +  obtain g where g: "linear g" "g \<circ> f = id"
    1.95 +    using linear_injective_left_inverse [OF assms]
    1.96 +    by blast
    1.97 +  assume "coplanar (f ` s)"
    1.98 +  then obtain u v w where "f ` s \<subseteq> affine hull {u, v, w}"
    1.99 +    by (auto simp: coplanar_def)
   1.100 +  then have "g ` f ` s \<subseteq> g ` (affine hull {u, v, w})"
   1.101 +    by blast
   1.102 +  then have "s \<subseteq> g ` (affine hull {u, v, w})"
   1.103 +    using g by (simp add: Fun.image_comp)
   1.104 +  then show "coplanar s"
   1.105 +    unfolding coplanar_def
   1.106 +    using affine_hull_linear_image [of g "{u,v,w}" for u v w]  `linear g` linear_conv_bounded_linear 
   1.107 +    by fastforce
   1.108 +qed
   1.109 +(*The HOL Light proof is simply
   1.110 +    MATCH_ACCEPT_TAC(LINEAR_INVARIANT_RULE COPLANAR_LINEAR_IMAGE));;
   1.111  *)
   1.112  
   1.113  lemma coplanar_subset: "\<lbrakk>coplanar t; s \<subseteq> t\<rbrakk> \<Longrightarrow> coplanar s"
     2.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Jul 27 16:35:12 2015 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Jul 27 16:52:57 2015 +0100
     2.3 @@ -2315,4 +2315,9 @@
     2.4  lemma vector_derivative_const_at [simp]: "vector_derivative (\<lambda>x. c) (at a) = 0"
     2.5    by (simp add: vector_derivative_at)
     2.6  
     2.7 +lemma vector_derivative_at_within_ivl:
     2.8 +  "(f has_vector_derivative f') (at x) \<Longrightarrow>
     2.9 +    a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
    2.10 +using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
    2.11 +
    2.12  end
     3.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jul 27 16:35:12 2015 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jul 27 16:52:57 2015 +0100
     3.3 @@ -6803,22 +6803,13 @@
     3.4  lemma has_integral_affinity:
     3.5    fixes a :: "'a::euclidean_space"
     3.6    assumes "(f has_integral i) (cbox a b)"
     3.7 -    and "m \<noteq> 0"
     3.8 +      and "m \<noteq> 0"
     3.9    shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral ((1 / (abs(m) ^ DIM('a))) *\<^sub>R i)) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` cbox a b)"
    3.10    apply (rule has_integral_twiddle)
    3.11 -  apply safe
    3.12 +  using assms
    3.13 +  apply (safe intro!: interval_image_affinity_interval content_image_affinity_cbox)
    3.14    apply (rule zero_less_power)
    3.15 -  unfolding euclidean_eq_iff[where 'a='a]
    3.16 -  unfolding scaleR_right_distrib inner_simps scaleR_scaleR
    3.17 -  defer
    3.18 -  apply (insert assms(2))
    3.19 -  apply (simp add: field_simps)
    3.20 -  apply (insert assms(2))
    3.21 -  apply (simp add: field_simps)
    3.22 -  apply (rule continuous_intros)+
    3.23 -  apply (rule interval_image_affinity_interval)+
    3.24 -  apply (rule content_image_affinity_cbox)
    3.25 -  using assms
    3.26 +  unfolding scaleR_right_distrib  
    3.27    apply auto
    3.28    done
    3.29  
    3.30 @@ -6833,6 +6824,7 @@
    3.31    apply auto
    3.32    done
    3.33  
    3.34 +lemmas has_integral_affinity01 = has_integral_affinity [of _ _ 0 "1::real", simplified]
    3.35  
    3.36  subsection \<open>Special case of stretching coordinate axes separately.\<close>
    3.37  
     4.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Jul 27 16:35:12 2015 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Jul 27 16:52:57 2015 +0100
     4.3 @@ -255,7 +255,7 @@
     4.4    done
     4.5  
     4.6  lemma linear_cmul: "linear f \<Longrightarrow> f (c *\<^sub>R x) = c *\<^sub>R f x"
     4.7 -  by (simp add: linear_iff)
     4.8 +  by (rule linear.scaleR)
     4.9  
    4.10  lemma linear_neg: "linear f \<Longrightarrow> f (- x) = - f x"
    4.11    using linear_cmul [where c="-1"] by simp
    4.12 @@ -2692,6 +2692,11 @@
    4.13    with h(1) show ?thesis by blast
    4.14  qed
    4.15  
    4.16 +lemma inj_linear_imp_inv_linear:
    4.17 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
    4.18 +  assumes "linear f" "inj f" shows "linear (inv f)"
    4.19 +using assms inj_iff left_inverse_linear by blast
    4.20 +
    4.21  
    4.22  subsection \<open>Infinity norm\<close>
    4.23  
     5.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Jul 27 16:35:12 2015 +0200
     5.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jul 27 16:52:57 2015 +0100
     5.3 @@ -228,6 +228,29 @@
     5.4  apply (erule (1) nonzero_inverse_scaleR_distrib)
     5.5  done
     5.6  
     5.7 +lemma real_vector_affinity_eq:
     5.8 +  fixes x :: "'a :: real_vector"
     5.9 +  assumes m0: "m \<noteq> 0"
    5.10 +  shows "m *\<^sub>R x + c = y \<longleftrightarrow> x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)"
    5.11 +proof
    5.12 +  assume h: "m *\<^sub>R x + c = y"
    5.13 +  hence "m *\<^sub>R x = y - c" by (simp add: field_simps)
    5.14 +  hence "inverse m *\<^sub>R (m *\<^sub>R x) = inverse m *\<^sub>R (y - c)" by simp
    5.15 +  then show "x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)"
    5.16 +    using m0
    5.17 +  by (simp add: real_vector.scale_right_diff_distrib)
    5.18 +next
    5.19 +  assume h: "x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)"
    5.20 +  show "m *\<^sub>R x + c = y" unfolding h
    5.21 +    using m0  by (simp add: real_vector.scale_right_diff_distrib)
    5.22 +qed
    5.23 +
    5.24 +lemma real_vector_eq_affinity:
    5.25 +  fixes x :: "'a :: real_vector"
    5.26 +  shows "m \<noteq> 0 ==> (y = m *\<^sub>R x + c \<longleftrightarrow> inverse m *\<^sub>R y - (inverse m *\<^sub>R c) = x)"
    5.27 +  using real_vector_affinity_eq[where m=m and x=x and y=y and c=c]
    5.28 +  by metis
    5.29 +
    5.30  
    5.31  subsection \<open>Embedding of the Reals into any @{text real_algebra_1}:
    5.32  @{term of_real}\<close>
    5.33 @@ -763,6 +786,18 @@
    5.34    finally show ?thesis .
    5.35  qed
    5.36  
    5.37 +lemma norm_diff_triangle_le:
    5.38 +  fixes x y z :: "'a::real_normed_vector"
    5.39 +  assumes "norm (x - y) \<le> e1"  "norm (y - z) \<le> e2"
    5.40 +    shows "norm (x - z) \<le> e1 + e2"
    5.41 +  using norm_diff_triangle_ineq [of x y y z] assms by simp
    5.42 +
    5.43 +lemma norm_diff_triangle_less:
    5.44 +  fixes x y z :: "'a::real_normed_vector"
    5.45 +  assumes "norm (x - y) < e1"  "norm (y - z) < e2"
    5.46 +    shows "norm (x - z) < e1 + e2"
    5.47 +  using norm_diff_triangle_ineq [of x y y z] assms by simp
    5.48 +
    5.49  lemma norm_triangle_mono:
    5.50    fixes a b :: "'a::real_normed_vector"
    5.51    shows "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> r + s"
    5.52 @@ -1123,6 +1158,11 @@
    5.53  
    5.54  end
    5.55  
    5.56 +lemma dist_of_real [simp]:
    5.57 +  fixes a :: "'a::real_normed_div_algebra"
    5.58 +  shows "dist (of_real x :: 'a) (of_real y) = dist x y"
    5.59 +by (metis dist_norm norm_of_real of_real_diff real_norm_def)
    5.60 +
    5.61  declare [[code abort: "open :: real set \<Rightarrow> bool"]]
    5.62  
    5.63  instance real :: linorder_topology
    5.64 @@ -1249,6 +1289,10 @@
    5.65  locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
    5.66    assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
    5.67  
    5.68 +lemma linear_imp_scaleR:
    5.69 +  assumes "linear D" obtains d where "D = (\<lambda>x. x *\<^sub>R d)"
    5.70 +  by (metis assms linear.scaleR mult.commute mult.left_neutral real_scaleR_def)
    5.71 +
    5.72  lemma linearI:
    5.73    assumes "\<And>x y. f (x + y) = f x + f y"
    5.74    assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
    5.75 @@ -1503,6 +1547,11 @@
    5.76      by (auto intro: exI[of _ "f 1"] bounded_linear_mult_left)
    5.77  qed
    5.78  
    5.79 +lemma bij_linear_imp_inv_linear:
    5.80 +  assumes "linear f" "bij f" shows "linear (inv f)"
    5.81 +  using assms unfolding linear_def linear_axioms_def additive_def
    5.82 +  by (auto simp: bij_is_surj bij_is_inj surj_f_inv_f intro!:  Hilbert_Choice.inv_f_eq)
    5.83 +    
    5.84  instance real_normed_algebra_1 \<subseteq> perfect_space
    5.85  proof
    5.86    fix x::'a