src/HOL/Analysis/L2_Norm.thy
 author wenzelm Sat Nov 04 19:17:19 2017 +0100 (20 months ago) changeset 67006 b1278ed3cd46 parent 66453 cc19f7ca2ed6 child 67143 db609ac2c307 permissions -rw-r--r--
prefer main entry points of HOL;
 hoelzl@63627 ` 1` ```(* Title: HOL/Analysis/L2_Norm.thy ``` huffman@36333 ` 2` ``` Author: Brian Huffman, Portland State University ``` huffman@36333 ` 3` ```*) ``` huffman@36333 ` 4` wenzelm@60420 ` 5` ```section \Square root of sum of squares\ ``` huffman@36333 ` 6` huffman@36333 ` 7` ```theory L2_Norm ``` wenzelm@67006 ` 8` ```imports Complex_Main ``` huffman@36333 ` 9` ```begin ``` huffman@36333 ` 10` huffman@36333 ` 11` ```definition ``` wenzelm@53015 ` 12` ``` "setL2 f A = sqrt (\i\A. (f i)\<^sup>2)" ``` huffman@36333 ` 13` huffman@36333 ` 14` ```lemma setL2_cong: ``` huffman@36333 ` 15` ``` "\A = B; \x. x \ B \ f x = g x\ \ setL2 f A = setL2 g B" ``` huffman@36333 ` 16` ``` unfolding setL2_def by simp ``` huffman@36333 ` 17` huffman@36333 ` 18` ```lemma strong_setL2_cong: ``` huffman@36333 ` 19` ``` "\A = B; \x. x \ B =simp=> f x = g x\ \ setL2 f A = setL2 g B" ``` huffman@36333 ` 20` ``` unfolding setL2_def simp_implies_def by simp ``` huffman@36333 ` 21` huffman@36333 ` 22` ```lemma setL2_infinite [simp]: "\ finite A \ setL2 f A = 0" ``` huffman@36333 ` 23` ``` unfolding setL2_def by simp ``` huffman@36333 ` 24` huffman@36333 ` 25` ```lemma setL2_empty [simp]: "setL2 f {} = 0" ``` huffman@36333 ` 26` ``` unfolding setL2_def by simp ``` huffman@36333 ` 27` huffman@36333 ` 28` ```lemma setL2_insert [simp]: ``` huffman@36333 ` 29` ``` "\finite F; a \ F\ \ ``` wenzelm@53015 ` 30` ``` setL2 f (insert a F) = sqrt ((f a)\<^sup>2 + (setL2 f F)\<^sup>2)" ``` nipkow@64267 ` 31` ``` unfolding setL2_def by (simp add: sum_nonneg) ``` huffman@36333 ` 32` huffman@36333 ` 33` ```lemma setL2_nonneg [simp]: "0 \ setL2 f A" ``` nipkow@64267 ` 34` ``` unfolding setL2_def by (simp add: sum_nonneg) ``` huffman@36333 ` 35` huffman@36333 ` 36` ```lemma setL2_0': "\a\A. f a = 0 \ setL2 f A = 0" ``` huffman@36333 ` 37` ``` unfolding setL2_def by simp ``` huffman@36333 ` 38` huffman@36333 ` 39` ```lemma setL2_constant: "setL2 (\x. y) A = sqrt (of_nat (card A)) * \y\" ``` huffman@36333 ` 40` ``` unfolding setL2_def by (simp add: real_sqrt_mult) ``` huffman@36333 ` 41` huffman@36333 ` 42` ```lemma setL2_mono: ``` huffman@36333 ` 43` ``` assumes "\i. i \ K \ f i \ g i" ``` huffman@36333 ` 44` ``` assumes "\i. i \ K \ 0 \ f i" ``` huffman@36333 ` 45` ``` shows "setL2 f K \ setL2 g K" ``` huffman@36333 ` 46` ``` unfolding setL2_def ``` nipkow@64267 ` 47` ``` by (simp add: sum_nonneg sum_mono power_mono assms) ``` huffman@36333 ` 48` huffman@36333 ` 49` ```lemma setL2_strict_mono: ``` huffman@36333 ` 50` ``` assumes "finite K" and "K \ {}" ``` huffman@36333 ` 51` ``` assumes "\i. i \ K \ f i < g i" ``` huffman@36333 ` 52` ``` assumes "\i. i \ K \ 0 \ f i" ``` huffman@36333 ` 53` ``` shows "setL2 f K < setL2 g K" ``` huffman@36333 ` 54` ``` unfolding setL2_def ``` nipkow@64267 ` 55` ``` by (simp add: sum_strict_mono power_strict_mono assms) ``` huffman@36333 ` 56` huffman@36333 ` 57` ```lemma setL2_right_distrib: ``` huffman@36333 ` 58` ``` "0 \ r \ r * setL2 f A = setL2 (\x. r * f x) A" ``` huffman@36333 ` 59` ``` unfolding setL2_def ``` huffman@36333 ` 60` ``` apply (simp add: power_mult_distrib) ``` nipkow@64267 ` 61` ``` apply (simp add: sum_distrib_left [symmetric]) ``` nipkow@64267 ` 62` ``` apply (simp add: real_sqrt_mult sum_nonneg) ``` huffman@36333 ` 63` ``` done ``` huffman@36333 ` 64` huffman@36333 ` 65` ```lemma setL2_left_distrib: ``` huffman@36333 ` 66` ``` "0 \ r \ setL2 f A * r = setL2 (\x. f x * r) A" ``` huffman@36333 ` 67` ``` unfolding setL2_def ``` huffman@36333 ` 68` ``` apply (simp add: power_mult_distrib) ``` nipkow@64267 ` 69` ``` apply (simp add: sum_distrib_right [symmetric]) ``` nipkow@64267 ` 70` ``` apply (simp add: real_sqrt_mult sum_nonneg) ``` huffman@36333 ` 71` ``` done ``` huffman@36333 ` 72` huffman@36333 ` 73` ```lemma setL2_eq_0_iff: "finite A \ setL2 f A = 0 \ (\x\A. f x = 0)" ``` huffman@36333 ` 74` ``` unfolding setL2_def ``` nipkow@64267 ` 75` ``` by (simp add: sum_nonneg sum_nonneg_eq_0_iff) ``` huffman@36333 ` 76` huffman@36333 ` 77` ```lemma setL2_triangle_ineq: ``` huffman@36333 ` 78` ``` shows "setL2 (\i. f i + g i) A \ setL2 f A + setL2 g A" ``` huffman@36333 ` 79` ```proof (cases "finite A") ``` huffman@36333 ` 80` ``` case False ``` huffman@36333 ` 81` ``` thus ?thesis by simp ``` huffman@36333 ` 82` ```next ``` huffman@36333 ` 83` ``` case True ``` huffman@36333 ` 84` ``` thus ?thesis ``` huffman@36333 ` 85` ``` proof (induct set: finite) ``` huffman@36333 ` 86` ``` case empty ``` huffman@36333 ` 87` ``` show ?case by simp ``` huffman@36333 ` 88` ``` next ``` huffman@36333 ` 89` ``` case (insert x F) ``` wenzelm@53015 ` 90` ``` hence "sqrt ((f x + g x)\<^sup>2 + (setL2 (\i. f i + g i) F)\<^sup>2) \ ``` wenzelm@53015 ` 91` ``` sqrt ((f x + g x)\<^sup>2 + (setL2 f F + setL2 g F)\<^sup>2)" ``` huffman@36333 ` 92` ``` by (intro real_sqrt_le_mono add_left_mono power_mono insert ``` huffman@36333 ` 93` ``` setL2_nonneg add_increasing zero_le_power2) ``` huffman@36333 ` 94` ``` also have ``` wenzelm@53015 ` 95` ``` "\ \ sqrt ((f x)\<^sup>2 + (setL2 f F)\<^sup>2) + sqrt ((g x)\<^sup>2 + (setL2 g F)\<^sup>2)" ``` huffman@36333 ` 96` ``` by (rule real_sqrt_sum_squares_triangle_ineq) ``` huffman@36333 ` 97` ``` finally show ?case ``` huffman@36333 ` 98` ``` using insert by simp ``` huffman@36333 ` 99` ``` qed ``` huffman@36333 ` 100` ```qed ``` huffman@36333 ` 101` huffman@36333 ` 102` ```lemma sqrt_sum_squares_le_sum: ``` wenzelm@53015 ` 103` ``` "\0 \ x; 0 \ y\ \ sqrt (x\<^sup>2 + y\<^sup>2) \ x + y" ``` huffman@36333 ` 104` ``` apply (rule power2_le_imp_le) ``` nipkow@56536 ` 105` ``` apply (simp add: power2_sum) ``` huffman@44142 ` 106` ``` apply simp ``` huffman@36333 ` 107` ``` done ``` huffman@36333 ` 108` nipkow@64267 ` 109` ```lemma setL2_le_sum [rule_format]: ``` nipkow@64267 ` 110` ``` "(\i\A. 0 \ f i) \ setL2 f A \ sum f A" ``` huffman@36333 ` 111` ``` apply (cases "finite A") ``` huffman@36333 ` 112` ``` apply (induct set: finite) ``` huffman@36333 ` 113` ``` apply simp ``` huffman@36333 ` 114` ``` apply clarsimp ``` huffman@36333 ` 115` ``` apply (erule order_trans [OF sqrt_sum_squares_le_sum]) ``` huffman@36333 ` 116` ``` apply simp ``` huffman@36333 ` 117` ``` apply simp ``` huffman@36333 ` 118` ``` apply simp ``` huffman@36333 ` 119` ``` done ``` huffman@36333 ` 120` wenzelm@53015 ` 121` ```lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \ \x\ + \y\" ``` huffman@36333 ` 122` ``` apply (rule power2_le_imp_le) ``` nipkow@56536 ` 123` ``` apply (simp add: power2_sum) ``` huffman@44142 ` 124` ``` apply simp ``` huffman@36333 ` 125` ``` done ``` huffman@36333 ` 126` nipkow@64267 ` 127` ```lemma setL2_le_sum_abs: "setL2 f A \ (\i\A. \f i\)" ``` huffman@36333 ` 128` ``` apply (cases "finite A") ``` huffman@36333 ` 129` ``` apply (induct set: finite) ``` huffman@36333 ` 130` ``` apply simp ``` huffman@36333 ` 131` ``` apply simp ``` huffman@36333 ` 132` ``` apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs]) ``` huffman@36333 ` 133` ``` apply simp ``` huffman@36333 ` 134` ``` apply simp ``` huffman@36333 ` 135` ``` done ``` huffman@36333 ` 136` huffman@36333 ` 137` ```lemma setL2_mult_ineq_lemma: ``` huffman@36333 ` 138` ``` fixes a b c d :: real ``` wenzelm@53015 ` 139` ``` shows "2 * (a * c) * (b * d) \ a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2" ``` huffman@36333 ` 140` ```proof - ``` wenzelm@53015 ` 141` ``` have "0 \ (a * d - b * c)\<^sup>2" by simp ``` wenzelm@53015 ` 142` ``` also have "\ = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * d) * (b * c)" ``` huffman@36333 ` 143` ``` by (simp only: power2_diff power_mult_distrib) ``` wenzelm@53015 ` 144` ``` also have "\ = a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2 - 2 * (a * c) * (b * d)" ``` huffman@36333 ` 145` ``` by simp ``` wenzelm@53015 ` 146` ``` finally show "2 * (a * c) * (b * d) \ a\<^sup>2 * d\<^sup>2 + b\<^sup>2 * c\<^sup>2" ``` huffman@36333 ` 147` ``` by simp ``` huffman@36333 ` 148` ```qed ``` huffman@36333 ` 149` huffman@36333 ` 150` ```lemma setL2_mult_ineq: "(\i\A. \f i\ * \g i\) \ setL2 f A * setL2 g A" ``` huffman@36333 ` 151` ``` apply (cases "finite A") ``` huffman@36333 ` 152` ``` apply (induct set: finite) ``` huffman@36333 ` 153` ``` apply simp ``` huffman@36333 ` 154` ``` apply (rule power2_le_imp_le, simp) ``` huffman@36333 ` 155` ``` apply (rule order_trans) ``` huffman@36333 ` 156` ``` apply (rule power_mono) ``` huffman@36333 ` 157` ``` apply (erule add_left_mono) ``` nipkow@64267 ` 158` ``` apply (simp add: sum_nonneg) ``` huffman@36333 ` 159` ``` apply (simp add: power2_sum) ``` huffman@36333 ` 160` ``` apply (simp add: power_mult_distrib) ``` webertj@49962 ` 161` ``` apply (simp add: distrib_left distrib_right) ``` huffman@36333 ` 162` ``` apply (rule ord_le_eq_trans) ``` huffman@36333 ` 163` ``` apply (rule setL2_mult_ineq_lemma) ``` nipkow@56536 ` 164` ``` apply simp_all ``` huffman@36333 ` 165` ``` done ``` huffman@36333 ` 166` huffman@36333 ` 167` ```lemma member_le_setL2: "\finite A; i \ A\ \ f i \ setL2 f A" ``` lp15@63938 ` 168` ``` unfolding setL2_def ``` nipkow@64267 ` 169` ``` by (auto intro!: member_le_sum real_le_rsqrt) ``` huffman@36333 ` 170` huffman@36333 ` 171` ```end ```