--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Dec 27 22:54:17 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Dec 27 22:54:29 2018 +0100
@@ -2637,9 +2637,9 @@
}
moreover
have "(\<Sum>v\<in>y ` {1..k}. sum u {i \<in> {1..k}. y i = v}) = 1"
- unfolding sum_image_gen[OF fin, symmetric] using obt(2) by auto
+ unfolding sum.image_gen[OF fin, symmetric] using obt(2) by auto
moreover have "(\<Sum>v\<in>y ` {1..k}. sum u {i \<in> {1..k}. y i = v} *\<^sub>R v) = x"
- using sum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
+ using sum.image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
unfolding scaleR_left.sum using obt(3) by auto
ultimately
have "\<exists>S u. finite S \<and> S \<subseteq> p \<and> (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = x"
@@ -2683,8 +2683,8 @@
by (auto simp: sum_constant_scaleR)
}
then have "(\<Sum>x = 1..card S. u (f x)) = 1" "(\<Sum>i = 1..card S. u (f i) *\<^sub>R f i) = y"
- unfolding sum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f]
- and sum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
+ unfolding sum.image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f]
+ and sum.image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
unfolding f
using sum.cong [of S S "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card S}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
using sum.cong [of S S "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card S}. f x = y}. u (f x))" u]
--- a/src/HOL/Analysis/Euclidean_Space.thy Thu Dec 27 22:54:17 2018 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy Thu Dec 27 22:54:29 2018 +0100
@@ -7,7 +7,9 @@
theory Euclidean_Space
imports
- L2_Norm Product_Vector
+ L2_Norm
+ Inner_Product
+ Product_Vector
begin
subsection \<open>Type class of Euclidean spaces\<close>
@@ -261,6 +263,44 @@
subsubsection%unimportant \<open>Type @{typ "'a \<times> 'b"}\<close>
+instantiation prod :: (real_inner, real_inner) real_inner
+begin
+
+definition inner_prod_def:
+ "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"
+
+lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
+ unfolding inner_prod_def by simp
+
+instance
+proof
+ fix r :: real
+ fix x y z :: "'a::real_inner \<times> 'b::real_inner"
+ show "inner x y = inner y x"
+ unfolding inner_prod_def
+ by (simp add: inner_commute)
+ show "inner (x + y) z = inner x z + inner y z"
+ unfolding inner_prod_def
+ by (simp add: inner_add_left)
+ show "inner (scaleR r x) y = r * inner x y"
+ unfolding inner_prod_def
+ by (simp add: distrib_left)
+ show "0 \<le> inner x x"
+ unfolding inner_prod_def
+ by (intro add_nonneg_nonneg inner_ge_zero)
+ show "inner x x = 0 \<longleftrightarrow> x = 0"
+ unfolding inner_prod_def prod_eq_iff
+ by (simp add: add_nonneg_eq_0_iff)
+ show "norm x = sqrt (inner x x)"
+ unfolding norm_prod_def inner_prod_def
+ by (simp add: power2_norm_eq_inner)
+qed
+
+end
+
+lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
+ by (cases x, simp)+
+
instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
begin
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Dec 27 22:54:17 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Dec 27 22:54:29 2018 +0100
@@ -5924,7 +5924,7 @@
next
have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>\<D>. integral K (f (m x))))
\<le> norm (\<Sum>j = 0..s. \<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = j}. content K *\<^sub>R f (m x) x - integral K (f (m x)))"
- apply (subst sum_group)
+ apply (subst sum.group)
using s by (auto simp: sum_subtractf split_def p'(1))
also have "\<dots> < e/2"
proof -
--- a/src/HOL/Analysis/Inner_Product.thy Thu Dec 27 22:54:17 2018 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy Thu Dec 27 22:54:29 2018 +0100
@@ -177,11 +177,6 @@
using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
by (force simp add: power2_eq_square)
-lemma norm_triangle_sub:
- fixes x y :: "'a::real_normed_vector"
- shows "norm x \<le> norm y + norm (x - y)"
- using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
-
lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
by (simp add: norm_eq_sqrt_inner)
--- a/src/HOL/Analysis/Linear_Algebra.thy Thu Dec 27 22:54:17 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Dec 27 22:54:29 2018 +0100
@@ -76,12 +76,6 @@
using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
unfolding dist_norm[symmetric] .
-lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
- by (rule norm_triangle_ineq [THEN order_trans])
-
-lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
- by (rule norm_triangle_ineq [THEN le_less_trans])
-
lemma abs_triangle_half_r:
fixes y :: "'a::linordered_field"
shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e"
@@ -99,19 +93,6 @@
and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
by (auto simp add: insert_absorb)
-lemma sum_norm_bound:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
- shows "norm (sum f S) \<le> of_nat (card S)*K"
- using sum_norm_le[OF K] sum_constant[symmetric]
- by simp
-
-lemma sum_group:
- assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
- shows "sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) T = sum g S"
- unfolding sum_image_gen[OF fS, of g f]
- by (auto intro: sum.neutral sum.mono_neutral_right[OF fT fST])
-
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
proof
assume "\<forall>x. x \<bullet> y = x \<bullet> z"
--- a/src/HOL/Analysis/Product_Vector.thy Thu Dec 27 22:54:17 2018 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy Thu Dec 27 22:54:29 2018 +0100
@@ -5,9 +5,9 @@
section \<open>Cartesian Products as Vector Spaces\<close>
theory Product_Vector
-imports
- Inner_Product
- "HOL-Library.Product_Plus"
+ imports
+ Complex_Main
+ "HOL-Library.Product_Plus"
begin
lemma Times_eq_image_sum:
@@ -395,47 +395,6 @@
using assms
by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
-
-subsection \<open>Product is an inner product space\<close>
-
-instantiation prod :: (real_inner, real_inner) real_inner
-begin
-
-definition inner_prod_def:
- "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"
-
-lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
- unfolding inner_prod_def by simp
-
-instance
-proof
- fix r :: real
- fix x y z :: "'a::real_inner \<times> 'b::real_inner"
- show "inner x y = inner y x"
- unfolding inner_prod_def
- by (simp add: inner_commute)
- show "inner (x + y) z = inner x z + inner y z"
- unfolding inner_prod_def
- by (simp add: inner_add_left)
- show "inner (scaleR r x) y = r * inner x y"
- unfolding inner_prod_def
- by (simp add: distrib_left)
- show "0 \<le> inner x x"
- unfolding inner_prod_def
- by (intro add_nonneg_nonneg inner_ge_zero)
- show "inner x x = 0 \<longleftrightarrow> x = 0"
- unfolding inner_prod_def prod_eq_iff
- by (simp add: add_nonneg_eq_0_iff)
- show "norm x = sqrt (inner x x)"
- unfolding norm_prod_def inner_prod_def
- by (simp add: power2_norm_eq_inner)
-qed
-
-end
-
-lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
- by (cases x, simp)+
-
lemma
fixes x :: "'a::real_normed_vector"
shows norm_Pair1 [simp]: "norm (0,x) = norm x"
--- a/src/HOL/Groups_Big.thy Thu Dec 27 22:54:17 2018 +0100
+++ b/src/HOL/Groups_Big.thy Thu Dec 27 22:54:29 2018 +0100
@@ -439,6 +439,25 @@
F (\<lambda>x. F (g x) {y. y \<in> B \<and> R x y}) A = F (\<lambda>y. F (\<lambda>x. g x y) {x. x \<in> A \<and> R x y}) B"
by (simp add: inter_filter) (rule swap)
+lemma image_gen:
+ assumes fin: "finite S"
+ shows "F h S = F (\<lambda>y. F h {x. x \<in> S \<and> g x = y}) (g ` S)"
+proof -
+ have "{y. y\<in> g`S \<and> g x = y} = {g x}" if "x \<in> S" for x
+ using that by auto
+ then have "F h S = F (\<lambda>x. F (\<lambda>y. h x) {y. y\<in> g`S \<and> g x = y}) S"
+ by simp
+ also have "\<dots> = F (\<lambda>y. F h {x. x \<in> S \<and> g x = y}) (g ` S)"
+ by (rule swap_restrict [OF fin finite_imageI [OF fin]])
+ finally show ?thesis .
+qed
+
+lemma group:
+ assumes fS: "finite S" and fT: "finite T" and fST: "g ` S \<subseteq> T"
+ shows "F (\<lambda>y. F h {x. x \<in> S \<and> g x = y}) T = F h S"
+ unfolding image_gen[OF fS, of h g]
+ by (auto intro: neutral mono_neutral_right[OF fT fST])
+
lemma Plus:
fixes A :: "'b set" and B :: "'c set"
assumes fin: "finite A" "finite B"
@@ -534,21 +553,6 @@
in [(@{const_syntax sum}, K sum_tr')] end
\<close>
-(* TODO generalization candidates *)
-
-lemma (in comm_monoid_add) sum_image_gen:
- assumes fin: "finite S"
- shows "sum g S = sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) (f ` S)"
-proof -
- have "{y. y\<in> f`S \<and> f x = y} = {f x}" if "x \<in> S" for x
- using that by auto
- then have "sum g S = sum (\<lambda>x. sum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
- by simp
- also have "\<dots> = sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) (f ` S)"
- by (rule sum.swap_restrict [OF fin finite_imageI [OF fin]])
- finally show ?thesis .
-qed
-
subsubsection \<open>Properties in more restricted classes of structures\<close>
@@ -756,7 +760,7 @@
also have "\<dots> \<le> sum (\<lambda>y. sum g {x. x\<in>t \<and> i x = y}) (i ` t)"
using assms(2-4) by (auto intro!: sum_mono2 sum_nonneg)
also have "\<dots> \<le> sum g t"
- using assms by (auto simp: sum_image_gen[symmetric])
+ using assms by (auto simp: sum.image_gen[symmetric])
finally show ?thesis .
qed
--- a/src/HOL/Real_Vector_Spaces.thy Thu Dec 27 22:54:17 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Thu Dec 27 22:54:29 2018 +0100
@@ -648,33 +648,34 @@
then show "norm (1::'a) = 1" by simp
qed
-lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0"
+context real_normed_vector begin
+
+lemma norm_zero [simp]: "norm (0::'a) = 0"
by simp
lemma zero_less_norm_iff [simp]: "norm x > 0 \<longleftrightarrow> x \<noteq> 0"
- for x :: "'a::real_normed_vector"
by (simp add: order_less_le)
lemma norm_not_less_zero [simp]: "\<not> norm x < 0"
- for x :: "'a::real_normed_vector"
by (simp add: linorder_not_less)
lemma norm_le_zero_iff [simp]: "norm x \<le> 0 \<longleftrightarrow> x = 0"
- for x :: "'a::real_normed_vector"
by (simp add: order_le_less)
lemma norm_minus_cancel [simp]: "norm (- x) = norm x"
- for x :: "'a::real_normed_vector"
proof -
- have "norm (- x) = norm (scaleR (- 1) x)"
- by (simp only: scaleR_minus_left scaleR_one)
+ have "- 1 *\<^sub>R x = - (1 *\<^sub>R x)"
+ unfolding add_eq_0_iff2[symmetric] scaleR_add_left[symmetric]
+ using norm_eq_zero
+ by fastforce
+ then have "norm (- x) = norm (scaleR (- 1) x)"
+ by (simp only: scaleR_one)
also have "\<dots> = \<bar>- 1\<bar> * norm x"
by (rule norm_scaleR)
finally show ?thesis by simp
qed
lemma norm_minus_commute: "norm (a - b) = norm (b - a)"
- for a b :: "'a::real_normed_vector"
proof -
have "norm (- (b - a)) = norm (b - a)"
by (rule norm_minus_cancel)
@@ -682,22 +683,15 @@
qed
lemma dist_add_cancel [simp]: "dist (a + b) (a + c) = dist b c"
- for a :: "'a::real_normed_vector"
by (simp add: dist_norm)
lemma dist_add_cancel2 [simp]: "dist (b + a) (c + a) = dist b c"
- for a :: "'a::real_normed_vector"
by (simp add: dist_norm)
-lemma dist_scaleR [simp]: "dist (x *\<^sub>R a) (y *\<^sub>R a) = \<bar>x - y\<bar> * norm a"
- for a :: "'a::real_normed_vector"
- by (metis dist_norm norm_scaleR scaleR_left.diff)
-
-lemma norm_uminus_minus: "norm (- x - y :: 'a :: real_normed_vector) = norm (x + y)"
+lemma norm_uminus_minus: "norm (- x - y) = norm (x + y)"
by (subst (2) norm_minus_cancel[symmetric], subst minus_add_distrib) simp
lemma norm_triangle_ineq2: "norm a - norm b \<le> norm (a - b)"
- for a b :: "'a::real_normed_vector"
proof -
have "norm (a - b + b) \<le> norm (a - b) + norm b"
by (rule norm_triangle_ineq)
@@ -705,7 +699,6 @@
qed
lemma norm_triangle_ineq3: "\<bar>norm a - norm b\<bar> \<le> norm (a - b)"
- for a b :: "'a::real_normed_vector"
proof -
have "norm a - norm b \<le> norm (a - b)"
by (simp add: norm_triangle_ineq2)
@@ -716,32 +709,35 @@
qed
lemma norm_triangle_ineq4: "norm (a - b) \<le> norm a + norm b"
- for a b :: "'a::real_normed_vector"
proof -
have "norm (a + - b) \<le> norm a + norm (- b)"
by (rule norm_triangle_ineq)
then show ?thesis by simp
qed
-lemma norm_triangle_le_diff:
- fixes x y :: "'a::real_normed_vector"
- shows "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"
+lemma norm_triangle_le_diff: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"
by (meson norm_triangle_ineq4 order_trans)
lemma norm_diff_ineq: "norm a - norm b \<le> norm (a + b)"
- for a b :: "'a::real_normed_vector"
proof -
have "norm a - norm (- b) \<le> norm (a - - b)"
by (rule norm_triangle_ineq2)
then show ?thesis by simp
qed
+lemma norm_triangle_sub: "norm x \<le> norm y + norm (x - y)"
+ using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
+
+lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
+ by (rule norm_triangle_ineq [THEN order_trans])
+
+lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
+ by (rule norm_triangle_ineq [THEN le_less_trans])
+
lemma norm_add_leD: "norm (a + b) \<le> c \<Longrightarrow> norm b \<le> norm a + c"
- for a b :: "'a::real_normed_vector"
- by (metis add.commute diff_le_eq norm_diff_ineq order.trans)
+ by (metis ab_semigroup_add_class.add.commute add_commute diff_le_eq norm_diff_ineq order_trans)
lemma norm_diff_triangle_ineq: "norm ((a + b) - (c + d)) \<le> norm (a - c) + norm (b - d)"
- for a b c d :: "'a::real_normed_vector"
proof -
have "norm ((a + b) - (c + d)) = norm ((a - c) + (b - d))"
by (simp add: algebra_simps)
@@ -750,42 +746,54 @@
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_le: "norm (x - z) \<le> e1 + e2"
+ if "norm (x - y) \<le> e1" "norm (y - z) \<le> e2"
+proof -
+ have "norm (x - (y + z - y)) \<le> norm (x - y) + norm (y - z)"
+ using norm_diff_triangle_ineq that diff_diff_eq2 by presburger
+ with that show ?thesis by simp
+qed
-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_diff_triangle_less: "norm (x - z) < e1 + e2"
+ if "norm (x - y) < e1" "norm (y - z) < e2"
+proof -
+ have "norm (x - z) \<le> norm (x - y) + norm (y - z)"
+ by (metis norm_diff_triangle_ineq add_diff_cancel_left' diff_diff_eq2)
+ with that show ?thesis by auto
+qed
lemma norm_triangle_mono:
- fixes a b :: "'a::real_normed_vector"
- shows "norm a \<le> r \<Longrightarrow> norm b \<le> s \<Longrightarrow> norm (a + b) \<le> r + s"
- by (metis add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
+ "norm a \<le> r \<Longrightarrow> norm b \<le> s \<Longrightarrow> norm (a + b) \<le> r + s"
+ by (metis (mono_tags) add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
-lemma norm_sum:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- shows "norm (sum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
+lemma norm_sum: "norm (sum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
+ for f::"'b \<Rightarrow> 'a"
by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono)
-lemma sum_norm_le:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
- shows "norm (sum f S) \<le> sum g S"
- by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
+lemma sum_norm_le: "norm (sum f S) \<le> sum g S"
+ if "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
+ for f::"'b \<Rightarrow> 'a"
+ by (rule order_trans [OF norm_sum sum_mono]) (simp add: that)
lemma abs_norm_cancel [simp]: "\<bar>norm a\<bar> = norm a"
- for a :: "'a::real_normed_vector"
by (rule abs_of_nonneg [OF norm_ge_zero])
+lemma sum_norm_bound:
+ "norm (sum f S) \<le> of_nat (card S)*K"
+ if "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
+ for f :: "'b \<Rightarrow> 'a"
+ using sum_norm_le[OF that] sum_constant[symmetric]
+ by simp
+
lemma norm_add_less: "norm x < r \<Longrightarrow> norm y < s \<Longrightarrow> norm (x + y) < r + s"
- for x y :: "'a::real_normed_vector"
by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono])
+end
+
+lemma dist_scaleR [simp]: "dist (x *\<^sub>R a) (y *\<^sub>R a) = \<bar>x - y\<bar> * norm a"
+ for a :: "'a::real_normed_vector"
+ by (metis dist_norm norm_scaleR scaleR_left.diff)
+
lemma norm_mult_less: "norm x < r \<Longrightarrow> norm y < s \<Longrightarrow> norm (x * y) < r * s"
for x y :: "'a::real_normed_algebra"
by (rule order_le_less_trans [OF norm_mult_ineq]) (simp add: mult_strict_mono')