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.85    apply (simp add: power_mult_distrib)
    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.96    apply (simp add: power_mult_distrib)
    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.123 -                setL2_nonneg add_increasing zero_le_power2)
   1.124 +                L2_set_nonneg add_increasing zero_le_power2)
   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.170    apply (simp add: power_mult_distrib)
   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