canonical name
authornipkow
Thu Dec 07 15:48:50 2017 +0100 (9 months ago)
changeset 671559e5b05d54f9d
parent 67154 c7def8f836d0
child 67156 3a9966b88a50
child 67157 d0657c8b7616
canonical name
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/L2_Norm.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Dec 07 11:14:32 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Dec 07 15:48:50 2017 +0100
     1.3 @@ -290,7 +290,7 @@
     1.4  
     1.5  lemma component_le_norm_cart: "\<bar>x$i\<bar> <= norm x"
     1.6    apply (simp add: norm_vec_def)
     1.7 -  apply (rule member_le_setL2, simp_all)
     1.8 +  apply (rule member_le_L2_set, simp_all)
     1.9    done
    1.10  
    1.11  lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x$i\<bar> <= e"
    1.12 @@ -300,7 +300,7 @@
    1.13    by (metis component_le_norm_cart le_less_trans)
    1.14  
    1.15  lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
    1.16 -  by (simp add: norm_vec_def setL2_le_sum)
    1.17 +  by (simp add: norm_vec_def L2_set_le_sum)
    1.18  
    1.19  lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
    1.20    unfolding scaleR_vec_def vector_scalar_mult_def by simp
    1.21 @@ -984,7 +984,7 @@
    1.22      { fix n
    1.23        assume n: "\<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))"
    1.24        have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) $ i) (l $ i))"
    1.25 -        unfolding dist_vec_def using zero_le_dist by (rule setL2_le_sum)
    1.26 +        unfolding dist_vec_def using zero_le_dist by (rule L2_set_le_sum)
    1.27        also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
    1.28          by (rule sum_strict_mono) (simp_all add: n)
    1.29        finally have "dist (f (r n)) l < e" by simp
     2.1 --- a/src/HOL/Analysis/Connected.thy	Thu Dec 07 11:14:32 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Connected.thy	Thu Dec 07 15:48:50 2017 +0100
     2.3 @@ -2854,7 +2854,7 @@
     2.4  lemma diameter_cbox:
     2.5    fixes a b::"'a::euclidean_space"
     2.6    shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
     2.7 -  by (force simp: diameter_def intro!: cSup_eq_maximum setL2_mono
     2.8 +  by (force simp: diameter_def intro!: cSup_eq_maximum L2_set_mono
     2.9       simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
    2.10  
    2.11  subsection \<open>Separation between points and sets\<close>
    2.12 @@ -5038,7 +5038,7 @@
    2.13  
    2.14  text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
    2.15  lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
    2.16 -  by (metis (no_types) member_le_setL2 euclidean_dist_l2 finite_Basis)
    2.17 +  by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis)
    2.18  
    2.19  text\<open>But is the premise @{term \<open>i \<in> Basis\<close>} really necessary?\<close>
    2.20  lemma open_preimage_inner:
    2.21 @@ -5087,17 +5087,17 @@
    2.22    proof clarify
    2.23      fix e::real
    2.24      assume "0 < e"
    2.25 -    have *: "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
    2.26 +    have *: "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
    2.27               if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
    2.28      proof -
    2.29 -      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"
    2.30 -        by (simp add: setL2_le_sum)
    2.31 +      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"
    2.32 +        by (simp add: L2_set_le_sum)
    2.33        also have "... < DIM('b) * (e / real DIM('b))"
    2.34          apply (rule sum_bounded_above_strict)
    2.35          using that by auto
    2.36        also have "... = e"
    2.37          by (simp add: field_simps)
    2.38 -      finally show "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
    2.39 +      finally show "L2_set (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
    2.40      qed
    2.41      have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
    2.42        apply (rule R')
    2.43 @@ -5516,7 +5516,7 @@
    2.44      by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
    2.45    then show ?thesis
    2.46      by (auto intro: real_sqrt_le_mono
    2.47 -      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
    2.48 +      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def)
    2.49  qed (auto simp: clamp_def)
    2.50  
    2.51  lemma clamp_continuous_at:
     3.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 07 11:14:32 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 07 15:48:50 2017 +0100
     3.3 @@ -7262,7 +7262,7 @@
     3.4        unfolding 2
     3.5        apply clarsimp
     3.6        apply (subst euclidean_dist_l2)
     3.7 -      apply (rule order_trans [OF setL2_le_sum])
     3.8 +      apply (rule order_trans [OF L2_set_le_sum])
     3.9        apply (rule zero_le_dist)
    3.10        unfolding e'
    3.11        apply (rule sum_mono)
     4.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Dec 07 11:14:32 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Dec 07 15:48:50 2017 +0100
     4.3 @@ -342,7 +342,7 @@
     4.4  begin
     4.5  
     4.6  definition
     4.7 -  "dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
     4.8 +  "dist x y = L2_set (\<lambda>i. dist (x$i) (y$i)) UNIV"
     4.9  
    4.10  instance ..
    4.11  end
    4.12 @@ -364,19 +364,19 @@
    4.13  begin
    4.14  
    4.15  lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
    4.16 -  unfolding dist_vec_def by (rule member_le_setL2) simp_all
    4.17 +  unfolding dist_vec_def by (rule member_le_L2_set) simp_all
    4.18  
    4.19  instance proof
    4.20    fix x y :: "'a ^ 'b"
    4.21    show "dist x y = 0 \<longleftrightarrow> x = y"
    4.22      unfolding dist_vec_def
    4.23 -    by (simp add: setL2_eq_0_iff vec_eq_iff)
    4.24 +    by (simp add: L2_set_eq_0_iff vec_eq_iff)
    4.25  next
    4.26    fix x y z :: "'a ^ 'b"
    4.27    show "dist x y \<le> dist x z + dist y z"
    4.28      unfolding dist_vec_def
    4.29 -    apply (rule order_trans [OF _ setL2_triangle_ineq])
    4.30 -    apply (simp add: setL2_mono dist_triangle2)
    4.31 +    apply (rule order_trans [OF _ L2_set_triangle_ineq])
    4.32 +    apply (simp add: L2_set_mono dist_triangle2)
    4.33      done
    4.34  next
    4.35    fix S :: "('a ^ 'b) set"
    4.36 @@ -407,13 +407,13 @@
    4.37        define r where [abs_def]: "r i = e / sqrt (of_nat CARD('b))" for i :: 'b
    4.38        from \<open>0 < e\<close> have r: "\<forall>i. 0 < r i"
    4.39          unfolding r_def by simp_all
    4.40 -      from \<open>0 < e\<close> have e: "e = setL2 r UNIV"
    4.41 -        unfolding r_def by (simp add: setL2_constant)
    4.42 +      from \<open>0 < e\<close> have e: "e = L2_set r UNIV"
    4.43 +        unfolding r_def by (simp add: L2_set_constant)
    4.44        define A where "A i = {y. dist (x $ i) y < r i}" for i
    4.45        have "\<forall>i. open (A i) \<and> x $ i \<in> A i"
    4.46          unfolding A_def by (simp add: open_ball r)
    4.47        moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
    4.48 -        by (simp add: A_def S dist_vec_def e setL2_strict_mono dist_commute)
    4.49 +        by (simp add: A_def S dist_vec_def e L2_set_strict_mono dist_commute)
    4.50        ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and>
    4.51          (\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
    4.52      qed
    4.53 @@ -447,10 +447,10 @@
    4.54    {
    4.55      fix m n :: nat
    4.56      assume "M \<le> m" "M \<le> n"
    4.57 -    have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
    4.58 +    have "dist (X m) (X n) = L2_set (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
    4.59        unfolding dist_vec_def ..
    4.60      also have "\<dots> \<le> sum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
    4.61 -      by (rule setL2_le_sum [OF zero_le_dist])
    4.62 +      by (rule L2_set_le_sum [OF zero_le_dist])
    4.63      also have "\<dots> < sum (\<lambda>i::'n. ?s) UNIV"
    4.64        by (rule sum_strict_mono, simp_all add: M \<open>M \<le> m\<close> \<open>M \<le> n\<close>)
    4.65      also have "\<dots> = r"
    4.66 @@ -480,7 +480,7 @@
    4.67  instantiation vec :: (real_normed_vector, finite) real_normed_vector
    4.68  begin
    4.69  
    4.70 -definition "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV"
    4.71 +definition "norm x = L2_set (\<lambda>i. norm (x$i)) UNIV"
    4.72  
    4.73  definition "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
    4.74  
    4.75 @@ -488,15 +488,15 @@
    4.76    fix a :: real and x y :: "'a ^ 'b"
    4.77    show "norm x = 0 \<longleftrightarrow> x = 0"
    4.78      unfolding norm_vec_def
    4.79 -    by (simp add: setL2_eq_0_iff vec_eq_iff)
    4.80 +    by (simp add: L2_set_eq_0_iff vec_eq_iff)
    4.81    show "norm (x + y) \<le> norm x + norm y"
    4.82      unfolding norm_vec_def
    4.83 -    apply (rule order_trans [OF _ setL2_triangle_ineq])
    4.84 -    apply (simp add: setL2_mono norm_triangle_ineq)
    4.85 +    apply (rule order_trans [OF _ L2_set_triangle_ineq])
    4.86 +    apply (simp add: L2_set_mono norm_triangle_ineq)
    4.87      done
    4.88    show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
    4.89      unfolding norm_vec_def
    4.90 -    by (simp add: setL2_right_distrib)
    4.91 +    by (simp add: L2_set_right_distrib)
    4.92    show "sgn x = scaleR (inverse (norm x)) x"
    4.93      by (rule sgn_vec_def)
    4.94    show "dist x y = norm (x - y)"
    4.95 @@ -508,7 +508,7 @@
    4.96  
    4.97  lemma norm_nth_le: "norm (x $ i) \<le> norm x"
    4.98  unfolding norm_vec_def
    4.99 -by (rule member_le_setL2) simp_all
   4.100 +by (rule member_le_L2_set) simp_all
   4.101  
   4.102  lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
   4.103  apply standard
   4.104 @@ -545,7 +545,7 @@
   4.105      unfolding inner_vec_def
   4.106      by (simp add: vec_eq_iff sum_nonneg_eq_0_iff)
   4.107    show "norm x = sqrt (inner x x)"
   4.108 -    unfolding inner_vec_def norm_vec_def setL2_def
   4.109 +    unfolding inner_vec_def norm_vec_def L2_set_def
   4.110      by (simp add: power2_norm_eq_inner)
   4.111  qed
   4.112  
     5.1 --- a/src/HOL/Analysis/L2_Norm.thy	Thu Dec 07 11:14:32 2017 +0100
     5.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Thu Dec 07 15:48:50 2017 +0100
     5.3 @@ -8,74 +8,73 @@
     5.4  imports Complex_Main
     5.5  begin
     5.6  
     5.7 -definition
     5.8 -  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
     5.9 +definition "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
    5.10  
    5.11 -lemma setL2_cong:
    5.12 -  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
    5.13 -  unfolding setL2_def by simp
    5.14 +lemma L2_set_cong:
    5.15 +  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
    5.16 +  unfolding L2_set_def by simp
    5.17  
    5.18 -lemma strong_setL2_cong:
    5.19 -  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
    5.20 -  unfolding setL2_def simp_implies_def by simp
    5.21 +lemma strong_L2_set_cong:
    5.22 +  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
    5.23 +  unfolding L2_set_def simp_implies_def by simp
    5.24  
    5.25 -lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
    5.26 -  unfolding setL2_def by simp
    5.27 +lemma L2_set_infinite [simp]: "\<not> finite A \<Longrightarrow> L2_set f A = 0"
    5.28 +  unfolding L2_set_def by simp
    5.29  
    5.30 -lemma setL2_empty [simp]: "setL2 f {} = 0"
    5.31 -  unfolding setL2_def by simp
    5.32 +lemma L2_set_empty [simp]: "L2_set f {} = 0"
    5.33 +  unfolding L2_set_def by simp
    5.34  
    5.35 -lemma setL2_insert [simp]:
    5.36 +lemma L2_set_insert [simp]:
    5.37    "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
    5.38 -    setL2 f (insert a F) = sqrt ((f a)\<^sup>2 + (setL2 f F)\<^sup>2)"
    5.39 -  unfolding setL2_def by (simp add: sum_nonneg)
    5.40 +    L2_set f (insert a F) = sqrt ((f a)\<^sup>2 + (L2_set f F)\<^sup>2)"
    5.41 +  unfolding L2_set_def by (simp add: sum_nonneg)
    5.42  
    5.43 -lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
    5.44 -  unfolding setL2_def by (simp add: sum_nonneg)
    5.45 +lemma L2_set_nonneg [simp]: "0 \<le> L2_set f A"
    5.46 +  unfolding L2_set_def by (simp add: sum_nonneg)
    5.47  
    5.48 -lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
    5.49 -  unfolding setL2_def by simp
    5.50 +lemma L2_set_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> L2_set f A = 0"
    5.51 +  unfolding L2_set_def by simp
    5.52  
    5.53 -lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
    5.54 -  unfolding setL2_def by (simp add: real_sqrt_mult)
    5.55 +lemma L2_set_constant: "L2_set (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
    5.56 +  unfolding L2_set_def by (simp add: real_sqrt_mult)
    5.57  
    5.58 -lemma setL2_mono:
    5.59 +lemma L2_set_mono:
    5.60    assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
    5.61    assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
    5.62 -  shows "setL2 f K \<le> setL2 g K"
    5.63 -  unfolding setL2_def
    5.64 +  shows "L2_set f K \<le> L2_set g K"
    5.65 +  unfolding L2_set_def
    5.66    by (simp add: sum_nonneg sum_mono power_mono assms)
    5.67  
    5.68 -lemma setL2_strict_mono:
    5.69 +lemma L2_set_strict_mono:
    5.70    assumes "finite K" and "K \<noteq> {}"
    5.71    assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
    5.72    assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
    5.73 -  shows "setL2 f K < setL2 g K"
    5.74 -  unfolding setL2_def
    5.75 +  shows "L2_set f K < L2_set g K"
    5.76 +  unfolding L2_set_def
    5.77    by (simp add: sum_strict_mono power_strict_mono assms)
    5.78  
    5.79 -lemma setL2_right_distrib:
    5.80 -  "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
    5.81 -  unfolding setL2_def
    5.82 +lemma L2_set_right_distrib:
    5.83 +  "0 \<le> r \<Longrightarrow> r * L2_set f A = L2_set (\<lambda>x. r * f x) A"
    5.84 +  unfolding L2_set_def
    5.85    apply (simp add: power_mult_distrib)
    5.86    apply (simp add: sum_distrib_left [symmetric])
    5.87    apply (simp add: real_sqrt_mult sum_nonneg)
    5.88    done
    5.89  
    5.90 -lemma setL2_left_distrib:
    5.91 -  "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
    5.92 -  unfolding setL2_def
    5.93 +lemma L2_set_left_distrib:
    5.94 +  "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A"
    5.95 +  unfolding L2_set_def
    5.96    apply (simp add: power_mult_distrib)
    5.97    apply (simp add: sum_distrib_right [symmetric])
    5.98    apply (simp add: real_sqrt_mult sum_nonneg)
    5.99    done
   5.100  
   5.101 -lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
   5.102 -  unfolding setL2_def
   5.103 +lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
   5.104 +  unfolding L2_set_def
   5.105    by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
   5.106  
   5.107 -lemma setL2_triangle_ineq:
   5.108 -  shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
   5.109 +lemma L2_set_triangle_ineq:
   5.110 +  shows "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
   5.111  proof (cases "finite A")
   5.112    case False
   5.113    thus ?thesis by simp
   5.114 @@ -87,12 +86,12 @@
   5.115      show ?case by simp
   5.116    next
   5.117      case (insert x F)
   5.118 -    hence "sqrt ((f x + g x)\<^sup>2 + (setL2 (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
   5.119 -           sqrt ((f x + g x)\<^sup>2 + (setL2 f F + setL2 g F)\<^sup>2)"
   5.120 +    hence "sqrt ((f x + g x)\<^sup>2 + (L2_set (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
   5.121 +           sqrt ((f x + g x)\<^sup>2 + (L2_set f F + L2_set g F)\<^sup>2)"
   5.122        by (intro real_sqrt_le_mono add_left_mono power_mono insert
   5.123 -                setL2_nonneg add_increasing zero_le_power2)
   5.124 +                L2_set_nonneg add_increasing zero_le_power2)
   5.125      also have
   5.126 -      "\<dots> \<le> sqrt ((f x)\<^sup>2 + (setL2 f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (setL2 g F)\<^sup>2)"
   5.127 +      "\<dots> \<le> sqrt ((f x)\<^sup>2 + (L2_set f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (L2_set g F)\<^sup>2)"
   5.128        by (rule real_sqrt_sum_squares_triangle_ineq)
   5.129      finally show ?case
   5.130        using insert by simp
   5.131 @@ -106,8 +105,8 @@
   5.132    apply simp
   5.133    done
   5.134  
   5.135 -lemma setL2_le_sum [rule_format]:
   5.136 -  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> sum f A"
   5.137 +lemma L2_set_le_sum [rule_format]:
   5.138 +  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
   5.139    apply (cases "finite A")
   5.140    apply (induct set: finite)
   5.141    apply simp
   5.142 @@ -124,7 +123,7 @@
   5.143    apply simp
   5.144    done
   5.145  
   5.146 -lemma setL2_le_sum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
   5.147 +lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
   5.148    apply (cases "finite A")
   5.149    apply (induct set: finite)
   5.150    apply simp
   5.151 @@ -134,7 +133,7 @@
   5.152    apply simp
   5.153    done
   5.154  
   5.155 -lemma setL2_mult_ineq_lemma:
   5.156 +lemma L2_set_mult_ineq_lemma:
   5.157    fixes a b c d :: real
   5.158    shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
   5.159  proof -
   5.160 @@ -147,7 +146,7 @@
   5.161      by simp
   5.162  qed
   5.163  
   5.164 -lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
   5.165 +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"
   5.166    apply (cases "finite A")
   5.167    apply (induct set: finite)
   5.168    apply simp
   5.169 @@ -160,12 +159,12 @@
   5.170    apply (simp add: power_mult_distrib)
   5.171    apply (simp add: distrib_left distrib_right)
   5.172    apply (rule ord_le_eq_trans)
   5.173 -  apply (rule setL2_mult_ineq_lemma)
   5.174 +  apply (rule L2_set_mult_ineq_lemma)
   5.175    apply simp_all
   5.176    done
   5.177  
   5.178 -lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
   5.179 -  unfolding setL2_def
   5.180 +lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A"
   5.181 +  unfolding L2_set_def
   5.182    by (auto intro!: member_le_sum real_le_rsqrt)
   5.183  
   5.184  end
     6.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Dec 07 11:14:32 2017 +0100
     6.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Dec 07 15:48:50 2017 +0100
     6.3 @@ -1249,8 +1249,8 @@
     6.4  
     6.5  lemma euclidean_dist_l2:
     6.6    fixes x y :: "'a :: euclidean_space"
     6.7 -  shows "dist x y = setL2 (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
     6.8 -  unfolding dist_norm norm_eq_sqrt_inner setL2_def
     6.9 +  shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
    6.10 +  unfolding dist_norm norm_eq_sqrt_inner L2_set_def
    6.11    by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
    6.12  
    6.13  lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
    6.14 @@ -1358,7 +1358,7 @@
    6.15      fix y :: 'a
    6.16      assume *: "y \<in> box ?a ?b"
    6.17      have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
    6.18 -      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
    6.19 +      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
    6.20      also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
    6.21      proof (rule real_sqrt_less_mono, rule sum_strict_mono)
    6.22        fix i :: "'a"
    6.23 @@ -1460,7 +1460,7 @@
    6.24      fix y :: 'a
    6.25      assume *: "y \<in> cbox ?a ?b"
    6.26      have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
    6.27 -      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
    6.28 +      unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2)
    6.29      also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
    6.30      proof (rule real_sqrt_less_mono, rule sum_strict_mono)
    6.31        fix i :: "'a"
    6.32 @@ -4579,7 +4579,7 @@
    6.33        have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
    6.34          apply (subst euclidean_dist_l2)
    6.35          using zero_le_dist
    6.36 -        apply (rule setL2_le_sum)
    6.37 +        apply (rule L2_set_le_sum)
    6.38          done
    6.39        also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
    6.40          apply (rule sum_strict_mono)