src/HOL/Analysis/L2_Norm.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 months ago) changeset 69981 3dced198b9ec parent 69676 56acd449da41 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
```     1 (*  Title:      HOL/Analysis/L2_Norm.thy
```
```     2     Author:     Brian Huffman, Portland State University
```
```     3 *)
```
```     4
```
```     5 chapter \<open>Linear Algebra\<close>
```
```     6
```
```     7 theory L2_Norm
```
```     8 imports Complex_Main
```
```     9 begin
```
```    10
```
```    11 section \<open>L2 Norm\<close>
```
```    12
```
```    13 definition%important L2_set :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> real" where
```
```    14 "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
```
```    15
```
```    16 lemma L2_set_cong:
```
```    17   "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
```
```    18   unfolding L2_set_def by simp
```
```    19
```
```    20 lemma L2_set_cong_simp:
```
```    21   "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
```
```    22   unfolding L2_set_def simp_implies_def by simp
```
```    23
```
```    24 lemma L2_set_infinite [simp]: "\<not> finite A \<Longrightarrow> L2_set f A = 0"
```
```    25   unfolding L2_set_def by simp
```
```    26
```
```    27 lemma L2_set_empty [simp]: "L2_set f {} = 0"
```
```    28   unfolding L2_set_def by simp
```
```    29
```
```    30 lemma L2_set_insert [simp]:
```
```    31   "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
```
```    32     L2_set f (insert a F) = sqrt ((f a)\<^sup>2 + (L2_set f F)\<^sup>2)"
```
```    33   unfolding L2_set_def by (simp add: sum_nonneg)
```
```    34
```
```    35 lemma L2_set_nonneg [simp]: "0 \<le> L2_set f A"
```
```    36   unfolding L2_set_def by (simp add: sum_nonneg)
```
```    37
```
```    38 lemma L2_set_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> L2_set f A = 0"
```
```    39   unfolding L2_set_def by simp
```
```    40
```
```    41 lemma L2_set_constant: "L2_set (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
```
```    42   unfolding L2_set_def by (simp add: real_sqrt_mult)
```
```    43
```
```    44 lemma L2_set_mono:
```
```    45   assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
```
```    46   assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
```
```    47   shows "L2_set f K \<le> L2_set g K"
```
```    48   unfolding L2_set_def
```
```    49   by (simp add: sum_nonneg sum_mono power_mono assms)
```
```    50
```
```    51 lemma L2_set_strict_mono:
```
```    52   assumes "finite K" and "K \<noteq> {}"
```
```    53   assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
```
```    54   assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
```
```    55   shows "L2_set f K < L2_set g K"
```
```    56   unfolding L2_set_def
```
```    57   by (simp add: sum_strict_mono power_strict_mono assms)
```
```    58
```
```    59 lemma L2_set_right_distrib:
```
```    60   "0 \<le> r \<Longrightarrow> r * L2_set f A = L2_set (\<lambda>x. r * f x) A"
```
```    61   unfolding L2_set_def
```
```    62   apply (simp add: power_mult_distrib)
```
```    63   apply (simp add: sum_distrib_left [symmetric])
```
```    64   apply (simp add: real_sqrt_mult sum_nonneg)
```
```    65   done
```
```    66
```
```    67 lemma L2_set_left_distrib:
```
```    68   "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A"
```
```    69   unfolding L2_set_def
```
```    70   apply (simp add: power_mult_distrib)
```
```    71   apply (simp add: sum_distrib_right [symmetric])
```
```    72   apply (simp add: real_sqrt_mult sum_nonneg)
```
```    73   done
```
```    74
```
```    75 lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
```
```    76   unfolding L2_set_def
```
```    77   by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
```
```    78
```
```    79 proposition L2_set_triangle_ineq:
```
```    80   "L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A"
```
```    81 proof (cases "finite A")
```
```    82   case False
```
```    83   thus ?thesis by simp
```
```    84 next
```
```    85   case True
```
```    86   thus ?thesis
```
```    87   proof (induct set: finite)
```
```    88     case empty
```
```    89     show ?case by simp
```
```    90   next
```
```    91     case (insert x F)
```
```    92     hence "sqrt ((f x + g x)\<^sup>2 + (L2_set (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
```
```    93            sqrt ((f x + g x)\<^sup>2 + (L2_set f F + L2_set g F)\<^sup>2)"
```
```    94       by (intro real_sqrt_le_mono add_left_mono power_mono insert
```
```    95                 L2_set_nonneg add_increasing zero_le_power2)
```
```    96     also have
```
```    97       "\<dots> \<le> sqrt ((f x)\<^sup>2 + (L2_set f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (L2_set g F)\<^sup>2)"
```
```    98       by (rule real_sqrt_sum_squares_triangle_ineq)
```
```    99     finally show ?case
```
```   100       using insert by simp
```
```   101   qed
```
```   102 qed
```
```   103
```
```   104 lemma L2_set_le_sum [rule_format]:
```
```   105   "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
```
```   106   apply (cases "finite A")
```
```   107   apply (induct set: finite)
```
```   108   apply simp
```
```   109   apply clarsimp
```
```   110   apply (erule order_trans [OF sqrt_sum_squares_le_sum])
```
```   111   apply simp
```
```   112   apply simp
```
```   113   apply simp
```
```   114   done
```
```   115
```
```   116 lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
```
```   117   apply (cases "finite A")
```
```   118   apply (induct set: finite)
```
```   119   apply simp
```
```   120   apply simp
```
```   121   apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
```
```   122   apply simp
```
```   123   apply simp
```
```   124   done
```
```   125
```
```   126 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"
```
```   127   apply (cases "finite A")
```
```   128   apply (induct set: finite)
```
```   129   apply simp
```
```   130   apply (rule power2_le_imp_le, simp)
```
```   131   apply (rule order_trans)
```
```   132   apply (rule power_mono)
```
```   133   apply (erule add_left_mono)
```
```   134   apply (simp add: sum_nonneg)
```
```   135   apply (simp add: power2_sum)
```
```   136   apply (simp add: power_mult_distrib)
```
```   137   apply (simp add: distrib_left distrib_right)
```
```   138   apply (rule ord_le_eq_trans)
```
```   139   apply (rule L2_set_mult_ineq_lemma)
```
```   140   apply simp_all
```
```   141   done
```
```   142
```
```   143 lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A"
```
```   144   unfolding L2_set_def
```
```   145   by (auto intro!: member_le_sum real_le_rsqrt)
```
```   146
```
```   147 end
```