# Theory Bounds_Lemmas

chapter ‹General Lemmas for Proving Function Inequalities›
theory Bounds_Lemmas
imports Complex_Main
begin
text‹These are for functions that are differentiable over a closed interval.›
lemma gen_lower_bound_increasing:
fixes a :: real
assumes "a ≤ x"
and "⋀y. a ≤ y ⟹ y ≤ x ⟹ ((λx. fl x - f x) has_real_derivative g y) (at y)"
and "⋀y. a ≤ y ⟹ y ≤ x ⟹ g y ≤ 0"
and "fl a = f a"
shows "fl x ≤ f x"
proof -
have "fl x - f x ≤ fl a - f a"
apply (rule DERIV_nonpos_imp_nonincreasing [where f = "λx. fl x - f x"])
apply (rule assms)
apply (intro allI impI exI conjI)
apply (rule assms | simp)+
done
also have "... = 0"
by (simp add: assms)
finally show ?thesis
by simp
qed
lemma gen_lower_bound_decreasing:
fixes a :: real
assumes "x ≤ a"
and "⋀y. x ≤ y ⟹ y ≤ a ⟹ ((λx. fl x - f x) has_real_derivative g y) (at y)"
and "⋀y. x ≤ y ⟹ y ≤ a ⟹ g y ≥ 0"
and "fl a = f a"
shows "fl x ≤ f x"
proof -
have "fl (- (-x)) ≤ f (- (-x))"
apply (rule gen_lower_bound_increasing [of "-a" "-x" _ _ "λu. - g (-u)"])
apply (auto simp: assms)
apply (subst DERIV_mirror [symmetric])
apply (simp add: assms)
done
then show ?thesis
by simp
qed
lemma gen_upper_bound_increasing:
fixes a :: real
assumes "a ≤ x"
and "⋀y. a ≤ y ⟹ y ≤ x ⟹ ((λx. fu x - f x) has_real_derivative g y) (at y)"
and "⋀y. a ≤ y ⟹ y ≤ x ⟹ g y ≥ 0"
and "fu a = f a"
shows "f x ≤ fu x"
apply (rule gen_lower_bound_increasing [of a x f fu "λu. - g u"])
using assms DERIV_minus [where f = "λx. fu x - f x"]
apply auto
done
lemma gen_upper_bound_decreasing:
fixes a :: real
assumes "x ≤ a"
and "⋀y. x ≤ y ⟹ y ≤ a ⟹ ((λx. fu x - f x) has_real_derivative g y) (at y)"
and "⋀y. x ≤ y ⟹ y ≤ a ⟹ g y ≤ 0"
and "fu a = f a"
shows "f x ≤ fu x"
apply (rule gen_lower_bound_decreasing [of x a _ _ "λu. - g u"])
using assms DERIV_minus [where f = "λx. fu x - f x"]
apply auto
done
end