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.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
```