*To*: "L. Yu" <ly271 at cam.ac.uk>*Subject*: Re: [isabelle] Isabelle Theory*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Tue, 09 Apr 2013 17:20:08 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <Prayer.1.3.5.1304090949510.29553@hermes-2.csi.cam.ac.uk>*Organization*: Technische Universität München*References*: <Prayer.1.3.5.1304090949510.29553@hermes-2.csi.cam.ac.uk>

Am Dienstag, den 09.04.2013, 09:49 +0100 schrieb L. Yu: > Dear All, > > I need a theorem asserting that we can maximize a differentiable function > in an interval by considering values only at the endpoints and points of > zero derivative: > > theorem > assumes "∀x. a ≤ x ∧ x ≤ b ==> DERIV f x :> (f' x)" > assumes "abs (f a) ≤ K ∧ abs (f b) ≤ K" > assumes "∀x. a ≤ x ∧ x ≤ b ∧ (f' x = 0) ==> abs(f x) ≤ K" > shows "∀x. a ≤ x ∧ x ≤ b ==> abs (f x) ≤ K" > > Does anyone know whether such a theorem has been proved in Isabelle? I > tried to look for it in Deriv.thy but did find it. > > Many thanks, > Lei No this is not available in this form, you need to invoke isCont_eq_Ub and DERIV_local_max for an upper bound K. And then show that K is also a lower bound by instantiating f with "- f x". Actually I was curious what was necessary to show it, so here is the proof for the upper bound: theorem fixes f :: "real ⇒ real" assumes f: "⋀x. a ≤ x ⟹ x ≤ b ⟹ DERIV f x :> (f' x)" assumes K: "f a ≤ K" "f b ≤ K" assumes f'_eq_0: "∀x. a ≤ x ∧ x ≤ b ∧ (f' x = 0) ⟶ f x ≤ K" shows "∀x. a ≤ x ∧ x ≤ b ⟶ f x ≤ K" proof safe fix x assume x: "a ≤ x" "x ≤ b" with f isCont_eq_Ub[of a b f] obtain x' where x': "a ≤ x'" "x' ≤ b" and max: "⋀x. a ≤ x ⟹ x ≤ b ⟹ f x ≤ f x'" by (auto intro: DERIV_isCont) have "f x' ≤ K" proof cases assume "x' = a ∨ x' = b" with K show ?thesis by auto next assume "¬ (x' = a ∨ x' = b)" with x' have "a < x'" "x' < b" by auto then have d: "0 < min (x' - a) (b - x')" by auto have "f' x' = 0" by (intro DERIV_local_max[OF f[OF x'] d] max allI impI) auto with f'_eq_0 x' show "f x' ≤ K" by auto qed with max[OF x] show "f x ≤ K" by simp qed I think about adding this theorem in a more meta-logic form. - Johannes PS: be carefully with your statements, your stated assumptions are wrong, replace ==> by -->.

**References**:**[isabelle] Isabelle Theory***From:*L. Yu

- Previous by Date: [isabelle] Unknown logic "HOL"
- Next by Date: Re: [isabelle] Unknown logic "HOL"
- Previous by Thread: [isabelle] Isabelle Theory
- Next by Thread: [isabelle] Second CFP: Ninth Panhellenic Logic Symposium
- Cl-isabelle-users April 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list