--- 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" "((\<lambda>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 \<open>Coplanarity, and collinearity in terms of affine hull\<close>
-
definition coplanar where
"coplanar s \<equiv> \<exists>u v w. s \<subseteq> 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((\<lambda>x. a + x) ` s) \<longleftrightarrow> 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 \<Longrightarrow> coplanar ((\<lambda>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((\<lambda>x. a + x) ` s) \<longleftrightarrow> coplanar s"
+ by (metis (no_types) coplanar_translation_imp translation_galois)
lemma coplanar_linear_image_eq:
fixes f :: "'a::euclidean_space \<Rightarrow> '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 \<circ> f = id"
+ using linear_injective_left_inverse [OF assms]
+ by blast
+ assume "coplanar (f ` s)"
+ then obtain u v w where "f ` s \<subseteq> affine hull {u, v, w}"
+ by (auto simp: coplanar_def)
+ then have "g ` f ` s \<subseteq> g ` (affine hull {u, v, w})"
+ by blast
+ then have "s \<subseteq> 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: "\<lbrakk>coplanar t; s \<subseteq> t\<rbrakk> \<Longrightarrow> coplanar s"
--- 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 (\<lambda>x. c) (at a) = 0"
by (simp add: vector_derivative_at)
+lemma vector_derivative_at_within_ivl:
+ "(f has_vector_derivative f') (at x) \<Longrightarrow>
+ a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
+using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
+
end
--- 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 \<noteq> 0"
+ and "m \<noteq> 0"
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)"
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 \<open>Special case of stretching coordinate axes separately.\<close>
--- 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 \<Longrightarrow> f (c *\<^sub>R x) = c *\<^sub>R f x"
- by (simp add: linear_iff)
+ by (rule linear.scaleR)
lemma linear_neg: "linear f \<Longrightarrow> 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 \<Rightarrow> 'a::euclidean_space"
+ assumes "linear f" "inj f" shows "linear (inv f)"
+using assms inj_iff left_inverse_linear by blast
+
subsection \<open>Infinity norm\<close>
--- 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 \<noteq> 0"
+ shows "m *\<^sub>R x + c = y \<longleftrightarrow> 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 \<noteq> 0 ==> (y = m *\<^sub>R x + c \<longleftrightarrow> 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 \<open>Embedding of the Reals into any @{text real_algebra_1}:
@{term of_real}\<close>
@@ -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) \<le> e1" "norm (y - z) \<le> e2"
+ shows "norm (x - z) \<le> 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 "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> 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 \<Rightarrow> bool"]]
instance real :: linorder_topology
@@ -1249,6 +1289,10 @@
locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
+lemma linear_imp_scaleR:
+ assumes "linear D" obtains d where "D = (\<lambda>x. x *\<^sub>R d)"
+ by (metis assms linear.scaleR mult.commute mult.left_neutral real_scaleR_def)
+
lemma linearI:
assumes "\<And>x y. f (x + y) = f x + f y"
assumes "\<And>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 \<subseteq> perfect_space
proof
fix x::'a