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