src/HOL/Deriv.thy
changeset 41368 8afa26855137
parent 37891 c26f9d06e82c
child 41550 efa734d9b221
equal deleted inserted replaced
41367:1b65137d598c 41368:8afa26855137
   877 
   877 
   878 lemma DERIV_pos_inc_left:
   878 lemma DERIV_pos_inc_left:
   879   fixes f :: "real => real"
   879   fixes f :: "real => real"
   880   shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
   880   shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
   881   apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified])
   881   apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified])
   882   apply (auto simp add: DERIV_minus) 
   882   apply (auto simp add: DERIV_minus)
   883   done
   883   done
   884 
   884 
   885 lemma DERIV_neg_dec_right:
   885 lemma DERIV_neg_dec_right:
   886   fixes f :: "real => real"
   886   fixes f :: "real => real"
   887   shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
   887   shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
   888   apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified])
   888   apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified])
   889   apply (auto simp add: DERIV_minus) 
   889   apply (auto simp add: DERIV_minus)
   890   done
   890   done
   891 
   891 
   892 lemma DERIV_local_max:
   892 lemma DERIV_local_max:
   893   fixes f :: "real => real"
   893   fixes f :: "real => real"
   894   assumes der: "DERIV f x :> l"
   894   assumes der: "DERIV f x :> l"
  1552   with fd have "f differentiable c" by simp
  1552   with fd have "f differentiable c" by simp
  1553   hence "\<exists>D. DERIV f c :> D" by (rule differentiableD)
  1553   hence "\<exists>D. DERIV f c :> D" by (rule differentiableD)
  1554   then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
  1554   then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
  1555 
  1555 
  1556   from cdef have "DERIV ?h c :> l" by auto
  1556   from cdef have "DERIV ?h c :> l" by auto
  1557   moreover
  1557   moreover have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
  1558   {
  1558     using g'cdef f'cdef by (auto intro!: DERIV_intros)
  1559     have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
       
  1560       apply (insert DERIV_const [where k="f b - f a"])
       
  1561       apply (drule meta_spec [of _ c])
       
  1562       apply (drule DERIV_mult [OF _ g'cdef])
       
  1563       by simp
       
  1564     moreover have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
       
  1565       apply (insert DERIV_const [where k="g b - g a"])
       
  1566       apply (drule meta_spec [of _ c])
       
  1567       apply (drule DERIV_mult [OF _ f'cdef])
       
  1568       by simp
       
  1569     ultimately have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
       
  1570       by (simp add: DERIV_diff)
       
  1571   }
       
  1572   ultimately have leq: "l =  g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
  1559   ultimately have leq: "l =  g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
  1573 
  1560 
  1574   {
  1561   {
  1575     from cdef have "?h b - ?h a = (b - a) * l" by auto
  1562     from cdef have "?h b - ?h a = (b - a) * l" by auto
  1576     also with leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
  1563     also with leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp