199 proof - |
199 proof - |
200 have "graph H h \<subseteq> graph H' h'" |
200 have "graph H h \<subseteq> graph H' h'" |
201 proof (rule graph_extI) |
201 proof (rule graph_extI) |
202 fix t assume "t \<in> H" |
202 fix t assume "t \<in> H" |
203 have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) |
203 have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) |
204 = (t, #0)" |
204 = (t, Numeral0)" |
205 by (rule decomp_H'_H) (assumption+, rule x') |
205 by (rule decomp_H'_H) (assumption+, rule x') |
206 thus "h t = h' t" by (simp! add: Let_def) |
206 thus "h t = h' t" by (simp! add: Let_def) |
207 next |
207 next |
208 show "H \<subseteq> H'" |
208 show "H \<subseteq> H'" |
209 proof (rule subspace_subset) |
209 proof (rule subspace_subset) |
253 |
253 |
254 show "graph F f \<subseteq> graph H' h'" |
254 show "graph F f \<subseteq> graph H' h'" |
255 proof (rule graph_extI) |
255 proof (rule graph_extI) |
256 fix x assume "x \<in> F" |
256 fix x assume "x \<in> F" |
257 have "f x = h x" .. |
257 have "f x = h x" .. |
258 also have " ... = h x + #0 * xi" by simp |
258 also have " ... = h x + Numeral0 * xi" by simp |
259 also |
259 also |
260 have "... = (let (y, a) = (x, #0) in h y + a * xi)" |
260 have "... = (let (y, a) = (x, Numeral0) in h y + a * xi)" |
261 by (simp add: Let_def) |
261 by (simp add: Let_def) |
262 also have |
262 also have |
263 "(x, #0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)" |
263 "(x, Numeral0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)" |
264 by (rule decomp_H'_H [symmetric]) (simp! add: x')+ |
264 by (rule decomp_H'_H [symmetric]) (simp! add: x')+ |
265 also have |
265 also have |
266 "(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) |
266 "(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) |
267 in h y + a * xi) = h' x" by (simp!) |
267 in h y + a * xi) = h' x" by (simp!) |
268 finally show "f x = h' x" . |
268 finally show "f x = h' x" . |
370 proof |
370 proof |
371 fix x y a assume "x \<in> E" "y \<in> E" |
371 fix x y a assume "x \<in> E" "y \<in> E" |
372 |
372 |
373 txt {* @{text p} is positive definite: *} |
373 txt {* @{text p} is positive definite: *} |
374 |
374 |
375 show "#0 \<le> p x" |
375 show "Numeral0 \<le> p x" |
376 proof (unfold p_def, rule real_le_mult_order1a) |
376 proof (unfold p_def, rule real_le_mult_order1a) |
377 from f_cont f_norm show "#0 \<le> \<parallel>f\<parallel>F,norm" .. |
377 from f_cont f_norm show "Numeral0 \<le> \<parallel>f\<parallel>F,norm" .. |
378 show "#0 \<le> norm x" .. |
378 show "Numeral0 \<le> norm x" .. |
379 qed |
379 qed |
380 |
380 |
381 txt {* @{text p} is absolutely homogenous: *} |
381 txt {* @{text p} is absolutely homogenous: *} |
382 |
382 |
383 show "p (a \<cdot> x) = \<bar>a\<bar> * p x" |
383 show "p (a \<cdot> x) = \<bar>a\<bar> * p x" |
400 have "p (x + y) = \<parallel>f\<parallel>F,norm * norm (x + y)" |
400 have "p (x + y) = \<parallel>f\<parallel>F,norm * norm (x + y)" |
401 by (simp!) |
401 by (simp!) |
402 also |
402 also |
403 have "... \<le> \<parallel>f\<parallel>F,norm * (norm x + norm y)" |
403 have "... \<le> \<parallel>f\<parallel>F,norm * (norm x + norm y)" |
404 proof (rule real_mult_le_le_mono1a) |
404 proof (rule real_mult_le_le_mono1a) |
405 from f_cont f_norm show "#0 \<le> \<parallel>f\<parallel>F,norm" .. |
405 from f_cont f_norm show "Numeral0 \<le> \<parallel>f\<parallel>F,norm" .. |
406 show "norm (x + y) \<le> norm x + norm y" .. |
406 show "norm (x + y) \<le> norm x + norm y" .. |
407 qed |
407 qed |
408 also have "... = \<parallel>f\<parallel>F,norm * norm x |
408 also have "... = \<parallel>f\<parallel>F,norm * norm x |
409 + \<parallel>f\<parallel>F,norm * norm y" |
409 + \<parallel>f\<parallel>F,norm * norm y" |
410 by (simp! only: real_add_mult_distrib2) |
410 by (simp! only: real_add_mult_distrib2) |