41959

1 
(* Title: HOL/Multivariate_Analysis/L2_Norm.thy

36333

2 
Author: Brian Huffman, Portland State University


3 
*)


4 


5 
header {* Square root of sum of squares *}


6 


7 
theory L2_Norm


8 
imports NthRoot


9 
begin


10 


11 
definition


12 
"setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"


13 


14 
lemma setL2_cong:


15 
"\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"


16 
unfolding setL2_def by simp


17 


18 
lemma strong_setL2_cong:


19 
"\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"


20 
unfolding setL2_def simp_implies_def by simp


21 


22 
lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"


23 
unfolding setL2_def by simp


24 


25 
lemma setL2_empty [simp]: "setL2 f {} = 0"


26 
unfolding setL2_def by simp


27 


28 
lemma setL2_insert [simp]:


29 
"\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>


30 
setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)"


31 
unfolding setL2_def by (simp add: setsum_nonneg)


32 


33 
lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"


34 
unfolding setL2_def by (simp add: setsum_nonneg)


35 


36 
lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"


37 
unfolding setL2_def by simp


38 


39 
lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"


40 
unfolding setL2_def by (simp add: real_sqrt_mult)


41 


42 
lemma setL2_mono:


43 
assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"


44 
assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"


45 
shows "setL2 f K \<le> setL2 g K"


46 
unfolding setL2_def

41891

47 
by (simp add: setsum_nonneg setsum_mono power_mono assms)

36333

48 


49 
lemma setL2_strict_mono:


50 
assumes "finite K" and "K \<noteq> {}"


51 
assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"


52 
assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"


53 
shows "setL2 f K < setL2 g K"


54 
unfolding setL2_def


55 
by (simp add: setsum_strict_mono power_strict_mono assms)


56 


57 
lemma setL2_right_distrib:


58 
"0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"


59 
unfolding setL2_def


60 
apply (simp add: power_mult_distrib)


61 
apply (simp add: setsum_right_distrib [symmetric])


62 
apply (simp add: real_sqrt_mult setsum_nonneg)


63 
done


64 


65 
lemma setL2_left_distrib:


66 
"0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"


67 
unfolding setL2_def


68 
apply (simp add: power_mult_distrib)


69 
apply (simp add: setsum_left_distrib [symmetric])


70 
apply (simp add: real_sqrt_mult setsum_nonneg)


71 
done


72 


73 
lemma setsum_nonneg_eq_0_iff:


74 
fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"


75 
shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"


76 
apply (induct set: finite, simp)


77 
apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)


78 
done


79 


80 
lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"


81 
unfolding setL2_def


82 
by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)


83 


84 
lemma setL2_triangle_ineq:


85 
shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"


86 
proof (cases "finite A")


87 
case False


88 
thus ?thesis by simp


89 
next


90 
case True


91 
thus ?thesis


92 
proof (induct set: finite)


93 
case empty


94 
show ?case by simp


95 
next


96 
case (insert x F)


97 
hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le>


98 
sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)"


99 
by (intro real_sqrt_le_mono add_left_mono power_mono insert


100 
setL2_nonneg add_increasing zero_le_power2)


101 
also have


102 
"\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)"


103 
by (rule real_sqrt_sum_squares_triangle_ineq)


104 
finally show ?case


105 
using insert by simp


106 
qed


107 
qed


108 


109 
lemma sqrt_sum_squares_le_sum:


110 
"\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"


111 
apply (rule power2_le_imp_le)

44142

112 
apply (simp add: power2_sum mult_nonneg_nonneg)


113 
apply simp

36333

114 
done


115 


116 
lemma setL2_le_setsum [rule_format]:


117 
"(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A"


118 
apply (cases "finite A")


119 
apply (induct set: finite)


120 
apply simp


121 
apply clarsimp


122 
apply (erule order_trans [OF sqrt_sum_squares_le_sum])


123 
apply simp


124 
apply simp


125 
apply simp


126 
done


127 


128 
lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"


129 
apply (rule power2_le_imp_le)

44142

130 
apply (simp add: power2_sum mult_nonneg_nonneg)


131 
apply simp

36333

132 
done


133 


134 
lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"


135 
apply (cases "finite A")


136 
apply (induct set: finite)


137 
apply simp


138 
apply simp


139 
apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])


140 
apply simp


141 
apply simp


142 
done


143 


144 
lemma setL2_mult_ineq_lemma:


145 
fixes a b c d :: real


146 
shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"


147 
proof 


148 
have "0 \<le> (a * d  b * c)\<twosuperior>" by simp


149 
also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>  2 * (a * d) * (b * c)"


150 
by (simp only: power2_diff power_mult_distrib)


151 
also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>  2 * (a * c) * (b * d)"


152 
by simp


153 
finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"


154 
by simp


155 
qed


156 


157 
lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"


158 
apply (cases "finite A")


159 
apply (induct set: finite)


160 
apply simp


161 
apply (rule power2_le_imp_le, simp)


162 
apply (rule order_trans)


163 
apply (rule power_mono)


164 
apply (erule add_left_mono)

44142

165 
apply (simp add: mult_nonneg_nonneg setsum_nonneg)

36333

166 
apply (simp add: power2_sum)


167 
apply (simp add: power_mult_distrib)


168 
apply (simp add: right_distrib left_distrib)


169 
apply (rule ord_le_eq_trans)


170 
apply (rule setL2_mult_ineq_lemma)


171 
apply simp


172 
apply (intro mult_nonneg_nonneg setL2_nonneg)


173 
apply simp


174 
done


175 


176 
lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"


177 
apply (rule_tac s="insert i (A  {i})" and t="A" in subst)


178 
apply fast


179 
apply (subst setL2_insert)


180 
apply simp


181 
apply simp


182 
apply simp


183 
done


184 


185 
end
