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