59 fixes a b c d :: "'a::ab_group_add" |
59 fixes a b c d :: "'a::ab_group_add" |
60 shows "(a + c) - (b + d) = (a - b) + (c - d)" |
60 shows "(a + c) - (b + d) = (a - b) + (c - d)" |
61 by simp |
61 by simp |
62 |
62 |
63 lemma bounded_linear_add: |
63 lemma bounded_linear_add: |
64 includes bounded_linear f |
64 assumes "bounded_linear f" |
65 includes bounded_linear g |
65 assumes "bounded_linear g" |
66 shows "bounded_linear (\<lambda>x. f x + g x)" |
66 shows "bounded_linear (\<lambda>x. f x + g x)" |
67 apply (unfold_locales) |
67 proof - |
68 apply (simp only: f.add g.add add_ac) |
68 interpret f: bounded_linear [f] by fact |
69 apply (simp only: f.scaleR g.scaleR scaleR_right_distrib) |
69 interpret g: bounded_linear [g] by fact |
70 apply (rule f.pos_bounded [THEN exE], rename_tac Kf) |
70 show ?thesis apply (unfold_locales) |
71 apply (rule g.pos_bounded [THEN exE], rename_tac Kg) |
71 apply (simp only: f.add g.add add_ac) |
72 apply (rule_tac x="Kf + Kg" in exI, safe) |
72 apply (simp only: f.scaleR g.scaleR scaleR_right_distrib) |
73 apply (subst right_distrib) |
73 apply (rule f.pos_bounded [THEN exE], rename_tac Kf) |
74 apply (rule order_trans [OF norm_triangle_ineq]) |
74 apply (rule g.pos_bounded [THEN exE], rename_tac Kg) |
75 apply (rule add_mono, erule spec, erule spec) |
75 apply (rule_tac x="Kf + Kg" in exI, safe) |
76 done |
76 apply (subst right_distrib) |
|
77 apply (rule order_trans [OF norm_triangle_ineq]) |
|
78 apply (rule add_mono, erule spec, erule spec) |
|
79 done |
|
80 qed |
77 |
81 |
78 lemma norm_ratio_ineq: |
82 lemma norm_ratio_ineq: |
79 fixes x y :: "'a::real_normed_vector" |
83 fixes x y :: "'a::real_normed_vector" |
80 fixes h :: "'b::real_normed_vector" |
84 fixes h :: "'b::real_normed_vector" |
81 shows "norm (x + y) / norm h \<le> norm x / norm h + norm y / norm h" |
85 shows "norm (x + y) / norm h \<le> norm x / norm h + norm y / norm h" |
115 qed |
119 qed |
116 |
120 |
117 subsection {* Subtraction *} |
121 subsection {* Subtraction *} |
118 |
122 |
119 lemma bounded_linear_minus: |
123 lemma bounded_linear_minus: |
120 includes bounded_linear f |
124 assumes "bounded_linear f" |
121 shows "bounded_linear (\<lambda>x. - f x)" |
125 shows "bounded_linear (\<lambda>x. - f x)" |
122 apply (unfold_locales) |
126 proof - |
123 apply (simp add: f.add) |
127 interpret f: bounded_linear [f] by fact |
124 apply (simp add: f.scaleR) |
128 show ?thesis apply (unfold_locales) |
125 apply (simp add: f.bounded) |
129 apply (simp add: f.add) |
126 done |
130 apply (simp add: f.scaleR) |
|
131 apply (simp add: f.bounded) |
|
132 done |
|
133 qed |
127 |
134 |
128 lemma FDERIV_minus: |
135 lemma FDERIV_minus: |
129 "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)" |
136 "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)" |
130 apply (rule FDERIV_I) |
137 apply (rule FDERIV_I) |
131 apply (rule bounded_linear_minus) |
138 apply (rule bounded_linear_minus) |
167 fixes a b c :: real |
174 fixes a b c :: real |
168 shows "(b = 0 \<Longrightarrow> a = 0) \<Longrightarrow> (a / b) * (b / c) = a / c" |
175 shows "(b = 0 \<Longrightarrow> a = 0) \<Longrightarrow> (a / b) * (b / c) = a / c" |
169 by simp |
176 by simp |
170 |
177 |
171 lemma bounded_linear_compose: |
178 lemma bounded_linear_compose: |
172 includes bounded_linear f |
179 assumes "bounded_linear f" |
173 includes bounded_linear g |
180 assumes "bounded_linear g" |
174 shows "bounded_linear (\<lambda>x. f (g x))" |
181 shows "bounded_linear (\<lambda>x. f (g x))" |
175 proof (unfold_locales) |
182 proof - |
176 fix x y show "f (g (x + y)) = f (g x) + f (g y)" |
183 interpret f: bounded_linear [f] by fact |
177 by (simp only: f.add g.add) |
184 interpret g: bounded_linear [g] by fact |
178 next |
185 show ?thesis proof (unfold_locales) |
179 fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))" |
186 fix x y show "f (g (x + y)) = f (g x) + f (g y)" |
180 by (simp only: f.scaleR g.scaleR) |
187 by (simp only: f.add g.add) |
181 next |
188 next |
182 from f.pos_bounded |
189 fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))" |
183 obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast |
190 by (simp only: f.scaleR g.scaleR) |
184 from g.pos_bounded |
191 next |
185 obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast |
192 from f.pos_bounded |
186 show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K" |
193 obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast |
187 proof (intro exI allI) |
194 from g.pos_bounded |
188 fix x |
195 obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast |
189 have "norm (f (g x)) \<le> norm (g x) * Kf" |
196 show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K" |
190 using f . |
197 proof (intro exI allI) |
191 also have "\<dots> \<le> (norm x * Kg) * Kf" |
198 fix x |
192 using g Kf [THEN order_less_imp_le] by (rule mult_right_mono) |
199 have "norm (f (g x)) \<le> norm (g x) * Kf" |
193 also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)" |
200 using f . |
194 by (rule mult_assoc) |
201 also have "\<dots> \<le> (norm x * Kg) * Kf" |
195 finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" . |
202 using g Kf [THEN order_less_imp_le] by (rule mult_right_mono) |
|
203 also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)" |
|
204 by (rule mult_assoc) |
|
205 finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" . |
|
206 qed |
196 qed |
207 qed |
197 qed |
208 qed |
198 |
209 |
199 lemma FDERIV_compose: |
210 lemma FDERIV_compose: |
200 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
211 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |