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