equal
deleted
inserted
replaced
353 have q: "seminorm E p" |
353 have q: "seminorm E p" |
354 proof |
354 proof |
355 fix x y a assume x: "x \<in> E" and y: "y \<in> E" |
355 fix x y a assume x: "x \<in> E" and y: "y \<in> E" |
356 |
356 |
357 txt {* @{text p} is positive definite: *} |
357 txt {* @{text p} is positive definite: *} |
358 show "0 \<le> p x" |
358 have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero) |
359 proof (unfold p_def, rule real_le_mult_order1a) |
359 moreover from x have "0 \<le> \<parallel>x\<parallel>" .. |
360 show "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero) |
360 ultimately show "0 \<le> p x" |
361 from x show "0 \<le> \<parallel>x\<parallel>" .. |
361 by (simp add: p_def zero_le_mult_iff) |
362 qed |
|
363 |
362 |
364 txt {* @{text p} is absolutely homogenous: *} |
363 txt {* @{text p} is absolutely homogenous: *} |
365 |
364 |
366 show "p (a \<cdot> x) = \<bar>a\<bar> * p x" |
365 show "p (a \<cdot> x) = \<bar>a\<bar> * p x" |
367 proof - |
366 proof - |
375 txt {* Furthermore, @{text p} is subadditive: *} |
374 txt {* Furthermore, @{text p} is subadditive: *} |
376 |
375 |
377 show "p (x + y) \<le> p x + p y" |
376 show "p (x + y) \<le> p x + p y" |
378 proof - |
377 proof - |
379 have "p (x + y) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel>" by (simp only: p_def) |
378 have "p (x + y) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel>" by (simp only: p_def) |
380 also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)" |
379 also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero) |
381 proof (rule real_mult_le_le_mono1a) |
380 from x y have "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" .. |
382 show "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero) |
381 with a have " \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)" |
383 from x y show "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" .. |
382 by (simp add: mult_left_mono) |
384 qed |
|
385 also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: right_distrib) |
383 also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: right_distrib) |
386 also have "\<dots> = p x + p y" by (simp only: p_def) |
384 also have "\<dots> = p x + p y" by (simp only: p_def) |
387 finally show ?thesis . |
385 finally show ?thesis . |
388 qed |
386 qed |
389 qed |
387 qed |