author huffman Wed Aug 10 16:35:50 2011 -0700 (2011-08-10) changeset 44140 2c10c35dd4be parent 44139 abccf1b7ea4b child 44141 0697c01ff3ea
remove several redundant and unused theorems about derivatives
```     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Aug 10 15:56:48 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Aug 10 16:35:50 2011 -0700
1.3 @@ -1526,9 +1526,9 @@
1.4
1.5  lemma has_derivative_vmul_component_cart: fixes c::"real^'a \<Rightarrow> real^'b" and v::"real^'c"
1.6    assumes "(c has_derivative c') net"
1.7 -  shows "((\<lambda>x. c(x)\$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)\$k *\<^sub>R v)) net"
1.8 -  using has_derivative_vmul_component[OF assms]
1.9 -  unfolding nth_conv_component .
1.10 +  shows "((\<lambda>x. c(x)\$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)\$k *\<^sub>R v)) net"
1.11 +  unfolding nth_conv_component
1.12 +  by (intro has_derivative_intros assms)
1.13
1.14  lemma differentiable_at_imp_differentiable_on: "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
1.15    unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)
1.16 @@ -1641,8 +1641,6 @@
1.17  lemma vec1_component[simp]: "(vec1 x)\$1 = x"
1.19
1.20 -declare vec1_dest_vec1(1) [simp]
1.21 -
1.22  lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
1.23    by (metis vec1_dest_vec1(1))
1.24
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Aug 10 15:56:48 2011 -0700
2.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Aug 10 16:35:50 2011 -0700
2.3 @@ -97,7 +97,7 @@
2.4    also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
2.6    also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
2.7 -    by (intro Lim_cong_within) (simp_all add: times_divide_eq field_simps)
2.8 +    by (intro Lim_cong_within) (simp_all add: field_simps)
2.9    finally show ?thesis
2.10      by (simp add: mult.bounded_linear_right has_derivative_within)
2.11  qed
2.12 @@ -116,43 +116,34 @@
2.13
2.14  subsubsection {* Combining theorems. *}
2.15
2.16 -lemma (in bounded_linear) has_derivative: "(f has_derivative f) net"
2.17 -  unfolding has_derivative_def apply(rule,rule bounded_linear_axioms)
2.18 -  unfolding diff by (simp add: tendsto_const)
2.19 -
2.20  lemma has_derivative_id: "((\<lambda>x. x) has_derivative (\<lambda>h. h)) net"
2.21 -  apply(rule bounded_linear.has_derivative) using bounded_linear_ident[unfolded id_def] by simp
2.22 +  unfolding has_derivative_def
2.23 +  by (simp add: bounded_linear_ident tendsto_const)
2.24
2.25  lemma has_derivative_const: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net"
2.26    unfolding has_derivative_def
2.27 -  by (rule, rule bounded_linear_zero, simp add: tendsto_const)
2.28 +  by (simp add: bounded_linear_zero tendsto_const)
2.29
2.30 -lemma (in bounded_linear) cmul: shows "bounded_linear (\<lambda>x. (c::real) *\<^sub>R f x)"
2.31 -proof -
2.32 -  have "bounded_linear (\<lambda>x. c *\<^sub>R x)"
2.33 -    by (rule scaleR.bounded_linear_right)
2.34 -  moreover have "bounded_linear f" ..
2.35 -  ultimately show ?thesis
2.36 -    by (rule bounded_linear_compose)
2.37 -qed
2.38 +lemma (in bounded_linear) has_derivative': "(f has_derivative f) net"
2.39 +  unfolding has_derivative_def apply(rule,rule bounded_linear_axioms)
2.40 +  unfolding diff by (simp add: tendsto_const)
2.41 +
2.42 +lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
2.43
2.44 -lemma has_derivative_cmul: assumes "(f has_derivative f') net" shows "((\<lambda>x. c *\<^sub>R f(x)) has_derivative (\<lambda>h. c *\<^sub>R f'(h))) net"
2.45 -  unfolding has_derivative_def apply(rule,rule bounded_linear.cmul)
2.46 -  using assms[unfolded has_derivative_def]
2.47 -  using scaleR.tendsto[OF tendsto_const assms[unfolded has_derivative_def,THEN conjunct2]]
2.48 -  unfolding scaleR_right_diff_distrib scaleR_right_distrib by auto
2.49 -
2.50 -lemma has_derivative_cmul_eq: assumes "c \<noteq> 0"
2.51 -  shows "(((\<lambda>x. c *\<^sub>R f(x)) has_derivative (\<lambda>h. c *\<^sub>R f'(h))) net \<longleftrightarrow> (f has_derivative f') net)"
2.52 -  apply(rule) defer apply(rule has_derivative_cmul,assumption)
2.53 -  apply(drule has_derivative_cmul[where c="1/c"]) using assms by auto
2.54 +lemma (in bounded_linear) has_derivative:
2.55 +  assumes "((\<lambda>x. g x) has_derivative (\<lambda>h. g' h)) net"
2.56 +  shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>h. f (g' h))) net"
2.57 +  using assms unfolding has_derivative_def
2.58 +  apply safe
2.59 +  apply (erule bounded_linear_compose [OF local.bounded_linear])
2.60 +  apply (drule local.tendsto)
2.62 +  done
2.63
2.64  lemma has_derivative_neg:
2.65 - "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
2.66 -  apply(drule has_derivative_cmul[where c="-1"]) by auto
2.67 -
2.68 -lemma has_derivative_neg_eq: "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net \<longleftrightarrow> (f has_derivative f') net"
2.69 -  apply(rule, drule_tac[!] has_derivative_neg) by auto
2.70 +  assumes "(f has_derivative f') net"
2.71 +  shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
2.72 +  using scaleR_right.has_derivative [where r="-1", OF assms] by auto
2.73
2.75    assumes "(f has_derivative f') net" and "(g has_derivative g') net"
2.76 @@ -161,11 +152,12 @@
2.77    note as = assms[unfolded has_derivative_def]
2.78    show ?thesis unfolding has_derivative_def apply(rule,rule bounded_linear_add)
2.79      using tendsto_add[OF as(1)[THEN conjunct2] as(2)[THEN conjunct2]] and as
2.80 -    by (auto simp add:algebra_simps scaleR_right_diff_distrib scaleR_right_distrib)
2.81 +    by (auto simp add: algebra_simps)
2.82  qed
2.83
2.84 -lemma has_derivative_add_const:"(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
2.85 -  apply(drule has_derivative_add) apply(rule has_derivative_const) by auto
2.87 +  "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
2.88 +  by (drule has_derivative_add, rule has_derivative_const, auto)
2.89
2.90  lemma has_derivative_sub:
2.91    assumes "(f has_derivative f') net" and "(g has_derivative g') net"
2.92 @@ -176,82 +168,22 @@
2.93    assumes "finite s" and "\<forall>a\<in>s. ((f a) has_derivative (f' a)) net"
2.94    shows "((\<lambda>x. setsum (\<lambda>a. f a x) s) has_derivative (\<lambda>h. setsum (\<lambda>a. f' a h) s)) net"
2.96 -
2.97 -lemma has_derivative_setsum_numseg:
2.98 -  "\<forall>i. m \<le> i \<and> i \<le> n \<longrightarrow> ((f i) has_derivative (f' i)) net \<Longrightarrow>
2.99 -  ((\<lambda>x. setsum (\<lambda>i. f i x) {m..n::nat}) has_derivative (\<lambda>h. setsum (\<lambda>i. f' i h) {m..n})) net"
2.100 -  by (rule has_derivative_setsum) simp_all
2.101 -
2.102  text {* Somewhat different results for derivative of scalar multiplier. *}
2.103
2.104  (** move **)
2.105 -lemma linear_vmul_component:
2.106 +lemma linear_vmul_component: (* TODO: delete *)
2.107    assumes lf: "linear f"
2.108    shows "linear (\<lambda>x. f x \$\$ k *\<^sub>R v)"
2.109    using lf
2.110    by (auto simp add: linear_def algebra_simps)
2.111
2.112 -lemma bounded_linear_euclidean_component: "bounded_linear (\<lambda>x. x \$\$ k)"
2.113 -  unfolding euclidean_component_def
2.114 -  by (rule inner.bounded_linear_right)
2.115 -
2.116 -lemma has_derivative_vmul_component:
2.117 -  fixes c::"'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" and v::"'c::real_normed_vector"
2.118 -  assumes "(c has_derivative c') net"
2.119 -  shows "((\<lambda>x. c(x)\$\$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)\$\$k *\<^sub>R v)) net" proof-
2.120 -  have *:"\<And>y. (c y \$\$ k *\<^sub>R v - (c (netlimit net) \$\$ k *\<^sub>R v + c' (y - netlimit net) \$\$ k *\<^sub>R v)) =
2.121 -        (c y \$\$ k - (c (netlimit net) \$\$ k + c' (y - netlimit net) \$\$ k)) *\<^sub>R v"
2.122 -    unfolding scaleR_left_diff_distrib scaleR_left_distrib by auto
2.123 -  show ?thesis unfolding has_derivative_def and *
2.124 -    apply (rule conjI)
2.125 -    apply (rule bounded_linear_compose [OF scaleR.bounded_linear_left])
2.126 -    apply (rule bounded_linear_compose [OF bounded_linear_euclidean_component])
2.127 -    apply (rule derivative_linear [OF assms])
2.128 -    apply(subst scaleR_zero_left[THEN sym, of v]) unfolding scaleR_scaleR
2.129 -    apply (intro tendsto_intros)
2.130 -    using assms[unfolded has_derivative_def] unfolding Lim o_def apply- apply(cases "trivial_limit net")
2.131 -    apply(rule,assumption,rule disjI2,rule,rule) proof-
2.132 -    have *:"\<And>x. x - 0 = (x::'a)" by auto
2.133 -    have **:"\<And>d x. d * (c x \$\$ k - (c (netlimit net) \$\$ k + c' (x - netlimit net) \$\$ k)) =
2.134 -      (d *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net) ))) \$\$k" by(auto simp add:field_simps)
2.135 -    fix e assume "\<not> trivial_limit net" "0 < (e::real)"
2.136 -    then have "eventually (\<lambda>x. dist ((1 / norm (x - netlimit net)) *\<^sub>R
2.137 -      (c x - (c (netlimit net) + c' (x - netlimit net)))) 0 < e) net"
2.138 -      using assms[unfolded has_derivative_def Lim] by auto
2.139 -    thus "eventually (\<lambda>x. dist (1 / norm (x - netlimit net) *
2.140 -      (c x \$\$ k - (c (netlimit net) \$\$ k + c' (x - netlimit net) \$\$ k))) 0 < e) net"
2.141 -      proof (rule eventually_elim1)
2.142 -      case goal1 thus ?case apply - unfolding dist_norm  apply(rule le_less_trans)
2.143 -        prefer 2 apply assumption unfolding * **
2.144 -        using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R
2.145 -          (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto
2.146 -    qed
2.147 -  qed
2.148 -qed
2.149 -
2.150 -lemma has_derivative_vmul_within: fixes c::"real \<Rightarrow> real"
2.151 -  assumes "(c has_derivative c') (at x within s)"
2.152 -  shows "((\<lambda>x. (c x) *\<^sub>R v) has_derivative (\<lambda>x. (c' x) *\<^sub>R v)) (at x within s)"
2.153 -  using has_derivative_vmul_component[OF assms, of 0 v] by auto
2.154 -
2.155 -lemma has_derivative_vmul_at: fixes c::"real \<Rightarrow> real"
2.156 -  assumes "(c has_derivative c') (at x)"
2.157 -  shows "((\<lambda>x. (c x) *\<^sub>R v) has_derivative (\<lambda>x. (c' x) *\<^sub>R v)) (at x)"
2.158 -  using has_derivative_vmul_within[where s=UNIV] and assms by(auto simp add: within_UNIV)
2.159 -
2.160 -lemma has_derivative_lift_dot:
2.161 -  assumes "(f has_derivative f') net"
2.162 -  shows "((\<lambda>x. inner v (f x)) has_derivative (\<lambda>t. inner v (f' t))) net" proof-
2.163 -  show ?thesis using assms unfolding has_derivative_def apply- apply(erule conjE,rule)
2.164 -    apply(rule bounded_linear_compose[of _ f']) apply(rule inner.bounded_linear_right,assumption)
2.165 -    apply(drule Lim_inner[where a=v]) unfolding o_def
2.167 -
2.168  lemmas has_derivative_intros =
2.169 -  has_derivative_sub has_derivative_add has_derivative_cmul has_derivative_id
2.170 -  has_derivative_const has_derivative_neg has_derivative_vmul_component
2.171 -  has_derivative_vmul_at has_derivative_vmul_within has_derivative_cmul
2.172 -  bounded_linear.has_derivative has_derivative_lift_dot
2.173 +  has_derivative_id has_derivative_const
2.176 +  scaleR_left.has_derivative scaleR_right.has_derivative
2.177 +  inner_left.has_derivative inner_right.has_derivative
2.178 +  euclidean_component.has_derivative
2.179
2.180  subsubsection {* Limit transformation for derivatives *}
2.181
2.182 @@ -359,7 +291,7 @@
2.183      apply (erule_tac x=e in allE)
2.184      apply (erule impE | assumption)+
2.185      apply (erule exE, rule_tac x=d in exI)
2.186 -    by (auto simp add: zero * elim!: allE)
2.187 +    by (auto simp add: zero *)
2.188  qed
2.189
2.190  lemma differentiable_imp_continuous_at:
2.191 @@ -527,7 +459,7 @@
2.192    "f differentiable net \<Longrightarrow>
2.193    (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
2.194    unfolding differentiable_def
2.195 -  apply(erule exE, drule has_derivative_cmul) by auto
2.196 +  apply(erule exE, drule scaleR_right.has_derivative) by auto
2.197
2.198  lemma differentiable_neg [intro]:
2.199    "f differentiable net \<Longrightarrow>
2.200 @@ -836,8 +768,8 @@
2.201    proof
2.202      fix x assume x:"x \<in> {a<..<b}"
2.203      show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
2.204 -      by(rule has_derivative_intros assms(3)[rule_format,OF x]
2.205 -        has_derivative_cmul[where 'b=real, unfolded real_scaleR_def])+
2.206 +      by (intro has_derivative_intros assms(3)[rule_format,OF x]
2.207 +        mult_right.has_derivative)
2.208    qed(insert assms(1), auto simp add:field_simps)
2.209    then guess x ..
2.210    thus ?thesis apply(rule_tac x=x in bexI)
2.211 @@ -882,7 +814,7 @@
2.212    have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)"
2.213      apply(rule mvt) apply(rule assms(1))
2.214      apply(rule continuous_on_inner continuous_on_intros assms(2))+
2.215 -    unfolding o_def apply(rule,rule has_derivative_lift_dot)
2.216 +    unfolding o_def apply(rule,rule has_derivative_intros)
2.217      using assms(3) by auto
2.218    then guess x .. note x=this
2.219    show ?thesis proof(cases "f a = f b")
2.220 @@ -1361,12 +1293,12 @@
2.221            unfolding o_def and diff using f'g' by auto
2.222          show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
2.223            unfolding ph' * apply(rule diff_chain_within) defer
2.224 -          apply(rule bounded_linear.has_derivative[OF assms(3)])
2.225 +          apply(rule bounded_linear.has_derivative'[OF assms(3)])
2.226            apply(rule has_derivative_intros) defer
2.227            apply(rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
2.228            apply(rule has_derivative_at_within)
2.229            using assms(5) and `u\<in>s` `a\<in>s`
2.230 -          by(auto intro!: has_derivative_intros derivative_linear)
2.231 +          by(auto intro!: has_derivative_intros bounded_linear.has_derivative' derivative_linear)
2.232          have **:"bounded_linear (\<lambda>x. f' u x - f' a x)"
2.233            "bounded_linear (\<lambda>x. f' a x - f' u x)"
2.234            apply(rule_tac[!] bounded_linear_sub)
2.235 @@ -1807,7 +1739,8 @@
2.236
2.237  lemma has_vector_derivative_cmul:
2.238    "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
2.239 -  unfolding has_vector_derivative_def apply(drule has_derivative_cmul)
2.240 +  unfolding has_vector_derivative_def
2.241 +  apply (drule scaleR_right.has_derivative)
2.242    by (auto simp add: algebra_simps)
2.243
2.244  lemma has_vector_derivative_cmul_eq:
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Aug 10 15:56:48 2011 -0700
3.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Aug 10 16:35:50 2011 -0700
3.3 @@ -3763,8 +3763,9 @@
3.4        using `x\<in>s` `c\<in>s` as by(auto simp add: algebra_simps)
3.5      have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"