# Re: [isabelle] Isabelle Theory

```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 -->.

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.