src/HOL/Analysis/L2_Norm.thy
 author wenzelm Sat Nov 04 19:17:19 2017 +0100 (19 months ago) changeset 67006 b1278ed3cd46 parent 66453 cc19f7ca2ed6 child 67143 db609ac2c307 permissions -rw-r--r--
prefer main entry points of HOL;
```     1 (*  Title:      HOL/Analysis/L2_Norm.thy
```
```     2     Author:     Brian Huffman, Portland State University
```
```     3 *)
```
```     4
```
```     5 section \<open>Square root of sum of squares\<close>
```
```     6
```
```     7 theory L2_Norm
```
```     8 imports Complex_Main
```
```     9 begin
```
```    10
```
```    11 definition
```
```    12   "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
```
```    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)\<^sup>2 + (setL2 f F)\<^sup>2)"
```
```    31   unfolding setL2_def by (simp add: sum_nonneg)
```
```    32
```
```    33 lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
```
```    34   unfolding setL2_def by (simp add: sum_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
```
```    47   by (simp add: sum_nonneg sum_mono power_mono assms)
```
```    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: sum_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: sum_distrib_left [symmetric])
```
```    62   apply (simp add: real_sqrt_mult sum_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: sum_distrib_right [symmetric])
```
```    70   apply (simp add: real_sqrt_mult sum_nonneg)
```
```    71   done
```
```    72
```
```    73 lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
```
```    74   unfolding setL2_def
```
```    75   by (simp add: sum_nonneg sum_nonneg_eq_0_iff)
```
```    76
```
```    77 lemma setL2_triangle_ineq:
```
```    78   shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
```
```    79 proof (cases "finite A")
```
```    80   case False
```
```    81   thus ?thesis by simp
```
```    82 next
```
```    83   case True
```
```    84   thus ?thesis
```
```    85   proof (induct set: finite)
```
```    86     case empty
```
```    87     show ?case by simp
```
```    88   next
```
```    89     case (insert x F)
```
```    90     hence "sqrt ((f x + g x)\<^sup>2 + (setL2 (\<lambda>i. f i + g i) F)\<^sup>2) \<le>
```
```    91            sqrt ((f x + g x)\<^sup>2 + (setL2 f F + setL2 g F)\<^sup>2)"
```
```    92       by (intro real_sqrt_le_mono add_left_mono power_mono insert
```
```    93                 setL2_nonneg add_increasing zero_le_power2)
```
```    94     also have
```
```    95       "\<dots> \<le> sqrt ((f x)\<^sup>2 + (setL2 f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (setL2 g F)\<^sup>2)"
```
```    96       by (rule real_sqrt_sum_squares_triangle_ineq)
```
```    97     finally show ?case
```
```    98       using insert by simp
```
```    99   qed
```
```   100 qed
```
```   101
```
```   102 lemma sqrt_sum_squares_le_sum:
```
```   103   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
```
```   104   apply (rule power2_le_imp_le)
```
```   105   apply (simp add: power2_sum)
```
```   106   apply simp
```
```   107   done
```
```   108
```
```   109 lemma setL2_le_sum [rule_format]:
```
```   110   "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> sum f A"
```
```   111   apply (cases "finite A")
```
```   112   apply (induct set: finite)
```
```   113   apply simp
```
```   114   apply clarsimp
```
```   115   apply (erule order_trans [OF sqrt_sum_squares_le_sum])
```
```   116   apply simp
```
```   117   apply simp
```
```   118   apply simp
```
```   119   done
```
```   120
```
```   121 lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
```
```   122   apply (rule power2_le_imp_le)
```
```   123   apply (simp add: power2_sum)
```
```   124   apply simp
```
```   125   done
```
```   126
```
```   127 lemma setL2_le_sum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
```
```   128   apply (cases "finite A")
```
```   129   apply (induct set: finite)
```
```   130   apply simp
```
```   131   apply simp
```
```   132   apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
```
```   133   apply simp
```
```   134   apply simp
```
```   135   done
```
```   136
```
```   137 lemma setL2_mult_ineq_lemma:
```
```   138   fixes a b c d :: real
```
```   139   shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
```
```   140 proof -
```
```   141   have "0 \<le> (a * d - b * c)\<^sup>2" by simp
```
```   142   also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * d) * (b * c)"
```
```   143     by (simp only: power2_diff power_mult_distrib)
```
```   144   also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * c) * (b * d)"
```
```   145     by simp
```
```   146   finally show "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2"
```
```   147     by simp
```
```   148 qed
```
```   149
```
```   150 lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
```
```   151   apply (cases "finite A")
```
```   152   apply (induct set: finite)
```
```   153   apply simp
```
```   154   apply (rule power2_le_imp_le, simp)
```
```   155   apply (rule order_trans)
```
```   156   apply (rule power_mono)
```
```   157   apply (erule add_left_mono)
```
```   158   apply (simp add: sum_nonneg)
```
```   159   apply (simp add: power2_sum)
```
```   160   apply (simp add: power_mult_distrib)
```
```   161   apply (simp add: distrib_left distrib_right)
```
```   162   apply (rule ord_le_eq_trans)
```
```   163   apply (rule setL2_mult_ineq_lemma)
```
```   164   apply simp_all
```
```   165   done
```
```   166
```
```   167 lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
```
```   168   unfolding setL2_def
```
```   169   by (auto intro!: member_le_sum real_le_rsqrt)
```
```   170
```
```   171 end
```