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