# HG changeset patch # User paulson # Date 1438012377 -3600 # Node ID 7d04351c795aeffdf541708d4bc08dfb69c8a086 # Parent 57dd0b45fc2135f05dfef48974daa47e0d4fc6bf New material for Cauchy's integral theorem diff -r 57dd0b45fc21 -r 7d04351c795a src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Jul 27 16:35:12 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Jul 27 16:52:57 2015 +0100 @@ -1387,7 +1387,7 @@ by auto qed -lemma convex_ball: +lemma convex_ball [iff]: fixes x :: "'a::real_normed_vector" shows "convex (ball x e)" proof (auto simp add: convex_def) @@ -1404,7 +1404,7 @@ using convex_bound_lt[OF yz uv] by auto qed -lemma convex_cball: +lemma convex_cball [iff]: fixes x :: "'a::real_normed_vector" shows "convex (cball x e)" proof - @@ -3239,6 +3239,9 @@ shows "rel_interior S = S" by (metis assms interior_eq interior_subset_rel_interior rel_interior_subset set_eq_subset) +lemma interior_ball [simp]: "interior (ball x e) = ball x e" + by (simp add: interior_open) + lemma interior_rel_interior_gen: fixes S :: "'n::euclidean_space set" shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})" @@ -3551,7 +3554,7 @@ using mem_rel_interior[of "a+x" "((\x. a + x) ` S)"] by auto } then show ?thesis by auto -qed +qed lemma rel_interior_translation: fixes a :: "'n::euclidean_space" @@ -9317,9 +9320,9 @@ done qed + subsection \Coplanarity, and collinearity in terms of affine hull\ - definition coplanar where "coplanar s \ \u v w. s \ affine hull {u,v,w}" @@ -9425,26 +9428,46 @@ by auto (meson assms(1) coplanar_def) qed -(*? Still not ported -lemma COPLANAR_TRANSLATION_EQ: "coplanar((\x. a + x) ` s) \ coplanar s" - apply (simp add: coplanar_def) - apply (simp add: Set.image_subset_iff_subset_vimage) - apply (auto simp:) - apply (rule_tac x="u-a" in exI) - apply (rule_tac x="v-a" in exI) - apply (rule_tac x="w-a" in exI) - apply (auto simp:) - apply (drule_tac c="x+a" in subsetD) - apply (simp add: affine_alt) - -lemma COPLANAR_TRANSLATION: - !a:real^N s. coplanar s ==> coplanar(IMAGE (\x. a + x) s)" - REWRITE_TAC[COPLANAR_TRANSLATION_EQ]);; +lemma coplanar_translation_imp: "coplanar s \ coplanar ((\x. a + x) ` s)" + unfolding coplanar_def + apply clarify + apply (rule_tac x="u+a" in exI) + apply (rule_tac x="v+a" in exI) + apply (rule_tac x="w+a" in exI) + using affine_hull_translation [of a "{u,v,w}" for u v w] + apply (force simp: add.commute) + done + +lemma coplanar_translation_eq: "coplanar((\x. a + x) ` s) \ coplanar s" + by (metis (no_types) coplanar_translation_imp translation_galois) lemma coplanar_linear_image_eq: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "linear f" "inj f" shows "coplanar(f ` s) = coplanar s" - MATCH_ACCEPT_TAC(LINEAR_INVARIANT_RULE COPLANAR_LINEAR_IMAGE));; +proof + assume "coplanar s" + then show "coplanar (f ` s)" + unfolding coplanar_def + using affine_hull_linear_image [of f "{u,v,w}" for u v w] assms + by (meson coplanar_def coplanar_linear_image) +next + obtain g where g: "linear g" "g \ f = id" + using linear_injective_left_inverse [OF assms] + by blast + assume "coplanar (f ` s)" + then obtain u v w where "f ` s \ affine hull {u, v, w}" + by (auto simp: coplanar_def) + then have "g ` f ` s \ g ` (affine hull {u, v, w})" + by blast + then have "s \ g ` (affine hull {u, v, w})" + using g by (simp add: Fun.image_comp) + then show "coplanar s" + unfolding coplanar_def + using affine_hull_linear_image [of g "{u,v,w}" for u v w] `linear g` linear_conv_bounded_linear + by fastforce +qed +(*The HOL Light proof is simply + MATCH_ACCEPT_TAC(LINEAR_INVARIANT_RULE COPLANAR_LINEAR_IMAGE));; *) lemma coplanar_subset: "\coplanar t; s \ t\ \ coplanar s" diff -r 57dd0b45fc21 -r 7d04351c795a src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jul 27 16:35:12 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jul 27 16:52:57 2015 +0100 @@ -2315,4 +2315,9 @@ lemma vector_derivative_const_at [simp]: "vector_derivative (\x. c) (at a) = 0" by (simp add: vector_derivative_at) +lemma vector_derivative_at_within_ivl: + "(f has_vector_derivative f') (at x) \ + a \ x \ x \ b \ a vector_derivative f (at x within {a..b}) = f'" +using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce + end diff -r 57dd0b45fc21 -r 7d04351c795a src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Jul 27 16:35:12 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Jul 27 16:52:57 2015 +0100 @@ -6803,22 +6803,13 @@ lemma has_integral_affinity: fixes a :: "'a::euclidean_space" assumes "(f has_integral i) (cbox a b)" - and "m \ 0" + and "m \ 0" shows "((\x. f(m *\<^sub>R x + c)) has_integral ((1 / (abs(m) ^ DIM('a))) *\<^sub>R i)) ((\x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` cbox a b)" apply (rule has_integral_twiddle) - apply safe + using assms + apply (safe intro!: interval_image_affinity_interval content_image_affinity_cbox) apply (rule zero_less_power) - unfolding euclidean_eq_iff[where 'a='a] - unfolding scaleR_right_distrib inner_simps scaleR_scaleR - defer - apply (insert assms(2)) - apply (simp add: field_simps) - apply (insert assms(2)) - apply (simp add: field_simps) - apply (rule continuous_intros)+ - apply (rule interval_image_affinity_interval)+ - apply (rule content_image_affinity_cbox) - using assms + unfolding scaleR_right_distrib apply auto done @@ -6833,6 +6824,7 @@ apply auto done +lemmas has_integral_affinity01 = has_integral_affinity [of _ _ 0 "1::real", simplified] subsection \Special case of stretching coordinate axes separately.\ diff -r 57dd0b45fc21 -r 7d04351c795a src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Jul 27 16:35:12 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Jul 27 16:52:57 2015 +0100 @@ -255,7 +255,7 @@ done lemma linear_cmul: "linear f \ f (c *\<^sub>R x) = c *\<^sub>R f x" - by (simp add: linear_iff) + by (rule linear.scaleR) lemma linear_neg: "linear f \ f (- x) = - f x" using linear_cmul [where c="-1"] by simp @@ -2692,6 +2692,11 @@ with h(1) show ?thesis by blast qed +lemma inj_linear_imp_inv_linear: + fixes f :: "'a::euclidean_space \ 'a::euclidean_space" + assumes "linear f" "inj f" shows "linear (inv f)" +using assms inj_iff left_inverse_linear by blast + subsection \Infinity norm\ diff -r 57dd0b45fc21 -r 7d04351c795a src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Mon Jul 27 16:35:12 2015 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Mon Jul 27 16:52:57 2015 +0100 @@ -228,6 +228,29 @@ apply (erule (1) nonzero_inverse_scaleR_distrib) done +lemma real_vector_affinity_eq: + fixes x :: "'a :: real_vector" + assumes m0: "m \ 0" + shows "m *\<^sub>R x + c = y \ x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)" +proof + assume h: "m *\<^sub>R x + c = y" + hence "m *\<^sub>R x = y - c" by (simp add: field_simps) + hence "inverse m *\<^sub>R (m *\<^sub>R x) = inverse m *\<^sub>R (y - c)" by simp + then show "x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)" + using m0 + by (simp add: real_vector.scale_right_diff_distrib) +next + assume h: "x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)" + show "m *\<^sub>R x + c = y" unfolding h + using m0 by (simp add: real_vector.scale_right_diff_distrib) +qed + +lemma real_vector_eq_affinity: + fixes x :: "'a :: real_vector" + shows "m \ 0 ==> (y = m *\<^sub>R x + c \ inverse m *\<^sub>R y - (inverse m *\<^sub>R c) = x)" + using real_vector_affinity_eq[where m=m and x=x and y=y and c=c] + by metis + subsection \Embedding of the Reals into any @{text real_algebra_1}: @{term of_real}\ @@ -763,6 +786,18 @@ finally show ?thesis . qed +lemma norm_diff_triangle_le: + fixes x y z :: "'a::real_normed_vector" + assumes "norm (x - y) \ e1" "norm (y - z) \ e2" + shows "norm (x - z) \ e1 + e2" + using norm_diff_triangle_ineq [of x y y z] assms by simp + +lemma norm_diff_triangle_less: + fixes x y z :: "'a::real_normed_vector" + assumes "norm (x - y) < e1" "norm (y - z) < e2" + shows "norm (x - z) < e1 + e2" + using norm_diff_triangle_ineq [of x y y z] assms by simp + lemma norm_triangle_mono: fixes a b :: "'a::real_normed_vector" shows "\norm a \ r; norm b \ s\ \ norm (a + b) \ r + s" @@ -1123,6 +1158,11 @@ end +lemma dist_of_real [simp]: + fixes a :: "'a::real_normed_div_algebra" + shows "dist (of_real x :: 'a) (of_real y) = dist x y" +by (metis dist_norm norm_of_real of_real_diff real_norm_def) + declare [[code abort: "open :: real set \ bool"]] instance real :: linorder_topology @@ -1249,6 +1289,10 @@ locale linear = additive f for f :: "'a::real_vector \ 'b::real_vector" + assumes scaleR: "f (scaleR r x) = scaleR r (f x)" +lemma linear_imp_scaleR: + assumes "linear D" obtains d where "D = (\x. x *\<^sub>R d)" + by (metis assms linear.scaleR mult.commute mult.left_neutral real_scaleR_def) + lemma linearI: assumes "\x y. f (x + y) = f x + f y" assumes "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" @@ -1503,6 +1547,11 @@ by (auto intro: exI[of _ "f 1"] bounded_linear_mult_left) qed +lemma bij_linear_imp_inv_linear: + assumes "linear f" "bij f" shows "linear (inv f)" + using assms unfolding linear_def linear_axioms_def additive_def + by (auto simp: bij_is_surj bij_is_inj surj_f_inv_f intro!: Hilbert_Choice.inv_f_eq) + instance real_normed_algebra_1 \ perfect_space proof fix x::'a