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.63    using fst_add fst_scaleR
    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.68    using snd_add snd_scaleR
    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: