Email Gateway (Aug 19 2022 at 10:50): Email Gateway (Aug 19 2022 at 10:50):From: "L. Yu" <ly271@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 10:50):From: Johannes Hölzl <hoelzl@in.tum.de>
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.
PS: be carefully with your statements, your stated assumptions are wrong, replace ==> by -->.
Last updated: Apr 23 2024 at 08:19 UTC