author nipkow Thu, 07 Dec 2017 15:48:50 +0100 changeset 67155 9e5b05d54f9d parent 67154 c7def8f836d0 child 67156 3a9966b88a50 child 67157 d0657c8b7616
canonical name
```--- 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 (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"
+      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"
also have "... < DIM('b) * (e / real DIM('b))"
apply (rule sum_bounded_above_strict)
using that by auto
also have "... = e"
-      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
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
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
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
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
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

-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
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 (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)```