author | wenzelm |
Fri, 12 Apr 2019 22:09:25 +0200 | |
changeset 70136 | f03a01a18c6e |
parent 69676 | 56acd449da41 |
permissions | -rw-r--r-- |
63627 | 1 |
(* Title: HOL/Analysis/L2_Norm.thy |
36333 | 2 |
Author: Brian Huffman, Portland State University |
3 |
*) |
|
4 |
||
69676 | 5 |
chapter \<open>Linear Algebra\<close> |
36333 | 6 |
|
7 |
theory L2_Norm |
|
67006 | 8 |
imports Complex_Main |
36333 | 9 |
begin |
10 |
||
69676 | 11 |
section \<open>L2 Norm\<close> |
12 |
||
70136 | 13 |
definition\<^marker>\<open>tag important\<close> L2_set :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> real" where |
69600 | 14 |
"L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)" |
36333 | 15 |
|
67155 | 16 |
lemma L2_set_cong: |
17 |
"\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B" |
|
18 |
unfolding L2_set_def by simp |
|
36333 | 19 |
|
69546
27dae626822b
prefer naming convention from datatype package for strong congruence rules
haftmann
parents:
69164
diff
changeset
|
20 |
lemma L2_set_cong_simp: |
67155 | 21 |
"\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B" |
22 |
unfolding L2_set_def simp_implies_def by simp |
|
36333 | 23 |
|
67155 | 24 |
lemma L2_set_infinite [simp]: "\<not> finite A \<Longrightarrow> L2_set f A = 0" |
25 |
unfolding L2_set_def by simp |
|
26 |
||
27 |
lemma L2_set_empty [simp]: "L2_set f {} = 0" |
|
28 |
unfolding L2_set_def by simp |
|
36333 | 29 |
|
67155 | 30 |
lemma L2_set_insert [simp]: |
31 |
"\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow> |
|
32 |
L2_set f (insert a F) = sqrt ((f a)\<^sup>2 + (L2_set f F)\<^sup>2)" |
|
33 |
unfolding L2_set_def by (simp add: sum_nonneg) |
|
36333 | 34 |
|
67155 | 35 |
lemma L2_set_nonneg [simp]: "0 \<le> L2_set f A" |
36 |
unfolding L2_set_def by (simp add: sum_nonneg) |
|
36333 | 37 |
|
67155 | 38 |
lemma L2_set_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> L2_set f A = 0" |
39 |
unfolding L2_set_def by simp |
|
36333 | 40 |
|
67155 | 41 |
lemma L2_set_constant: "L2_set (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>" |
42 |
unfolding L2_set_def by (simp add: real_sqrt_mult) |
|
36333 | 43 |
|
67155 | 44 |
lemma L2_set_mono: |
36333 | 45 |
assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i" |
46 |
assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i" |
|
67155 | 47 |
shows "L2_set f K \<le> L2_set g K" |
48 |
unfolding L2_set_def |
|
64267 | 49 |
by (simp add: sum_nonneg sum_mono power_mono assms) |
36333 | 50 |
|
67155 | 51 |
lemma L2_set_strict_mono: |
36333 | 52 |
assumes "finite K" and "K \<noteq> {}" |
53 |
assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i" |
|
54 |
assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i" |
|
67155 | 55 |
shows "L2_set f K < L2_set g K" |
56 |
unfolding L2_set_def |
|
64267 | 57 |
by (simp add: sum_strict_mono power_strict_mono assms) |
36333 | 58 |
|
67155 | 59 |
lemma L2_set_right_distrib: |
60 |
"0 \<le> r \<Longrightarrow> r * L2_set f A = L2_set (\<lambda>x. r * f x) A" |
|
61 |
unfolding L2_set_def |
|
36333 | 62 |
apply (simp add: power_mult_distrib) |
64267 | 63 |
apply (simp add: sum_distrib_left [symmetric]) |
64 |
apply (simp add: real_sqrt_mult sum_nonneg) |
|
36333 | 65 |
done |
66 |
||
67155 | 67 |
lemma L2_set_left_distrib: |
68 |
"0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A" |
|
69 |
unfolding L2_set_def |
|
36333 | 70 |
apply (simp add: power_mult_distrib) |
64267 | 71 |
apply (simp add: sum_distrib_right [symmetric]) |
72 |
apply (simp add: real_sqrt_mult sum_nonneg) |
|
36333 | 73 |
done |
74 |
||
67155 | 75 |
lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" |
76 |
unfolding L2_set_def |
|
64267 | 77 |
by (simp add: sum_nonneg sum_nonneg_eq_0_iff) |
36333 | 78 |
|
68607
67bb59e49834
make theorem, corollary, and proposition %important for HOL-Analysis manual
immler
parents:
68465
diff
changeset
|
79 |
proposition L2_set_triangle_ineq: |
67156 | 80 |
"L2_set (\<lambda>i. f i + g i) A \<le> L2_set f A + L2_set g A" |
68607
67bb59e49834
make theorem, corollary, and proposition %important for HOL-Analysis manual
immler
parents:
68465
diff
changeset
|
81 |
proof (cases "finite A") |
36333 | 82 |
case False |
83 |
thus ?thesis by simp |
|
84 |
next |
|
85 |
case True |
|
86 |
thus ?thesis |
|
87 |
proof (induct set: finite) |
|
88 |
case empty |
|
89 |
show ?case by simp |
|
90 |
next |
|
91 |
case (insert x F) |
|
67155 | 92 |
hence "sqrt ((f x + g x)\<^sup>2 + (L2_set (\<lambda>i. f i + g i) F)\<^sup>2) \<le> |
93 |
sqrt ((f x + g x)\<^sup>2 + (L2_set f F + L2_set g F)\<^sup>2)" |
|
36333 | 94 |
by (intro real_sqrt_le_mono add_left_mono power_mono insert |
67155 | 95 |
L2_set_nonneg add_increasing zero_le_power2) |
36333 | 96 |
also have |
67155 | 97 |
"\<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 | 98 |
by (rule real_sqrt_sum_squares_triangle_ineq) |
99 |
finally show ?case |
|
100 |
using insert by simp |
|
101 |
qed |
|
102 |
qed |
|
103 |
||
67155 | 104 |
lemma L2_set_le_sum [rule_format]: |
105 |
"(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A" |
|
36333 | 106 |
apply (cases "finite A") |
107 |
apply (induct set: finite) |
|
108 |
apply simp |
|
109 |
apply clarsimp |
|
110 |
apply (erule order_trans [OF sqrt_sum_squares_le_sum]) |
|
111 |
apply simp |
|
112 |
apply simp |
|
113 |
apply simp |
|
114 |
done |
|
115 |
||
67155 | 116 |
lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)" |
36333 | 117 |
apply (cases "finite A") |
118 |
apply (induct set: finite) |
|
119 |
apply simp |
|
120 |
apply simp |
|
121 |
apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs]) |
|
122 |
apply simp |
|
123 |
apply simp |
|
124 |
done |
|
125 |
||
67155 | 126 |
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 | 127 |
apply (cases "finite A") |
128 |
apply (induct set: finite) |
|
129 |
apply simp |
|
130 |
apply (rule power2_le_imp_le, simp) |
|
131 |
apply (rule order_trans) |
|
132 |
apply (rule power_mono) |
|
133 |
apply (erule add_left_mono) |
|
64267 | 134 |
apply (simp add: sum_nonneg) |
36333 | 135 |
apply (simp add: power2_sum) |
136 |
apply (simp add: power_mult_distrib) |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44142
diff
changeset
|
137 |
apply (simp add: distrib_left distrib_right) |
36333 | 138 |
apply (rule ord_le_eq_trans) |
67155 | 139 |
apply (rule L2_set_mult_ineq_lemma) |
56536 | 140 |
apply simp_all |
36333 | 141 |
done |
142 |
||
67155 | 143 |
lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A" |
144 |
unfolding L2_set_def |
|
64267 | 145 |
by (auto intro!: member_le_sum real_le_rsqrt) |
36333 | 146 |
|
147 |
end |