src/HOL/Multivariate_Analysis/L2_Norm.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 44142 8e27e0177518
child 49962 a8cc904a6820
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 41891
diff changeset
     1
(*  Title:      HOL/Multivariate_Analysis/L2_Norm.thy
36333
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman, Portland State University
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
     3
*)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
     4
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
     5
header {* Square root of sum of squares *}
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
     6
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
     7
theory L2_Norm
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
     8
imports NthRoot
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
     9
begin
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    10
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    11
definition
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    12
  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    13
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    14
lemma setL2_cong:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    15
  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    16
  unfolding setL2_def by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    17
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    18
lemma strong_setL2_cong:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    19
  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    20
  unfolding setL2_def simp_implies_def by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    21
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    22
lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    23
  unfolding setL2_def by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    24
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    25
lemma setL2_empty [simp]: "setL2 f {} = 0"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    26
  unfolding setL2_def by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    27
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    28
lemma setL2_insert [simp]:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    29
  "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    30
    setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    31
  unfolding setL2_def by (simp add: setsum_nonneg)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    32
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    33
lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    34
  unfolding setL2_def by (simp add: setsum_nonneg)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    35
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    36
lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    37
  unfolding setL2_def by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    38
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    39
lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    40
  unfolding setL2_def by (simp add: real_sqrt_mult)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    41
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    42
lemma setL2_mono:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    43
  assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    44
  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    45
  shows "setL2 f K \<le> setL2 g K"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    46
  unfolding setL2_def
41891
d37babdf5cae tuned proofs -- eliminated prems;
wenzelm
parents: 36333
diff changeset
    47
  by (simp add: setsum_nonneg setsum_mono power_mono assms)
36333
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    48
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    49
lemma setL2_strict_mono:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    50
  assumes "finite K" and "K \<noteq> {}"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    51
  assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    52
  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    53
  shows "setL2 f K < setL2 g K"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    54
  unfolding setL2_def
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    55
  by (simp add: setsum_strict_mono power_strict_mono assms)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    56
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    57
lemma setL2_right_distrib:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    58
  "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    59
  unfolding setL2_def
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    60
  apply (simp add: power_mult_distrib)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    61
  apply (simp add: setsum_right_distrib [symmetric])
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    62
  apply (simp add: real_sqrt_mult setsum_nonneg)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    63
  done
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    64
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    65
lemma setL2_left_distrib:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    66
  "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    67
  unfolding setL2_def
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    68
  apply (simp add: power_mult_distrib)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    69
  apply (simp add: setsum_left_distrib [symmetric])
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    70
  apply (simp add: real_sqrt_mult setsum_nonneg)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    71
  done
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    72
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    73
lemma setsum_nonneg_eq_0_iff:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    74
  fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    75
  shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    76
  apply (induct set: finite, simp)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    77
  apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    78
  done
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    79
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    80
lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    81
  unfolding setL2_def
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    82
  by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    83
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    84
lemma setL2_triangle_ineq:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    85
  shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    86
proof (cases "finite A")
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    87
  case False
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    88
  thus ?thesis by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    89
next
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    90
  case True
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    91
  thus ?thesis
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    92
  proof (induct set: finite)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    93
    case empty
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    94
    show ?case by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    95
  next
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    96
    case (insert x F)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    97
    hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le>
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    98
           sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
    99
      by (intro real_sqrt_le_mono add_left_mono power_mono insert
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   100
                setL2_nonneg add_increasing zero_le_power2)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   101
    also have
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   102
      "\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   103
      by (rule real_sqrt_sum_squares_triangle_ineq)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   104
    finally show ?case
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   105
      using insert by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   106
  qed
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   107
qed
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   108
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   109
lemma sqrt_sum_squares_le_sum:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   110
  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   111
  apply (rule power2_le_imp_le)
44142
8e27e0177518 avoid warnings about duplicate rules
huffman
parents: 41959
diff changeset
   112
  apply (simp add: power2_sum mult_nonneg_nonneg)
8e27e0177518 avoid warnings about duplicate rules
huffman
parents: 41959
diff changeset
   113
  apply simp
36333
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   114
  done
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   115
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   116
lemma setL2_le_setsum [rule_format]:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   117
  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   118
  apply (cases "finite A")
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   119
  apply (induct set: finite)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   120
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   121
  apply clarsimp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   122
  apply (erule order_trans [OF sqrt_sum_squares_le_sum])
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   123
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   124
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   125
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   126
  done
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   127
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   128
lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   129
  apply (rule power2_le_imp_le)
44142
8e27e0177518 avoid warnings about duplicate rules
huffman
parents: 41959
diff changeset
   130
  apply (simp add: power2_sum mult_nonneg_nonneg)
8e27e0177518 avoid warnings about duplicate rules
huffman
parents: 41959
diff changeset
   131
  apply simp
36333
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   132
  done
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   133
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   134
lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   135
  apply (cases "finite A")
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   136
  apply (induct set: finite)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   137
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   138
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   139
  apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   140
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   141
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   142
  done
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   143
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   144
lemma setL2_mult_ineq_lemma:
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   145
  fixes a b c d :: real
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   146
  shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   147
proof -
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   148
  have "0 \<le> (a * d - b * c)\<twosuperior>" by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   149
  also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * d) * (b * c)"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   150
    by (simp only: power2_diff power_mult_distrib)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   151
  also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * c) * (b * d)"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   152
    by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   153
  finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   154
    by simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   155
qed
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   156
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   157
lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   158
  apply (cases "finite A")
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   159
  apply (induct set: finite)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   160
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   161
  apply (rule power2_le_imp_le, simp)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   162
  apply (rule order_trans)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   163
  apply (rule power_mono)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   164
  apply (erule add_left_mono)
44142
8e27e0177518 avoid warnings about duplicate rules
huffman
parents: 41959
diff changeset
   165
  apply (simp add: mult_nonneg_nonneg setsum_nonneg)
36333
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   166
  apply (simp add: power2_sum)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   167
  apply (simp add: power_mult_distrib)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   168
  apply (simp add: right_distrib left_distrib)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   169
  apply (rule ord_le_eq_trans)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   170
  apply (rule setL2_mult_ineq_lemma)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   171
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   172
  apply (intro mult_nonneg_nonneg setL2_nonneg)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   173
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   174
  done
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   175
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   176
lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   177
  apply (rule_tac s="insert i (A - {i})" and t="A" in subst)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   178
  apply fast
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   179
  apply (subst setL2_insert)
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   180
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   181
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   182
  apply simp
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   183
  done
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   184
82356c9e218a move l2-norm stuff into separate theory file
huffman
parents:
diff changeset
   185
end