src/HOL/Deriv.thy
 changeset 41368 8afa26855137 parent 37891 c26f9d06e82c child 41550 efa734d9b221
equal 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`