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