src/HOL/Multivariate_Analysis/L2_Norm.thy
changeset 63627 6ddb43c6b711
parent 63626 44ce6b524ff3
child 63631 2edc8da89edc
child 63633 2accfb71e33b
     1.1 --- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Fri Aug 05 18:34:57 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,176 +0,0 @@
     1.4 -(*  Title:      HOL/Multivariate_Analysis/L2_Norm.thy
     1.5 -    Author:     Brian Huffman, Portland State University
     1.6 -*)
     1.7 -
     1.8 -section \<open>Square root of sum of squares\<close>
     1.9 -
    1.10 -theory L2_Norm
    1.11 -imports NthRoot
    1.12 -begin
    1.13 -
    1.14 -definition
    1.15 -  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
    1.16 -
    1.17 -lemma setL2_cong:
    1.18 -  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
    1.19 -  unfolding setL2_def by simp
    1.20 -
    1.21 -lemma strong_setL2_cong:
    1.22 -  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
    1.23 -  unfolding setL2_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 -
    1.28 -lemma setL2_empty [simp]: "setL2 f {} = 0"
    1.29 -  unfolding setL2_def by simp
    1.30 -
    1.31 -lemma setL2_insert [simp]:
    1.32 -  "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
    1.33 -    setL2 f (insert a F) = sqrt ((f a)\<^sup>2 + (setL2 f F)\<^sup>2)"
    1.34 -  unfolding setL2_def by (simp add: setsum_nonneg)
    1.35 -
    1.36 -lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
    1.37 -  unfolding setL2_def by (simp add: setsum_nonneg)
    1.38 -
    1.39 -lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
    1.40 -  unfolding setL2_def by simp
    1.41 -
    1.42 -lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
    1.43 -  unfolding setL2_def by (simp add: real_sqrt_mult)
    1.44 -
    1.45 -lemma setL2_mono:
    1.46 -  assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
    1.47 -  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
    1.48 -  shows "setL2 f K \<le> setL2 g K"
    1.49 -  unfolding setL2_def
    1.50 -  by (simp add: setsum_nonneg setsum_mono power_mono assms)
    1.51 -
    1.52 -lemma setL2_strict_mono:
    1.53 -  assumes "finite K" and "K \<noteq> {}"
    1.54 -  assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
    1.55 -  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
    1.56 -  shows "setL2 f K < setL2 g K"
    1.57 -  unfolding setL2_def
    1.58 -  by (simp add: setsum_strict_mono power_strict_mono assms)
    1.59 -
    1.60 -lemma setL2_right_distrib:
    1.61 -  "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
    1.62 -  unfolding setL2_def
    1.63 -  apply (simp add: power_mult_distrib)
    1.64 -  apply (simp add: setsum_right_distrib [symmetric])
    1.65 -  apply (simp add: real_sqrt_mult setsum_nonneg)
    1.66 -  done
    1.67 -
    1.68 -lemma setL2_left_distrib:
    1.69 -  "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
    1.70 -  unfolding setL2_def
    1.71 -  apply (simp add: power_mult_distrib)
    1.72 -  apply (simp add: setsum_left_distrib [symmetric])
    1.73 -  apply (simp add: real_sqrt_mult setsum_nonneg)
    1.74 -  done
    1.75 -
    1.76 -lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
    1.77 -  unfolding setL2_def
    1.78 -  by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)
    1.79 -
    1.80 -lemma setL2_triangle_ineq:
    1.81 -  shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
    1.82 -proof (cases "finite A")
    1.83 -  case False
    1.84 -  thus ?thesis by simp
    1.85 -next
    1.86 -  case True
    1.87 -  thus ?thesis
    1.88 -  proof (induct set: finite)
    1.89 -    case empty
    1.90 -    show ?case by simp
    1.91 -  next
    1.92 -    case (insert x F)
    1.93 -    hence "sqrt ((f x + g x)\<^sup>2 + (setL2 (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
    1.94 -           sqrt ((f x + g x)\<^sup>2 + (setL2 f F + setL2 g F)\<^sup>2)"
    1.95 -      by (intro real_sqrt_le_mono add_left_mono power_mono insert
    1.96 -                setL2_nonneg add_increasing zero_le_power2)
    1.97 -    also have
    1.98 -      "\<dots> \<le> sqrt ((f x)\<^sup>2 + (setL2 f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (setL2 g F)\<^sup>2)"
    1.99 -      by (rule real_sqrt_sum_squares_triangle_ineq)
   1.100 -    finally show ?case
   1.101 -      using insert by simp
   1.102 -  qed
   1.103 -qed
   1.104 -
   1.105 -lemma sqrt_sum_squares_le_sum:
   1.106 -  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
   1.107 -  apply (rule power2_le_imp_le)
   1.108 -  apply (simp add: power2_sum)
   1.109 -  apply simp
   1.110 -  done
   1.111 -
   1.112 -lemma setL2_le_setsum [rule_format]:
   1.113 -  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A"
   1.114 -  apply (cases "finite A")
   1.115 -  apply (induct set: finite)
   1.116 -  apply simp
   1.117 -  apply clarsimp
   1.118 -  apply (erule order_trans [OF sqrt_sum_squares_le_sum])
   1.119 -  apply simp
   1.120 -  apply simp
   1.121 -  apply simp
   1.122 -  done
   1.123 -
   1.124 -lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
   1.125 -  apply (rule power2_le_imp_le)
   1.126 -  apply (simp add: power2_sum)
   1.127 -  apply simp
   1.128 -  done
   1.129 -
   1.130 -lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
   1.131 -  apply (cases "finite A")
   1.132 -  apply (induct set: finite)
   1.133 -  apply simp
   1.134 -  apply simp
   1.135 -  apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
   1.136 -  apply simp
   1.137 -  apply simp
   1.138 -  done
   1.139 -
   1.140 -lemma setL2_mult_ineq_lemma:
   1.141 -  fixes a b c d :: real
   1.142 -  shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
   1.143 -proof -
   1.144 -  have "0 \<le> (a * d - b * c)\<^sup>2" by simp
   1.145 -  also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * d) * (b * c)"
   1.146 -    by (simp only: power2_diff power_mult_distrib)
   1.147 -  also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * c) * (b * d)"
   1.148 -    by simp
   1.149 -  finally show "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
   1.150 -    by simp
   1.151 -qed
   1.152 -
   1.153 -lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
   1.154 -  apply (cases "finite A")
   1.155 -  apply (induct set: finite)
   1.156 -  apply simp
   1.157 -  apply (rule power2_le_imp_le, simp)
   1.158 -  apply (rule order_trans)
   1.159 -  apply (rule power_mono)
   1.160 -  apply (erule add_left_mono)
   1.161 -  apply (simp add: setsum_nonneg)
   1.162 -  apply (simp add: power2_sum)
   1.163 -  apply (simp add: power_mult_distrib)
   1.164 -  apply (simp add: distrib_left distrib_right)
   1.165 -  apply (rule ord_le_eq_trans)
   1.166 -  apply (rule setL2_mult_ineq_lemma)
   1.167 -  apply simp_all
   1.168 -  done
   1.169 -
   1.170 -lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
   1.171 -  apply (rule_tac s="insert i (A - {i})" and t="A" in subst)
   1.172 -  apply fast
   1.173 -  apply (subst setL2_insert)
   1.174 -  apply simp
   1.175 -  apply simp
   1.176 -  apply simp
   1.177 -  done
   1.178 -
   1.179 -end