src/HOL/Analysis/Product_Vector.thy
 changeset 67962 0acdcd8f4ba1 parent 67685 bdff8bf0a75b child 68072 493b818e8e10
```     1.1 --- a/src/HOL/Analysis/Product_Vector.thy	Thu Apr 05 06:15:02 2018 +0000
1.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Fri Apr 06 17:34:50 2018 +0200
1.3 @@ -12,7 +12,7 @@
1.4
1.5  subsection \<open>Product is a real vector space\<close>
1.6
1.7 -instantiation prod :: (real_vector, real_vector) real_vector
1.8 +instantiation%important prod :: (real_vector, real_vector) real_vector
1.9  begin
1.10
1.11  definition scaleR_prod_def:
1.12 @@ -46,10 +46,10 @@
1.13
1.14  (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
1.15
1.16 -instantiation prod :: (metric_space, metric_space) dist
1.17 +instantiation%important prod :: (metric_space, metric_space) dist
1.18  begin
1.19
1.20 -definition dist_prod_def[code del]:
1.21 +definition%important dist_prod_def[code del]:
1.22    "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
1.23
1.24  instance ..
1.25 @@ -68,7 +68,7 @@
1.26
1.27  declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
1.28
1.29 -instantiation prod :: (metric_space, metric_space) metric_space
1.30 +instantiation%important prod :: (metric_space, metric_space) metric_space
1.31  begin
1.32
1.33  lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
1.34 @@ -186,8 +186,8 @@
1.35
1.36  subsection \<open>Product is a complete metric space\<close>
1.37
1.38 -instance prod :: (complete_space, complete_space) complete_space
1.39 -proof
1.40 +instance%important prod :: (complete_space, complete_space) complete_space
1.41 +proof%unimportant
1.42    fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
1.43    have 1: "(\<lambda>n. fst (X n)) \<longlonglongrightarrow> lim (\<lambda>n. fst (X n))"
1.44      using Cauchy_fst [OF \<open>Cauchy X\<close>]
1.45 @@ -203,7 +203,7 @@
1.46
1.47  subsection \<open>Product is a normed vector space\<close>
1.48
1.49 -instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
1.50 +instantiation%important prod :: (real_normed_vector, real_normed_vector) real_normed_vector
1.51  begin
1.52
1.53  definition norm_prod_def[code del]:
1.54 @@ -245,13 +245,13 @@
1.55
1.56  instance prod :: (banach, banach) banach ..
1.57
1.58 -subsubsection \<open>Pair operations are linear\<close>
1.59 +subsubsection%unimportant \<open>Pair operations are linear\<close>
1.60
1.61 -lemma bounded_linear_fst: "bounded_linear fst"
1.62 +lemma%important bounded_linear_fst: "bounded_linear fst"
1.64    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
1.65
1.66 -lemma bounded_linear_snd: "bounded_linear snd"
1.67 +lemma%important bounded_linear_snd: "bounded_linear snd"
1.69    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
1.70
1.71 @@ -285,12 +285,12 @@
1.72    then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
1.73  qed
1.74
1.75 -subsubsection \<open>Frechet derivatives involving pairs\<close>
1.76 +subsubsection%unimportant \<open>Frechet derivatives involving pairs\<close>
1.77
1.78 -lemma has_derivative_Pair [derivative_intros]:
1.79 +lemma%important has_derivative_Pair [derivative_intros]:
1.80    assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
1.81    shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
1.82 -proof (rule has_derivativeI_sandwich[of 1])
1.83 +proof%unimportant (rule has_derivativeI_sandwich[of 1])
1.84    show "bounded_linear (\<lambda>h. (f' h, g' h))"
1.85      using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
1.86    let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
1.87 @@ -319,7 +319,7 @@
1.88    unfolding split_beta' .
1.89
1.90
1.91 -subsubsection \<open>Vector derivatives involving pairs\<close>
1.92 +subsubsection%unimportant \<open>Vector derivatives involving pairs\<close>
1.93
1.94  lemma has_vector_derivative_Pair[derivative_intros]:
1.95    assumes "(f has_vector_derivative f') (at x within s)"
1.96 @@ -331,7 +331,7 @@
1.97
1.98  subsection \<open>Product is an inner product space\<close>
1.99
1.100 -instantiation prod :: (real_inner, real_inner) real_inner
1.101 +instantiation%important prod :: (real_inner, real_inner) real_inner
1.102  begin
1.103
1.104  definition inner_prod_def:
```