author | eberlm <eberlm@in.tum.de> |
Sat, 04 Aug 2018 01:03:39 +0200 | |
changeset 68721 | 53ad5c01be3f |
parent 68607 | 67bb59e49834 |
child 69164 | 74f1b0f10b2b |
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 |
|
68607
67bb59e49834
make theorem, corollary, and proposition %important for HOL-Analysis manual
immler
parents:
68465
diff
changeset
|
76 |
proposition L2_set_triangle_ineq: |
67156 | 77 |
"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
|
78 |
proof (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 |
||
67155 | 113 |
lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)" |
36333 | 114 |
apply (cases "finite A") |
115 |
apply (induct set: finite) |
|
116 |
apply simp |
|
117 |
apply simp |
|
118 |
apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs]) |
|
119 |
apply simp |
|
120 |
apply simp |
|
121 |
done |
|
122 |
||
67155 | 123 |
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 | 124 |
apply (cases "finite A") |
125 |
apply (induct set: finite) |
|
126 |
apply simp |
|
127 |
apply (rule power2_le_imp_le, simp) |
|
128 |
apply (rule order_trans) |
|
129 |
apply (rule power_mono) |
|
130 |
apply (erule add_left_mono) |
|
64267 | 131 |
apply (simp add: sum_nonneg) |
36333 | 132 |
apply (simp add: power2_sum) |
133 |
apply (simp add: power_mult_distrib) |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44142
diff
changeset
|
134 |
apply (simp add: distrib_left distrib_right) |
36333 | 135 |
apply (rule ord_le_eq_trans) |
67155 | 136 |
apply (rule L2_set_mult_ineq_lemma) |
56536 | 137 |
apply simp_all |
36333 | 138 |
done |
139 |
||
67155 | 140 |
lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A" |
141 |
unfolding L2_set_def |
|
64267 | 142 |
by (auto intro!: member_le_sum real_le_rsqrt) |
36333 | 143 |
|
144 |
end |