64 apply (simp add: real_sqrt_mult sum_nonneg) |
64 apply (simp add: real_sqrt_mult sum_nonneg) |
65 done |
65 done |
66 |
66 |
67 lemma L2_set_left_distrib: |
67 lemma L2_set_left_distrib: |
68 "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A" |
68 "0 \<le> r \<Longrightarrow> L2_set f A * r = L2_set (\<lambda>x. f x * r) A" |
69 unfolding L2_set_def |
69 unfolding L2_set_def power_mult_distrib |
70 apply (simp add: power_mult_distrib) |
70 by (simp add: real_sqrt_mult sum_nonneg flip: sum_distrib_right) |
71 apply (simp add: sum_distrib_right [symmetric]) |
|
72 apply (simp add: real_sqrt_mult sum_nonneg) |
|
73 done |
|
74 |
71 |
75 lemma L2_set_eq_0_iff: "finite A \<Longrightarrow> L2_set f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" |
72 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 |
73 unfolding L2_set_def |
77 by (simp add: sum_nonneg sum_nonneg_eq_0_iff) |
74 by (simp add: sum_nonneg sum_nonneg_eq_0_iff) |
78 |
75 |
99 finally show ?case |
96 finally show ?case |
100 using insert by simp |
97 using insert by simp |
101 qed |
98 qed |
102 qed |
99 qed |
103 |
100 |
104 lemma L2_set_le_sum [rule_format]: |
101 lemma L2_set_le_sum: |
105 "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A" |
102 "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> L2_set f A \<le> sum f A" |
106 apply (cases "finite A") |
103 proof (induction A rule: infinite_finite_induct) |
107 apply (induct set: finite) |
104 case (insert a A) |
108 apply simp |
105 with order_trans [OF sqrt_sum_squares_le_sum] show ?case by force |
109 apply clarsimp |
106 qed auto |
110 apply (erule order_trans [OF sqrt_sum_squares_le_sum]) |
|
111 apply simp |
|
112 apply simp |
|
113 apply simp |
|
114 done |
|
115 |
107 |
116 lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)" |
108 lemma L2_set_le_sum_abs: "L2_set f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)" |
117 apply (cases "finite A") |
109 proof (induction A rule: infinite_finite_induct) |
118 apply (induct set: finite) |
110 case (insert a A) |
119 apply simp |
111 with order_trans [OF sqrt_sum_squares_le_sum_abs] show ?case by force |
120 apply simp |
112 qed auto |
121 apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs]) |
|
122 apply simp |
|
123 apply simp |
|
124 done |
|
125 |
113 |
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" |
114 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" |
127 apply (cases "finite A") |
115 proof (induction A rule: infinite_finite_induct) |
128 apply (induct set: finite) |
116 case (insert a A) |
129 apply simp |
117 have "(\<bar>f a\<bar> * \<bar>g a\<bar> + (\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>))\<^sup>2 |
130 apply (rule power2_le_imp_le, simp) |
118 \<le> (\<bar>f a\<bar> * \<bar>g a\<bar> + L2_set f A * L2_set g A)\<^sup>2" |
131 apply (rule order_trans) |
119 by (simp add: insert.IH sum_nonneg) |
132 apply (rule power_mono) |
120 also have "... \<le> ((f a)\<^sup>2 + (L2_set f A)\<^sup>2) * ((g a)\<^sup>2 + (L2_set g A)\<^sup>2)" |
133 apply (erule add_left_mono) |
121 using L2_set_mult_ineq_lemma [of "L2_set f A" "L2_set g A" "\<bar>f a\<bar>" "\<bar>g a\<bar>"] |
134 apply (simp add: sum_nonneg) |
122 by (simp add: power2_eq_square algebra_simps) |
135 apply (simp add: power2_sum) |
123 also have "... = (sqrt ((f a)\<^sup>2 + (L2_set f A)\<^sup>2) * sqrt ((g a)\<^sup>2 + (L2_set g A)\<^sup>2))\<^sup>2" |
136 apply (simp add: power_mult_distrib) |
124 using real_sqrt_mult real_sqrt_sum_squares_mult_squared_eq by presburger |
137 apply (simp add: distrib_left distrib_right) |
125 finally have "(\<bar>f a\<bar> * \<bar>g a\<bar> + (\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>))\<^sup>2 |
138 apply (rule ord_le_eq_trans) |
126 \<le> (sqrt ((f a)\<^sup>2 + (L2_set f A)\<^sup>2) * sqrt ((g a)\<^sup>2 + (L2_set g A)\<^sup>2))\<^sup>2" . |
139 apply (rule L2_set_mult_ineq_lemma) |
127 then |
140 apply simp_all |
128 show ?case |
141 done |
129 using power2_le_imp_le insert.hyps by fastforce |
|
130 qed auto |
142 |
131 |
143 lemma member_le_L2_set: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> L2_set f A" |
132 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 |
133 unfolding L2_set_def |
145 by (auto intro!: member_le_sum real_le_rsqrt) |
134 by (auto intro!: member_le_sum real_le_rsqrt) |
146 |
135 |