src/HOL/Multivariate_Analysis/Derivative.thy
changeset 51733 70abecafe9ac
parent 51642 400ec5ae7f8f
child 53077 a1b3784f8129
equal deleted inserted replaced
51732:4392eb046a97 51733:70abecafe9ac
  1431     by (rule frechet_derivative_unique_at)
  1431     by (rule frechet_derivative_unique_at)
  1432   thus ?thesis unfolding fun_eq_iff by auto
  1432   thus ?thesis unfolding fun_eq_iff by auto
  1433 qed
  1433 qed
  1434 
  1434 
  1435 lemma vector_derivative_unique_within_closed_interval:
  1435 lemma vector_derivative_unique_within_closed_interval:
  1436   fixes f::"real \<Rightarrow> 'n::ordered_euclidean_space"
       
  1437   assumes "a < b" and "x \<in> {a..b}"
  1436   assumes "a < b" and "x \<in> {a..b}"
  1438   assumes "(f has_vector_derivative f') (at x within {a..b})"
  1437   assumes "(f has_vector_derivative f') (at x within {a..b})"
  1439   assumes "(f has_vector_derivative f'') (at x within {a..b})"
  1438   assumes "(f has_vector_derivative f'') (at x within {a..b})"
  1440   shows "f' = f''"
  1439   shows "f' = f''"
  1441 proof-
  1440 proof-
  1458   apply(rule vector_derivative_unique_at) defer apply assumption
  1457   apply(rule vector_derivative_unique_at) defer apply assumption
  1459   unfolding vector_derivative_works[THEN sym] differentiable_def
  1458   unfolding vector_derivative_works[THEN sym] differentiable_def
  1460   unfolding has_vector_derivative_def by auto
  1459   unfolding has_vector_derivative_def by auto
  1461 
  1460 
  1462 lemma vector_derivative_within_closed_interval:
  1461 lemma vector_derivative_within_closed_interval:
  1463   fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"
       
  1464   assumes "a < b" and "x \<in> {a..b}"
  1462   assumes "a < b" and "x \<in> {a..b}"
  1465   assumes "(f has_vector_derivative f') (at x within {a..b})"
  1463   assumes "(f has_vector_derivative f') (at x within {a..b})"
  1466   shows "vector_derivative f (at x within {a..b}) = f'"
  1464   shows "vector_derivative f (at x within {a..b}) = f'"
  1467   apply(rule vector_derivative_unique_within_closed_interval)
  1465   apply(rule vector_derivative_unique_within_closed_interval)
  1468   using vector_derivative_works[unfolded differentiable_def]
  1466   using vector_derivative_works[unfolded differentiable_def]