src/HOL/Analysis/Product_Vector.thy
changeset 67685 bdff8bf0a75b
parent 66453 cc19f7ca2ed6
child 67962 0acdcd8f4ba1
     1.1 --- a/src/HOL/Analysis/Product_Vector.thy	Tue Feb 20 22:25:23 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Thu Feb 22 15:17:25 2018 +0100
     1.3 @@ -306,6 +306,11 @@
     1.4      by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
     1.5  qed simp
     1.6  
     1.7 +lemma differentiable_Pair [simp, derivative_intros]:
     1.8 +  "f differentiable at x within s \<Longrightarrow> g differentiable at x within s \<Longrightarrow>
     1.9 +    (\<lambda>x. (f x, g x)) differentiable at x within s"
    1.10 +  unfolding differentiable_def by (blast intro: has_derivative_Pair)
    1.11 +
    1.12  lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
    1.13  lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
    1.14  
    1.15 @@ -313,6 +318,17 @@
    1.16    "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
    1.17    unfolding split_beta' .
    1.18  
    1.19 +
    1.20 +subsubsection \<open>Vector derivatives involving pairs\<close>
    1.21 +
    1.22 +lemma has_vector_derivative_Pair[derivative_intros]:
    1.23 +  assumes "(f has_vector_derivative f') (at x within s)"
    1.24 +    "(g has_vector_derivative g') (at x within s)"
    1.25 +  shows "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
    1.26 +  using assms
    1.27 +  by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
    1.28 +
    1.29 +
    1.30  subsection \<open>Product is an inner product space\<close>
    1.31  
    1.32  instantiation prod :: (real_inner, real_inner) real_inner
    1.33 @@ -368,4 +384,9 @@
    1.34  lemma norm_snd_le: "norm y \<le> norm (x,y)"
    1.35    by (metis dist_snd_le snd_conv snd_zero norm_conv_dist)
    1.36  
    1.37 +lemma norm_Pair_le:
    1.38 +  shows "norm (x, y) \<le> norm x + norm y"
    1.39 +  unfolding norm_Pair
    1.40 +  by (metis norm_ge_zero sqrt_sum_squares_le_sum)
    1.41 +
    1.42  end