author | immler |
Thu, 22 Feb 2018 15:17:25 +0100 | |
changeset 67685 | bdff8bf0a75b |
parent 67156 | 3a9966b88a50 |
child 68465 | e699ca8e22b7 |
permissions | -rw-r--r-- |
63627 | 1 |
(* Title: HOL/Analysis/L2_Norm.thy |
36333 | 2 |
Author: Brian Huffman, Portland State University |
3 |
*) |
|
4 |
||
67143 | 5 |
section \<open>L2 Norm\<close> |
36333 | 6 |
|
7 |
theory L2_Norm |
|
67006 | 8 |
imports Complex_Main |
36333 | 9 |
begin |
10 |
||
67156 | 11 |
definition %important "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)" |
36333 | 12 |
|
67155 | 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 |
|
36333 | 16 |
|
67155 | 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 |
|
36333 | 20 |
|
67155 | 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 |
|
36333 | 26 |
|
67155 | 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) |
|
36333 | 31 |
|
67155 | 32 |
lemma L2_set_nonneg [simp]: "0 \<le> L2_set f A" |
33 |
unfolding L2_set_def by (simp add: sum_nonneg) |
|
36333 | 34 |
|
67155 | 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 |
|
36333 | 37 |
|
67155 | 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) |
|
36333 | 40 |
|
67155 | 41 |
lemma L2_set_mono: |
36333 | 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" |
|
67155 | 44 |
shows "L2_set f K \<le> L2_set g K" |
45 |
unfolding L2_set_def |
|
64267 | 46 |
by (simp add: sum_nonneg sum_mono power_mono assms) |
36333 | 47 |
|
67155 | 48 |
lemma L2_set_strict_mono: |
36333 | 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" |
|
67155 | 52 |
shows "L2_set f K < L2_set g K" |
53 |
unfolding L2_set_def |
|
64267 | 54 |
by (simp add: sum_strict_mono power_strict_mono assms) |
36333 | 55 |
|
67155 | 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 |
|
36333 | 59 |
apply (simp add: power_mult_distrib) |
64267 | 60 |
apply (simp add: sum_distrib_left [symmetric]) |
61 |
apply (simp add: real_sqrt_mult sum_nonneg) |
|
36333 | 62 |
done |
63 |
||
67155 | 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 |
|
36333 | 67 |
apply (simp add: power_mult_distrib) |
64267 | 68 |
apply (simp add: sum_distrib_right [symmetric]) |
69 |
apply (simp add: real_sqrt_mult sum_nonneg) |
|
36333 | 70 |
done |
71 |
||
67155 | 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 |
|
64267 | 74 |
by (simp add: sum_nonneg sum_nonneg_eq_0_iff) |
36333 | 75 |
|
67156 | 76 |
lemma %important L2_set_triangle_ineq: |
77 |
"L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A" |
|
78 |
proof %unimportant (cases "finite A") |
|
36333 | 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) |
|
67155 | 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)" |
|
36333 | 91 |
by (intro real_sqrt_le_mono add_left_mono power_mono insert |
67155 | 92 |
L2_set_nonneg add_increasing zero_le_power2) |
36333 | 93 |
also have |
67155 | 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)" |
36333 | 95 |
by (rule real_sqrt_sum_squares_triangle_ineq) |
96 |
finally show ?case |
|
97 |
using insert by simp |
|
98 |
qed |
|
99 |
qed |
|
100 |
||
67155 | 101 |
lemma L2_set_le_sum [rule_format]: |
102 |
"(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A" |
|
36333 | 103 |
apply (cases "finite A") |
104 |
apply (induct set: finite) |
|
105 |
apply simp |
|
106 |
apply clarsimp |
|
107 |
apply (erule order_trans [OF sqrt_sum_squares_le_sum]) |
|
108 |
apply simp |
|
109 |
apply simp |
|
110 |
apply simp |
|
111 |
done |
|
112 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49962
diff
changeset
|
113 |
lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \<le> \<bar>x\<bar> + \<bar>y\<bar>" |
36333 | 114 |
apply (rule power2_le_imp_le) |
56536 | 115 |
apply (simp add: power2_sum) |
44142 | 116 |
apply simp |
36333 | 117 |
done |
118 |
||
67155 | 119 |
lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)" |
36333 | 120 |
apply (cases "finite A") |
121 |
apply (induct set: finite) |
|
122 |
apply simp |
|
123 |
apply simp |
|
124 |
apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs]) |
|
125 |
apply simp |
|
126 |
apply simp |
|
127 |
done |
|
128 |
||
67155 | 129 |
lemma L2_set_mult_ineq_lemma: |
36333 | 130 |
fixes a b c d :: real |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49962
diff
changeset
|
131 |
shows "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2" |
36333 | 132 |
proof - |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49962
diff
changeset
|
133 |
have "0 \<le> (a * d - b * c)\<^sup>2" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49962
diff
changeset
|
134 |
also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * d) * (b * c)" |
36333 | 135 |
by (simp only: power2_diff power_mult_distrib) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49962
diff
changeset
|
136 |
also have "\<dots> = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * c) * (b * d)" |
36333 | 137 |
by simp |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49962
diff
changeset
|
138 |
finally show "2 * (a * c) * (b * d) \<le> a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2" |
36333 | 139 |
by simp |
140 |
qed |
|
141 |
||
67155 | 142 |
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" |
36333 | 143 |
apply (cases "finite A") |
144 |
apply (induct set: finite) |
|
145 |
apply simp |
|
146 |
apply (rule power2_le_imp_le, simp) |
|
147 |
apply (rule order_trans) |
|
148 |
apply (rule power_mono) |
|
149 |
apply (erule add_left_mono) |
|
64267 | 150 |
apply (simp add: sum_nonneg) |
36333 | 151 |
apply (simp add: power2_sum) |
152 |
apply (simp add: power_mult_distrib) |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44142
diff
changeset
|
153 |
apply (simp add: distrib_left distrib_right) |
36333 | 154 |
apply (rule ord_le_eq_trans) |
67155 | 155 |
apply (rule L2_set_mult_ineq_lemma) |
56536 | 156 |
apply simp_all |
36333 | 157 |
done |
158 |
||
67155 | 159 |
lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A" |
160 |
unfolding L2_set_def |
|
64267 | 161 |
by (auto intro!: member_le_sum real_le_rsqrt) |
36333 | 162 |
|
163 |
end |