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.