src/HOL/Analysis/Cartesian_Euclidean_Space.thy

-section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
+section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\<close>
 
 theory Cartesian_Euclidean_Space
 imports Finite_Cartesian_Product Derivative
 begin
 

     then show "j \<in> (\<lambda>j. j + i * B) ` {..<B}"
       by (auto intro!: image_eqI[of _ _ "j - i * B"])
   qed simp
 qed simp
 
-subsection\<open>Basic componentwise operations on vectors.\<close>
+subsection\<open>Basic componentwise operations on vectors\<close>
 
 instantiation vec :: (times, finite) times
 begin
 
 definition "( * ) \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"

 
 definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
   where "c *s x = (\<chi> i. c * (x$i))"
 
 
-subsection \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space.\<close>
+subsection \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\<close>
 
 lemma sum_cong_aux:
   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> sum f A = sum g A"
   by (auto intro: sum.cong)
 

   vec_component vector_add_component vector_mult_component
   vector_smult_component vector_minus_component vector_uminus_component
   vector_scaleR_component cond_component
 
 
-subsection \<open>Some frequently useful arithmetic lemmas over vectors.\<close>
+subsection \<open>Some frequently useful arithmetic lemmas over vectors\<close>
 
 instance vec :: (semigroup_mult, finite) semigroup_mult
   by standard (vector mult.assoc)
 
 instance vec :: (monoid_mult, finite) monoid_mult

   unfolding adjoint_matrix matrix_of_matrix_vector_mul
   apply rule
   done
 
 
-subsection\<open>Some bounds on components etc. relative to operator norm.\<close>
+subsection\<open>Some bounds on components etc. relative to operator norm\<close>
 
 lemma norm_column_le_onorm:
   fixes A :: "real^'n^'m"
   shows "norm(column i A) \<le> onorm(( *v) A)"
 proof -

   apply assumption
   done
 
 
 subsection \<open>Component of the differential must be zero if it exists at a local
-  maximum or minimum for that corresponding component.\<close>
+  maximum or minimum for that corresponding component\<close>
 
 lemma differential_zero_maxmin_cart:
   fixes f::"real^'a \<Rightarrow> real^'b"
   assumes "0 < e" "((\<forall>y \<in> ball x e. (f y)$k \<le> (f x)$k) \<or> (\<forall>y\<in>ball x e. (f x)$k \<le> (f y)$k))"
     "f differentiable (at x)"

   show "CARD(1) = Suc 0" by auto
 qed
 
 end
 
-subsection\<open>The collapse of the general concepts to dimension one.\<close>
+subsection\<open>The collapse of the general concepts to dimension one\<close>
 
 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
   by (simp add: vec_eq_iff)
 
 lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"

 
 lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>"
   by (auto simp add: norm_real dist_norm)
 
 
-subsection\<open>Explicit vector construction from lists.\<close>
+subsection\<open>Explicit vector construction from lists\<close>
 
 definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
 
 lemma vector_1: "(vector[x]) $1 = x"
   unfolding vector_def by simp