src/HOL/Analysis/L2_Norm.thy
 changeset 67155 9e5b05d54f9d parent 67144 cef9a1514ed0 child 67156 3a9966b88a50
```     1.1 --- a/src/HOL/Analysis/L2_Norm.thy	Wed Dec 06 16:01:15 2017 +0100
1.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Thu Dec 07 15:48:50 2017 +0100
1.3 @@ -8,74 +8,73 @@
1.4  imports Complex_Main
1.5  begin
1.6
1.7 -definition
1.8 -  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
1.9 +definition "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
1.10
1.11 -lemma setL2_cong:
1.12 -  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
1.13 -  unfolding setL2_def by simp
1.14 +lemma L2_set_cong:
1.15 +  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
1.16 +  unfolding L2_set_def by simp
1.17
1.18 -lemma strong_setL2_cong:
1.19 -  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
1.20 -  unfolding setL2_def simp_implies_def by simp
1.21 +lemma strong_L2_set_cong:
1.22 +  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
1.23 +  unfolding L2_set_def simp_implies_def by simp
1.24
1.25 -lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
1.26 -  unfolding setL2_def by simp
1.27 +lemma L2_set_infinite [simp]: "\<not> finite A \<Longrightarrow> L2_set f A = 0"
1.28 +  unfolding L2_set_def by simp
1.29
1.30 -lemma setL2_empty [simp]: "setL2 f {} = 0"
1.31 -  unfolding setL2_def by simp
1.32 +lemma L2_set_empty [simp]: "L2_set f {} = 0"
1.33 +  unfolding L2_set_def by simp
1.34
1.35 -lemma setL2_insert [simp]:
1.36 +lemma L2_set_insert [simp]:
1.37    "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
1.38 -    setL2 f (insert a F) = sqrt ((f a)\<^sup>2 + (setL2 f F)\<^sup>2)"
1.39 -  unfolding setL2_def by (simp add: sum_nonneg)
1.40 +    L2_set f (insert a F) = sqrt ((f a)\<^sup>2 + (L2_set f F)\<^sup>2)"
1.41 +  unfolding L2_set_def by (simp add: sum_nonneg)
1.42
1.43 -lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
1.44 -  unfolding setL2_def by (simp add: sum_nonneg)
1.45 +lemma L2_set_nonneg [simp]: "0 \<le> L2_set f A"
1.46 +  unfolding L2_set_def by (simp add: sum_nonneg)
1.47
1.48 -lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
1.49 -  unfolding setL2_def by simp
1.50 +lemma L2_set_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> L2_set f A = 0"
1.51 +  unfolding L2_set_def by simp
1.52
1.53 -lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
1.54 -  unfolding setL2_def by (simp add: real_sqrt_mult)
1.55 +lemma L2_set_constant: "L2_set (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
1.56 +  unfolding L2_set_def by (simp add: real_sqrt_mult)
1.57
1.58 -lemma setL2_mono:
1.59 +lemma L2_set_mono:
1.60    assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
1.61    assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
1.62 -  shows "setL2 f K \<le> setL2 g K"
1.63 -  unfolding setL2_def
1.64 +  shows "L2_set f K \<le> L2_set g K"
1.65 +  unfolding L2_set_def
1.66    by (simp add: sum_nonneg sum_mono power_mono assms)
1.67
1.68 -lemma setL2_strict_mono:
1.69 +lemma L2_set_strict_mono:
1.70    assumes "finite K" and "K \<noteq> {}"
1.71    assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
1.72    assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
1.73 -  shows "setL2 f K < setL2 g K"
1.74 -  unfolding setL2_def
1.75 +  shows "L2_set f K < L2_set g K"
1.76 +  unfolding L2_set_def
1.77    by (simp add: sum_strict_mono power_strict_mono assms)
1.78
1.79 -lemma setL2_right_distrib:
1.80 -  "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
1.81 -  unfolding setL2_def
1.82 +lemma L2_set_right_distrib:
1.83 +  "0 \<le> r \<Longrightarrow> r * L2_set f A = L2_set (\<lambda>x. r * f x) A"
1.84 +  unfolding L2_set_def
1.86    apply (simp add: sum_distrib_left [symmetric])
1.87    apply (simp add: real_sqrt_mult sum_nonneg)
1.88    done
1.89
1.90 -lemma setL2_left_distrib:
1.91 -  "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
1.92 -  unfolding setL2_def
1.93 +lemma L2_set_left_distrib:
1.94 +  "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A"
1.95 +  unfolding L2_set_def
1.97    apply (simp add: sum_distrib_right [symmetric])
1.98    apply (simp add: real_sqrt_mult sum_nonneg)
1.99    done
1.100
1.101 -lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
1.102 -  unfolding setL2_def
1.103 +lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
1.104 +  unfolding L2_set_def
1.105    by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
1.106
1.107 -lemma setL2_triangle_ineq:
1.108 -  shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
1.109 +lemma L2_set_triangle_ineq:
1.110 +  shows "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
1.111  proof (cases "finite A")
1.112    case False
1.113    thus ?thesis by simp
1.114 @@ -87,12 +86,12 @@
1.115      show ?case by simp
1.116    next
1.117      case (insert x F)
1.118 -    hence "sqrt ((f x + g x)\<^sup>2 + (setL2 (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
1.119 -           sqrt ((f x + g x)\<^sup>2 + (setL2 f F + setL2 g F)\<^sup>2)"
1.120 +    hence "sqrt ((f x + g x)\<^sup>2 + (L2_set (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
1.121 +           sqrt ((f x + g x)\<^sup>2 + (L2_set f F + L2_set g F)\<^sup>2)"
1.122        by (intro real_sqrt_le_mono add_left_mono power_mono insert
1.125      also have
1.126 -      "\<dots> \<le> sqrt ((f x)\<^sup>2 + (setL2 f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (setL2 g F)\<^sup>2)"
1.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)"
1.128        by (rule real_sqrt_sum_squares_triangle_ineq)
1.129      finally show ?case
1.130        using insert by simp
1.131 @@ -106,8 +105,8 @@
1.132    apply simp
1.133    done
1.134
1.135 -lemma setL2_le_sum [rule_format]:
1.136 -  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> sum f A"
1.137 +lemma L2_set_le_sum [rule_format]:
1.138 +  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
1.139    apply (cases "finite A")
1.140    apply (induct set: finite)
1.141    apply simp
1.142 @@ -124,7 +123,7 @@
1.143    apply simp
1.144    done
1.145
1.146 -lemma setL2_le_sum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
1.147 +lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
1.148    apply (cases "finite A")
1.149    apply (induct set: finite)
1.150    apply simp
1.151 @@ -134,7 +133,7 @@
1.152    apply simp
1.153    done
1.154
1.155 -lemma setL2_mult_ineq_lemma:
1.156 +lemma L2_set_mult_ineq_lemma:
1.157    fixes a b c d :: real
1.158    shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
1.159  proof -
1.160 @@ -147,7 +146,7 @@
1.161      by simp
1.162  qed
1.163
1.164 -lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
1.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"
1.166    apply (cases "finite A")
1.167    apply (induct set: finite)
1.168    apply simp
1.169 @@ -160,12 +159,12 @@
1.171    apply (simp add: distrib_left distrib_right)
1.172    apply (rule ord_le_eq_trans)
1.173 -  apply (rule setL2_mult_ineq_lemma)
1.174 +  apply (rule L2_set_mult_ineq_lemma)
1.175    apply simp_all
1.176    done
1.177
1.178 -lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
1.179 -  unfolding setL2_def
1.180 +lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A"
1.181 +  unfolding L2_set_def
1.182    by (auto intro!: member_le_sum real_le_rsqrt)
1.183
1.184  end
```