src/HOL/Analysis/Product_Vector.thy

   "HOL-Library.Product_Plus"
 begin
 
 subsection \<open>Product is a real vector space\<close>
 
-instantiation prod :: (real_vector, real_vector) real_vector
+instantiation%important prod :: (real_vector, real_vector) real_vector
 begin
 
 definition scaleR_prod_def:
   "scaleR r A = (scaleR r (fst A), scaleR r (snd A))"
 

 
 subsection \<open>Product is a metric space\<close>
 
 (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
 
-instantiation prod :: (metric_space, metric_space) dist
-begin
-
-definition dist_prod_def[code del]:
+instantiation%important prod :: (metric_space, metric_space) dist
+begin
+
+definition%important dist_prod_def[code del]:
   "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
 
 instance ..
 end
 

   by standard (rule uniformity_prod_def)
 end
 
 declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
 
-instantiation prod :: (metric_space, metric_space) metric_space
+instantiation%important prod :: (metric_space, metric_space) metric_space
 begin
 
 lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
   unfolding dist_prod_def by simp
 

   then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
 qed
 
 subsection \<open>Product is a complete metric space\<close>
 
-instance prod :: (complete_space, complete_space) complete_space
-proof
+instance%important prod :: (complete_space, complete_space) complete_space
+proof%unimportant
   fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
   have 1: "(\<lambda>n. fst (X n)) \<longlonglongrightarrow> lim (\<lambda>n. fst (X n))"
     using Cauchy_fst [OF \<open>Cauchy X\<close>]
     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   have 2: "(\<lambda>n. snd (X n)) \<longlonglongrightarrow> lim (\<lambda>n. snd (X n))"

     by (rule convergentI)
 qed
 
 subsection \<open>Product is a normed vector space\<close>
 
-instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
+instantiation%important prod :: (real_normed_vector, real_normed_vector) real_normed_vector
 begin
 
 definition norm_prod_def[code del]:
   "norm x = sqrt ((norm (fst x))\<^sup>2 + (norm (snd x))\<^sup>2)"
 

 
 declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \<Rightarrow> real"]]
 
 instance prod :: (banach, banach) banach ..
 
-subsubsection \<open>Pair operations are linear\<close>
-
-lemma bounded_linear_fst: "bounded_linear fst"
+subsubsection%unimportant \<open>Pair operations are linear\<close>
+
+lemma%important bounded_linear_fst: "bounded_linear fst"
   using fst_add fst_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
-lemma bounded_linear_snd: "bounded_linear snd"
+lemma%important bounded_linear_snd: "bounded_linear snd"
   using snd_add snd_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
 lemmas bounded_linear_fst_comp = bounded_linear_fst[THEN bounded_linear_compose]
 

     apply (rule add_mono [OF norm_f norm_g])
     done
   then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
 qed
 
-subsubsection \<open>Frechet derivatives involving pairs\<close>
-
-lemma has_derivative_Pair [derivative_intros]:
+subsubsection%unimportant \<open>Frechet derivatives involving pairs\<close>
+
+lemma%important has_derivative_Pair [derivative_intros]:
   assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
-proof (rule has_derivativeI_sandwich[of 1])
+proof%unimportant (rule has_derivativeI_sandwich[of 1])
   show "bounded_linear (\<lambda>h. (f' h, g' h))"
     using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
   let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
   let ?Rg = "\<lambda>y. g y - g x - g' (y - x)"
   let ?R = "\<lambda>y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))"

 lemma has_derivative_split [derivative_intros]:
   "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
   unfolding split_beta' .
 
 
-subsubsection \<open>Vector derivatives involving pairs\<close>
+subsubsection%unimportant \<open>Vector derivatives involving pairs\<close>
 
 lemma has_vector_derivative_Pair[derivative_intros]:
   assumes "(f has_vector_derivative f') (at x within s)"
     "(g has_vector_derivative g') (at x within s)"
   shows "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"

   by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
 
 
 subsection \<open>Product is an inner product space\<close>
 
-instantiation prod :: (real_inner, real_inner) real_inner
+instantiation%important prod :: (real_inner, real_inner) real_inner
 begin
 
 definition inner_prod_def:
   "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"