# 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"
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])
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

```