--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Dec 07 15:48:50 2017 +0100
@@ -290,7 +290,7 @@
lemma component_le_norm_cart: "\<bar>x$i\<bar> <= norm x"
apply (simp add: norm_vec_def)
- apply (rule member_le_setL2, simp_all)
+ apply (rule member_le_L2_set, simp_all)
done
lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x$i\<bar> <= e"
@@ -300,7 +300,7 @@
by (metis component_le_norm_cart le_less_trans)
lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
- by (simp add: norm_vec_def setL2_le_sum)
+ by (simp add: norm_vec_def L2_set_le_sum)
lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
unfolding scaleR_vec_def vector_scalar_mult_def by simp
@@ -984,7 +984,7 @@
{ fix n
assume n: "\<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))"
have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) $ i) (l $ i))"
- unfolding dist_vec_def using zero_le_dist by (rule setL2_le_sum)
+ unfolding dist_vec_def using zero_le_dist by (rule L2_set_le_sum)
also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
by (rule sum_strict_mono) (simp_all add: n)
finally have "dist (f (r n)) l < e" by simp
--- a/src/HOL/Analysis/Connected.thy Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/Connected.thy Thu Dec 07 15:48:50 2017 +0100
@@ -2854,7 +2854,7 @@
lemma diameter_cbox:
fixes a b::"'a::euclidean_space"
shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
- by (force simp: diameter_def intro!: cSup_eq_maximum setL2_mono
+ by (force simp: diameter_def intro!: cSup_eq_maximum L2_set_mono
simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
subsection \<open>Separation between points and sets\<close>
@@ -5038,7 +5038,7 @@
text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
- by (metis (no_types) member_le_setL2 euclidean_dist_l2 finite_Basis)
+ by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
text\<open>But is the premise @{term \<open>i \<in> Basis\<close>} really necessary?\<close>
lemma open_preimage_inner:
@@ -5087,17 +5087,17 @@
proof clarify
fix e::real
assume "0 < e"
- have *: "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
+ have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
proof -
- have "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> sum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
- by (simp add: setL2_le_sum)
+ have "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> sum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
+ by (simp add: L2_set_le_sum)
also have "... < DIM('b) * (e / real DIM('b))"
apply (rule sum_bounded_above_strict)
using that by auto
also have "... = e"
by (simp add: field_simps)
- finally show "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
+ finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
qed
have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
apply (rule R')
@@ -5516,7 +5516,7 @@
by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
then show ?thesis
by (auto intro: real_sqrt_le_mono
- simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
+ simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
qed (auto simp: clamp_def)
lemma clamp_continuous_at:
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Dec 07 15:48:50 2017 +0100
@@ -7262,7 +7262,7 @@
unfolding 2
apply clarsimp
apply (subst euclidean_dist_l2)
- apply (rule order_trans [OF setL2_le_sum])
+ apply (rule order_trans [OF L2_set_le_sum])
apply (rule zero_le_dist)
unfolding e'
apply (rule sum_mono)
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Dec 07 15:48:50 2017 +0100
@@ -342,7 +342,7 @@
begin
definition
- "dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
+ "dist x y = L2_set (\<lambda>i. dist (x$i) (y$i)) UNIV"
instance ..
end
@@ -364,19 +364,19 @@
begin
lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
- unfolding dist_vec_def by (rule member_le_setL2) simp_all
+ unfolding dist_vec_def by (rule member_le_L2_set) simp_all
instance proof
fix x y :: "'a ^ 'b"
show "dist x y = 0 \<longleftrightarrow> x = y"
unfolding dist_vec_def
- by (simp add: setL2_eq_0_iff vec_eq_iff)
+ by (simp add: L2_set_eq_0_iff vec_eq_iff)
next
fix x y z :: "'a ^ 'b"
show "dist x y \<le> dist x z + dist y z"
unfolding dist_vec_def
- apply (rule order_trans [OF _ setL2_triangle_ineq])
- apply (simp add: setL2_mono dist_triangle2)
+ apply (rule order_trans [OF _ L2_set_triangle_ineq])
+ apply (simp add: L2_set_mono dist_triangle2)
done
next
fix S :: "('a ^ 'b) set"
@@ -407,13 +407,13 @@
define r where [abs_def]: "r i = e / sqrt (of_nat CARD('b))" for i :: 'b
from \<open>0 < e\<close> have r: "\<forall>i. 0 < r i"
unfolding r_def by simp_all
- from \<open>0 < e\<close> have e: "e = setL2 r UNIV"
- unfolding r_def by (simp add: setL2_constant)
+ from \<open>0 < e\<close> have e: "e = L2_set r UNIV"
+ unfolding r_def by (simp add: L2_set_constant)
define A where "A i = {y. dist (x $ i) y < r i}" for i
have "\<forall>i. open (A i) \<and> x $ i \<in> A i"
unfolding A_def by (simp add: open_ball r)
moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
- by (simp add: A_def S dist_vec_def e setL2_strict_mono dist_commute)
+ by (simp add: A_def S dist_vec_def e L2_set_strict_mono dist_commute)
ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and>
(\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
qed
@@ -447,10 +447,10 @@
{
fix m n :: nat
assume "M \<le> m" "M \<le> n"
- have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
+ have "dist (X m) (X n) = L2_set (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
unfolding dist_vec_def ..
also have "\<dots> \<le> sum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
- by (rule setL2_le_sum [OF zero_le_dist])
+ by (rule L2_set_le_sum [OF zero_le_dist])
also have "\<dots> < sum (\<lambda>i::'n. ?s) UNIV"
by (rule sum_strict_mono, simp_all add: M \<open>M \<le> m\<close> \<open>M \<le> n\<close>)
also have "\<dots> = r"
@@ -480,7 +480,7 @@
instantiation vec :: (real_normed_vector, finite) real_normed_vector
begin
-definition "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV"
+definition "norm x = L2_set (\<lambda>i. norm (x$i)) UNIV"
definition "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
@@ -488,15 +488,15 @@
fix a :: real and x y :: "'a ^ 'b"
show "norm x = 0 \<longleftrightarrow> x = 0"
unfolding norm_vec_def
- by (simp add: setL2_eq_0_iff vec_eq_iff)
+ by (simp add: L2_set_eq_0_iff vec_eq_iff)
show "norm (x + y) \<le> norm x + norm y"
unfolding norm_vec_def
- apply (rule order_trans [OF _ setL2_triangle_ineq])
- apply (simp add: setL2_mono norm_triangle_ineq)
+ apply (rule order_trans [OF _ L2_set_triangle_ineq])
+ apply (simp add: L2_set_mono norm_triangle_ineq)
done
show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
unfolding norm_vec_def
- by (simp add: setL2_right_distrib)
+ by (simp add: L2_set_right_distrib)
show "sgn x = scaleR (inverse (norm x)) x"
by (rule sgn_vec_def)
show "dist x y = norm (x - y)"
@@ -508,7 +508,7 @@
lemma norm_nth_le: "norm (x $ i) \<le> norm x"
unfolding norm_vec_def
-by (rule member_le_setL2) simp_all
+by (rule member_le_L2_set) simp_all
lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
apply standard
@@ -545,7 +545,7 @@
unfolding inner_vec_def
by (simp add: vec_eq_iff sum_nonneg_eq_0_iff)
show "norm x = sqrt (inner x x)"
- unfolding inner_vec_def norm_vec_def setL2_def
+ unfolding inner_vec_def norm_vec_def L2_set_def
by (simp add: power2_norm_eq_inner)
qed
--- a/src/HOL/Analysis/L2_Norm.thy Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy Thu Dec 07 15:48:50 2017 +0100
@@ -8,74 +8,73 @@
imports Complex_Main
begin
-definition
- "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
+definition "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
-lemma setL2_cong:
- "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
- unfolding setL2_def by simp
+lemma L2_set_cong:
+ "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
+ unfolding L2_set_def by simp
-lemma strong_setL2_cong:
- "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
- unfolding setL2_def simp_implies_def by simp
+lemma strong_L2_set_cong:
+ "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
+ unfolding L2_set_def simp_implies_def by simp
-lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
- unfolding setL2_def by simp
+lemma L2_set_infinite [simp]: "\<not> finite A \<Longrightarrow> L2_set f A = 0"
+ unfolding L2_set_def by simp
+
+lemma L2_set_empty [simp]: "L2_set f {} = 0"
+ unfolding L2_set_def by simp
-lemma setL2_empty [simp]: "setL2 f {} = 0"
- unfolding setL2_def by simp
+lemma L2_set_insert [simp]:
+ "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
+ L2_set f (insert a F) = sqrt ((f a)\<^sup>2 + (L2_set f F)\<^sup>2)"
+ unfolding L2_set_def by (simp add: sum_nonneg)
-lemma setL2_insert [simp]:
- "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
- setL2 f (insert a F) = sqrt ((f a)\<^sup>2 + (setL2 f F)\<^sup>2)"
- unfolding setL2_def by (simp add: sum_nonneg)
+lemma L2_set_nonneg [simp]: "0 \<le> L2_set f A"
+ unfolding L2_set_def by (simp add: sum_nonneg)
-lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
- unfolding setL2_def by (simp add: sum_nonneg)
+lemma L2_set_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> L2_set f A = 0"
+ unfolding L2_set_def by simp
-lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
- unfolding setL2_def by simp
+lemma L2_set_constant: "L2_set (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
+ unfolding L2_set_def by (simp add: real_sqrt_mult)
-lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
- unfolding setL2_def by (simp add: real_sqrt_mult)
-
-lemma setL2_mono:
+lemma L2_set_mono:
assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
- shows "setL2 f K \<le> setL2 g K"
- unfolding setL2_def
+ shows "L2_set f K \<le> L2_set g K"
+ unfolding L2_set_def
by (simp add: sum_nonneg sum_mono power_mono assms)
-lemma setL2_strict_mono:
+lemma L2_set_strict_mono:
assumes "finite K" and "K \<noteq> {}"
assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
- shows "setL2 f K < setL2 g K"
- unfolding setL2_def
+ shows "L2_set f K < L2_set g K"
+ unfolding L2_set_def
by (simp add: sum_strict_mono power_strict_mono assms)
-lemma setL2_right_distrib:
- "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
- unfolding setL2_def
+lemma L2_set_right_distrib:
+ "0 \<le> r \<Longrightarrow> r * L2_set f A = L2_set (\<lambda>x. r * f x) A"
+ unfolding L2_set_def
apply (simp add: power_mult_distrib)
apply (simp add: sum_distrib_left [symmetric])
apply (simp add: real_sqrt_mult sum_nonneg)
done
-lemma setL2_left_distrib:
- "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
- unfolding setL2_def
+lemma L2_set_left_distrib:
+ "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A"
+ unfolding L2_set_def
apply (simp add: power_mult_distrib)
apply (simp add: sum_distrib_right [symmetric])
apply (simp add: real_sqrt_mult sum_nonneg)
done
-lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
- unfolding setL2_def
+lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+ unfolding L2_set_def
by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
-lemma setL2_triangle_ineq:
- shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
+lemma L2_set_triangle_ineq:
+ shows "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
proof (cases "finite A")
case False
thus ?thesis by simp
@@ -87,12 +86,12 @@
show ?case by simp
next
case (insert x F)
- hence "sqrt ((f x + g x)\<^sup>2 + (setL2 (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
- sqrt ((f x + g x)\<^sup>2 + (setL2 f F + setL2 g F)\<^sup>2)"
+ hence "sqrt ((f x + g x)\<^sup>2 + (L2_set (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
+ sqrt ((f x + g x)\<^sup>2 + (L2_set f F + L2_set g F)\<^sup>2)"
by (intro real_sqrt_le_mono add_left_mono power_mono insert
- setL2_nonneg add_increasing zero_le_power2)
+ L2_set_nonneg add_increasing zero_le_power2)
also have
- "\<dots> \<le> sqrt ((f x)\<^sup>2 + (setL2 f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (setL2 g F)\<^sup>2)"
+ "\<dots> \<le> sqrt ((f x)\<^sup>2 + (L2_set f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (L2_set g F)\<^sup>2)"
by (rule real_sqrt_sum_squares_triangle_ineq)
finally show ?case
using insert by simp
@@ -106,8 +105,8 @@
apply simp
done
-lemma setL2_le_sum [rule_format]:
- "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> sum f A"
+lemma L2_set_le_sum [rule_format]:
+ "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
apply (cases "finite A")
apply (induct set: finite)
apply simp
@@ -124,7 +123,7 @@
apply simp
done
-lemma setL2_le_sum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
+lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
apply (cases "finite A")
apply (induct set: finite)
apply simp
@@ -134,7 +133,7 @@
apply simp
done
-lemma setL2_mult_ineq_lemma:
+lemma L2_set_mult_ineq_lemma:
fixes a b c d :: real
shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
proof -
@@ -147,7 +146,7 @@
by simp
qed
-lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
+lemma L2_set_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> L2_set f A * L2_set g A"
apply (cases "finite A")
apply (induct set: finite)
apply simp
@@ -160,12 +159,12 @@
apply (simp add: power_mult_distrib)
apply (simp add: distrib_left distrib_right)
apply (rule ord_le_eq_trans)
- apply (rule setL2_mult_ineq_lemma)
+ apply (rule L2_set_mult_ineq_lemma)
apply simp_all
done
-lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
- unfolding setL2_def
+lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A"
+ unfolding L2_set_def
by (auto intro!: member_le_sum real_le_rsqrt)
end
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Dec 07 11:14:32 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Dec 07 15:48:50 2017 +0100
@@ -1249,8 +1249,8 @@
lemma euclidean_dist_l2:
fixes x y :: "'a :: euclidean_space"
- shows "dist x y = setL2 (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
- unfolding dist_norm norm_eq_sqrt_inner setL2_def
+ shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
+ unfolding dist_norm norm_eq_sqrt_inner L2_set_def
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
@@ -1358,7 +1358,7 @@
fix y :: 'a
assume *: "y \<in> box ?a ?b"
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
- unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
+ unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
proof (rule real_sqrt_less_mono, rule sum_strict_mono)
fix i :: "'a"
@@ -1460,7 +1460,7 @@
fix y :: 'a
assume *: "y \<in> cbox ?a ?b"
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
- unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
+ unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
proof (rule real_sqrt_less_mono, rule sum_strict_mono)
fix i :: "'a"
@@ -4579,7 +4579,7 @@
have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
apply (subst euclidean_dist_l2)
using zero_le_dist
- apply (rule setL2_le_sum)
+ apply (rule L2_set_le_sum)
done
also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
apply (rule sum_strict_mono)