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