Session Special_Function_Bounds

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

Theory Atan_CF_Bounds

chapter ‹Arctan Upper and Lower Bounds›

theory Atan_CF_Bounds
imports Bounds_Lemmas  
        "HOL-Library.Sum_of_Squares"

begin

text‹Covers all bounds used in arctan-upper.ax, arctan-lower.ax and arctan-extended.ax,
excepting only arctan-extended2.ax, which is used in two atan-error-analysis problems.›

section ‹Upper Bound 1›

definition arctan_upper_11 :: "real  real"
  where "arctan_upper_11  λx. -(pi/2) - 1/x"

definition diff_delta_arctan_upper_11 :: "real  real"
  where "diff_delta_arctan_upper_11  λx. 1 / (x^2 * (1 + x^2))"

lemma d_delta_arctan_upper_11: "x  0 
    ((λx. arctan_upper_11 x - arctan x) has_field_derivative diff_delta_arctan_upper_11 x) (at x)"
unfolding arctan_upper_11_def diff_delta_arctan_upper_11_def
apply (intro derivative_eq_intros | simp)+
apply (simp add: divide_simps add_nonneg_eq_0_iff, algebra)
done

lemma d_delta_arctan_upper_11_pos: "x  0  diff_delta_arctan_upper_11 x > 0"
unfolding diff_delta_arctan_upper_11_def
by (simp add: divide_simps zero_less_mult_iff add_pos_pos)

text‹Different proof needed here: they coincide not at zero, but at (-) infinity!›

lemma arctan_upper_11:
  assumes "x < 0"
    shows "arctan(x) < arctan_upper_11 x"
proof -
  have "((λx. arctan_upper_11 x - arctan x)  - (pi / 2) - 0 - (- (pi / 2))) at_bot"
    unfolding arctan_upper_11_def
    apply (intro tendsto_intros tendsto_arctan_at_bot, auto simp: ext [OF divide_inverse])
    apply (metis tendsto_inverse_0 at_bot_le_at_infinity tendsto_mono)
    done
  then have *: "((λx. arctan_upper_11 x - arctan x)  0) at_bot"
    by simp
  have "0 < arctan_upper_11 x - arctan x"
    apply (rule DERIV_pos_imp_increasing_at_bot [OF _ *])
    apply (metis assms d_delta_arctan_upper_11 d_delta_arctan_upper_11_pos not_le)
    done
  then show ?thesis
    by auto
qed

definition arctan_upper_12 :: "real  real"
  where "arctan_upper_12  λx. 3*x / (x^2 + 3)"

definition diff_delta_arctan_upper_12 :: "real  real"
  where "diff_delta_arctan_upper_12  λx. -4*x^4 / ((x^2+3)^2 * (1+x^2))"

lemma d_delta_arctan_upper_12:
     "((λx. arctan_upper_12 x - arctan x) has_field_derivative diff_delta_arctan_upper_12 x) (at x)"
  unfolding arctan_upper_12_def diff_delta_arctan_upper_12_def
  apply (intro derivative_eq_intros,  simp_all)
  apply (auto simp: divide_simps add_nonneg_eq_0_iff, algebra)
  done

text‹Strict inequalities also possible›
lemma arctan_upper_12:
  assumes "x  0" shows "arctan(x)  arctan_upper_12 x"
apply (rule gen_upper_bound_decreasing [OF assms d_delta_arctan_upper_12])
apply (auto simp: diff_delta_arctan_upper_12_def arctan_upper_12_def)
done

definition arctan_upper_13 :: "real  real"
  where "arctan_upper_13  λx. x"

definition diff_delta_arctan_upper_13 :: "real  real"
  where "diff_delta_arctan_upper_13  λx. x^2 / (1 + x^2)"

lemma d_delta_arctan_upper_13:
    "((λx. arctan_upper_13 x - arctan x) has_field_derivative diff_delta_arctan_upper_13 x) (at x)"
unfolding arctan_upper_13_def diff_delta_arctan_upper_13_def
apply (intro derivative_eq_intros, simp_all)
apply (simp add: divide_simps add_nonneg_eq_0_iff)
done

lemma arctan_upper_13:
  assumes "x  0" shows "arctan(x)  arctan_upper_13 x"
apply (rule gen_upper_bound_increasing [OF assms d_delta_arctan_upper_13])
apply (auto simp: diff_delta_arctan_upper_13_def arctan_upper_13_def)
done

definition arctan_upper_14 :: "real  real"
  where "arctan_upper_14  λx. pi/2 - 3*x / (1 + 3*x^2)"

definition diff_delta_arctan_upper_14 :: "real  real"
  where "diff_delta_arctan_upper_14  λx. -4 / ((1 + 3*x^2)^2 * (1+x^2))"

lemma d_delta_arctan_upper_14:
  "((λx. arctan_upper_14 x - arctan x) has_field_derivative diff_delta_arctan_upper_14 x) (at x)"
unfolding arctan_upper_14_def diff_delta_arctan_upper_14_def
apply (intro derivative_eq_intros | simp add: add_nonneg_eq_0_iff)+
apply (simp add: divide_simps add_nonneg_eq_0_iff, algebra)
done

lemma d_delta_arctan_upper_14_neg: "diff_delta_arctan_upper_14 x < 0"
unfolding diff_delta_arctan_upper_14_def
apply (auto simp: divide_simps add_nonneg_eq_0_iff zero_less_mult_iff)
using power2_less_0 [of x]
apply arith
done

lemma lim14: "((λx::real. 3 * x / (1 + 3 * x2))  0) at_infinity"
  apply (rule tendsto_0_le [where f = inverse and K=1])
  apply (metis tendsto_inverse_0)
  apply (simp add: eventually_at_infinity)
  apply (rule_tac x=1 in exI)
  apply (simp add: power_eq_if abs_if divide_simps add_sign_intros)
  done

text‹Different proof needed here: they coincide not at zero, but at (+) infinity!›

lemma arctan_upper_14:
  assumes "x > 0"
    shows "arctan(x) < arctan_upper_14 x"
proof -
  have "((λx. arctan_upper_14 x - arctan x)  pi / 2 - 0 - pi / 2) at_top"
    unfolding arctan_upper_14_def
    apply (intro tendsto_intros tendsto_arctan_at_top)
    apply (auto simp: tendsto_mono [OF at_top_le_at_infinity lim14])
    done
  then have *: "((λx. arctan_upper_14 x - arctan x)  0) at_top"
    by simp
  have "0 < arctan_upper_14 x - arctan x"
    apply (rule DERIV_neg_imp_decreasing_at_top [OF _ *])
    apply (metis d_delta_arctan_upper_14 d_delta_arctan_upper_14_neg)
    done
  then show ?thesis
    by auto
qed

section ‹Lower Bound 1›

definition arctan_lower_11 :: "real  real"
  where "arctan_lower_11  λx. -(pi/2) - 3*x / (1 + 3*x^2)"

lemma arctan_lower_11:
  assumes "x < 0"
    shows "arctan(x) > arctan_lower_11 x"
    using arctan_upper_14 [of "-x"] assms
    by (auto simp: arctan_upper_14_def arctan_lower_11_def arctan_minus)

abbreviation "arctan_lower_12  arctan_upper_13"

lemma arctan_lower_12:
  assumes "x  0"
    shows "arctan(x)  arctan_lower_12 x"
    using arctan_upper_13 [of "-x"] assms
    by (auto simp: arctan_upper_13_def arctan_minus)

abbreviation "arctan_lower_13  arctan_upper_12"

lemma arctan_lower_13:
  assumes "x  0"
    shows "arctan(x)  arctan_lower_13 x"
    using arctan_upper_12 [of "-x"] assms
    by (auto simp: arctan_upper_12_def arctan_minus)

definition arctan_lower_14 :: "real  real"
  where "arctan_lower_14  λx. pi/2 - 1/x"

lemma arctan_lower_14:
  assumes "x > 0"
    shows "arctan(x) > arctan_lower_14 x"
    using arctan_upper_11 [of "-x"] assms
    by (auto simp: arctan_upper_11_def arctan_lower_14_def arctan_minus)

section ‹Upper Bound 3›

definition arctan_upper_31 :: "real  real"
  where "arctan_upper_31  λx. -(pi/2) - (64 + 735*x^2 + 945*x^4) / (15*x*(15 + 70*x^2 + 63*x^4))"

definition diff_delta_arctan_upper_31 :: "real  real"
  where "diff_delta_arctan_upper_31  λx. 64 / (x^2 * (15 + 70*x^2 + 63*x^4)^2 * (1 + x^2))"

lemma d_delta_arctan_upper_31:
  assumes "x  0"
    shows "((λx. arctan_upper_31 x - arctan x) has_field_derivative diff_delta_arctan_upper_31 x) (at x)"
  unfolding arctan_upper_31_def diff_delta_arctan_upper_31_def
  using assms
  apply (intro derivative_eq_intros)
  apply (rule refl | simp add: add_nonneg_eq_0_iff)+
  apply (simp add: divide_simps add_nonneg_eq_0_iff, algebra)
  done

lemma d_delta_arctan_upper_31_pos: "x  0  diff_delta_arctan_upper_31 x > 0"
unfolding diff_delta_arctan_upper_31_def
by (auto simp: divide_simps zero_less_mult_iff add_pos_pos add_nonneg_eq_0_iff)

lemma arctan_upper_31:
  assumes "x < 0"
    shows "arctan(x) < arctan_upper_31 x"
proof -
  have *: "x::real.  (15 + 70 * x2 + 63 * x ^ 4) > 0"
    by (sos "((R<1 + ((R<1 * ((R<7/8 * [19/7*x^2 + 1]^2) + ((R<4 * [x]^2) + (R<10/7 * [x^2]^2)))) + ((A<=0 * R<1) * (R<1/8 * [1]^2)))))")
  then have **: "x::real. ¬ (15 + 70 * x2 + 63 * x ^ 4) < 0"
    by (simp add: not_less)
  have "((λx::real. (64 + 735 * x2 + 945 * x ^ 4) / (15 * x * (15 + 70 * x2 + 63 * x ^ 4)))  0) at_bot"
    apply (rule tendsto_0_le [where f = inverse and K=2])
    apply (metis at_bot_le_at_infinity tendsto_inverse_0 tendsto_mono)
    apply (simp add: eventually_at_bot_linorder)
    apply (rule_tac x="-1" in exI)
    apply (auto simp: divide_simps abs_if zero_less_mult_iff **)
    done
  then have "((λx. arctan_upper_31 x - arctan x)  - (pi / 2) - 0 - (- (pi / 2))) at_bot"
    unfolding arctan_upper_31_def
    apply (intro tendsto_intros tendsto_arctan_at_bot, auto)
    done
  then have *: "((λx. arctan_upper_31 x - arctan x)  0) at_bot"
    by simp
  have "0 < arctan_upper_31 x - arctan x"
    apply (rule DERIV_pos_imp_increasing_at_bot [OF _ *])
    apply (metis assms d_delta_arctan_upper_31 d_delta_arctan_upper_31_pos not_le)
    done
  then show ?thesis
    by auto
qed

definition arctan_upper_32 :: "real  real"
  where "arctan_upper_32  λx. 7*(33*x^4 + 170*x^2 + 165)*x / (5*(5*x^6 + 105*x^4 + 315*x^2 + 231))"

definition diff_delta_arctan_upper_32 :: "real  real"
  where "diff_delta_arctan_upper_32  λx. -256*x^12 / ((5*x^6+105*x^4+315*x^2+231)^2*(1+x^2))"

lemma d_delta_arctan_upper_32:
    "((λx. arctan_upper_32 x - arctan x) has_field_derivative diff_delta_arctan_upper_32 x) (at x)"
    unfolding arctan_upper_32_def diff_delta_arctan_upper_32_def
    apply (intro derivative_eq_intros | simp)+
    apply simp_all
    apply (auto simp: add_nonneg_eq_0_iff divide_simps, algebra)
    done

lemma arctan_upper_32:
  assumes "x  0" shows "arctan(x)  arctan_upper_32 x"
apply (rule gen_upper_bound_decreasing [OF assms d_delta_arctan_upper_32])
apply (auto simp: diff_delta_arctan_upper_32_def arctan_upper_32_def)
done

definition arctan_upper_33 :: "real  real"
  where "arctan_upper_33  λx. (64*x^4+735*x^2+945)*x / (15*(15*x^4+70*x^2+63))"

definition diff_delta_arctan_upper_33 :: "real  real"
  where "diff_delta_arctan_upper_33  λx. 64*x^10 / ((15*x^4+70*x^2+63)^2*(1+x^2))"

lemma d_delta_arctan_upper_33:
    "((λx. arctan_upper_33 x - arctan x) has_field_derivative diff_delta_arctan_upper_33 x) (at x)"
unfolding arctan_upper_33_def diff_delta_arctan_upper_33_def
apply (intro derivative_eq_intros, simp_all)
apply (auto simp: add_nonneg_eq_0_iff divide_simps, algebra)
done

lemma arctan_upper_33:
  assumes "x  0" shows "arctan(x)  arctan_upper_33 x"
apply (rule gen_upper_bound_increasing [OF assms d_delta_arctan_upper_33])
apply (auto simp: diff_delta_arctan_upper_33_def arctan_upper_33_def)
done

definition arctan_upper_34 :: "real  real"
  where "arctan_upper_34 
         λx. pi/2 - (33 + 170*x^2 + 165*x^4)*7*x / (5*(5 + 105*x^2 + 315*x^4 + 231*x^6))"

definition diff_delta_arctan_upper_34 :: "real  real"
  where "diff_delta_arctan_upper_34  λx. -256 / ((5+105*x^2+315*x^4+231*x^6)^2*(1+x^2))"

lemma d_delta_arctan_upper_34:
  "((λx. arctan_upper_34 x - arctan x) has_field_derivative diff_delta_arctan_upper_34 x) (at x)"
unfolding arctan_upper_34_def diff_delta_arctan_upper_34_def
apply (intro derivative_eq_intros | simp add: add_nonneg_eq_0_iff)+
apply (simp add: divide_simps add_nonneg_eq_0_iff, algebra)
done

lemma d_delta_arctan_upper_34_pos: "diff_delta_arctan_upper_34 x < 0"
unfolding diff_delta_arctan_upper_34_def
apply (simp add: divide_simps add_nonneg_eq_0_iff zero_less_mult_iff)
using power2_less_0 [of x]
apply arith
done

lemma arctan_upper_34:
  assumes "x > 0"
    shows "arctan(x) < arctan_upper_34 x"
proof -
  have "((λx. arctan_upper_34 x - arctan x)  pi / 2 - 0 - pi / 2) at_top"
    unfolding arctan_upper_34_def
    apply (intro tendsto_intros tendsto_arctan_at_top, auto)
    apply (rule tendsto_0_le [where f = inverse and K=1])
    apply (metis tendsto_inverse_0 at_top_le_at_infinity tendsto_mono)
    apply (simp add: eventually_at_top_linorder)
    apply (rule_tac x=1 in exI)
    apply (auto simp: divide_simps power_eq_if add_pos_pos algebra_simps)
    done
  then have *: "((λx. arctan_upper_34 x - arctan x)  0) at_top"
    by simp
  have "0 < arctan_upper_34 x - arctan x"
    apply (rule DERIV_neg_imp_decreasing_at_top [OF _ *])
    apply (metis d_delta_arctan_upper_34 d_delta_arctan_upper_34_pos)
    done
  then show ?thesis
    by auto
qed

section ‹Lower Bound 3›

definition arctan_lower_31 :: "real  real"
  where "arctan_lower_31  λx. -(pi/2) - (33 + 170*x^2 + 165*x^4)*7*x / (5*(5 + 105*x^2 + 315*x^4 + 231*x^6))"

lemma arctan_lower_31:
  assumes "x < 0"
    shows "arctan(x) > arctan_lower_31 x"
    using arctan_upper_34 [of "-x"] assms
    by (auto simp: arctan_upper_34_def arctan_lower_31_def arctan_minus)

abbreviation "arctan_lower_32  arctan_upper_33"

lemma arctan_lower_32:
  assumes "x  0"
    shows "arctan(x)  arctan_lower_32 x"
    using arctan_upper_33 [of "-x"] assms
    by (auto simp: arctan_upper_33_def arctan_minus)

abbreviation "arctan_lower_33  arctan_upper_32"

lemma arctan_lower_33:
  assumes "x  0"
    shows "arctan(x)  arctan_lower_33 x"
    using arctan_upper_32 [of "-x"] assms
    by (auto simp: arctan_upper_32_def arctan_minus)

definition arctan_lower_34 :: "real  real"
  where "arctan_lower_34  λx. pi/2 - (64 + 735*x^2 + 945*x^4) / (15*x*(15 + 70*x^2 + 63*x^4))"

lemma arctan_lower_34:
  assumes "x > 0"
    shows "arctan(x) > arctan_lower_34 x"
    using arctan_upper_31 [of "-x"] assms
    by (auto simp: arctan_upper_31_def arctan_lower_34_def arctan_minus)

section ‹Upper Bound 4›

definition arctan_upper_41 :: "real  real"
  where "arctan_upper_41 
        λx. -(pi/2) - (256 + 5943*x^2 + 19250*x^4 + 15015*x^6) /
               (35*x*(35 + 315*x^2 + 693*x^4 + 429*x^6))"

definition diff_delta_arctan_upper_41 :: "real  real"
  where "diff_delta_arctan_upper_41  λx. 256 / (x^2*(35+315*x^2+693*x^4+429*x^6)^2*(1+x^2))"

lemma d_delta_arctan_upper_41:
  assumes "x  0"
    shows "((λx. arctan_upper_41 x - arctan x) has_field_derivative diff_delta_arctan_upper_41 x) (at x)"
  unfolding arctan_upper_41_def diff_delta_arctan_upper_41_def
  using assms
  apply (intro derivative_eq_intros)
  apply (rule refl | simp add: add_nonneg_eq_0_iff)+
  apply (simp add: divide_simps add_nonneg_eq_0_iff, algebra)
  done

lemma d_delta_arctan_upper_41_pos: "x  0  diff_delta_arctan_upper_41 x > 0"
unfolding diff_delta_arctan_upper_41_def
by (auto simp: zero_less_mult_iff add_pos_pos add_nonneg_eq_0_iff)

lemma arctan_upper_41:
  assumes "x < 0"
    shows "arctan(x) < arctan_upper_41 x"
proof -
  have *: "x::real. (35 + 315 * x2 + 693 * x ^ 4 + 429 * x ^ 6) > 0"
    by (sos "((R<1 + ((R<1 * ((R<13/8589934592 * [95/26*x^2 + 1]^2) + ((R<38654705675/4294967296 * [170080704731/154618822700*x^3 + x]^2) + ((R<14271/446676598784 * [x^2]^2) + (R<3631584276674589067439/2656331147370089676800 * [x^3]^2))))) + ((A<=0 * R<1) * (R<245426703/8589934592 * [1]^2)))))")
  then have **: "x::real. x < 0  ¬ (35 + 315 * x2 + 693 * x ^ 4 + 429 * x ^ 6) < 0"
    by (simp add: not_less)
  have "((λx::real. (256 + 5943 * x2 + 19250 * x ^ 4 + 15015 * x ^ 6) /
           (35 * x * (35 + 315 * x2 + 693 * x ^ 4 + 429 * x ^ 6)))  0) at_bot"
    apply (rule tendsto_0_le [where f = inverse and K=2])
    apply (metis at_bot_le_at_infinity tendsto_inverse_0 tendsto_mono)
    apply (simp add: eventually_at_bot_linorder)
    apply (rule_tac x="-1" in exI)
    apply (auto simp: ** abs_if divide_simps zero_less_mult_iff)
    done
  then have "((λx. arctan_upper_41 x - arctan x)  - (pi / 2) - 0 - (- (pi / 2))) at_bot"
    unfolding arctan_upper_41_def
    apply (intro tendsto_intros tendsto_arctan_at_bot, auto)
    done
  then have *: "((λx. arctan_upper_41 x - arctan x)  0) at_bot"
    by simp
  have "0 < arctan_upper_41 x - arctan x"
    apply (rule DERIV_pos_imp_increasing_at_bot [OF _ *])
    apply (metis assms d_delta_arctan_upper_41 d_delta_arctan_upper_41_pos not_le)
    done
  then show ?thesis
    by auto
qed

definition arctan_upper_42 :: "real  real"
  where "arctan_upper_42 
          λx. (15159*x^6+147455*x^4+345345*x^2+225225)*x / (35*(35*x^8+1260*x^6+6930*x^4+12012*x^2+6435))"

definition diff_delta_arctan_upper_42 :: "real  real"
  where "diff_delta_arctan_upper_42 
            λx. -16384*x^16 / ((35*x^8+1260*x^6+6930*x^4+12012*x^2+6435)^2*(1+x^2))"

lemma d_delta_arctan_upper_42:
    "((λx. arctan_upper_42 x - arctan x) has_field_derivative diff_delta_arctan_upper_42 x) (at x)"
    unfolding arctan_upper_42_def diff_delta_arctan_upper_42_def
    apply (intro derivative_eq_intros, simp_all)
    apply (auto simp: divide_simps add_nonneg_eq_0_iff, algebra)
    done

lemma arctan_upper_42:
  assumes "x  0" shows "arctan(x)  arctan_upper_42 x"
apply (rule gen_upper_bound_decreasing [OF assms d_delta_arctan_upper_42])
apply (auto simp: diff_delta_arctan_upper_42_def arctan_upper_42_def)
done

definition arctan_upper_43 :: "real  real"
  where "arctan_upper_43 
          λx. (256*x^6+5943*x^4+19250*x^2+15015)*x /
              (35 * (35*x^6+315*x^4+693*x^2+429))"

definition diff_delta_arctan_upper_43 :: "real  real"
  where "diff_delta_arctan_upper_43  λx. 256*x^14 / ((35*x^6+315*x^4+693*x^2+429)^2*(1+x^2))"

lemma d_delta_arctan_upper_43:
    "((λx. arctan_upper_43 x - arctan x) has_field_derivative diff_delta_arctan_upper_43 x) (at x)"
unfolding arctan_upper_43_def diff_delta_arctan_upper_43_def
apply (intro derivative_eq_intros, simp_all)
apply (auto simp: add_nonneg_eq_0_iff divide_simps, algebra)
done

lemma arctan_upper_43:
  assumes "x  0" shows "arctan(x)  arctan_upper_43 x"
apply (rule gen_upper_bound_increasing [OF assms d_delta_arctan_upper_43])
apply (auto simp: diff_delta_arctan_upper_43_def arctan_upper_43_def)
done

definition arctan_upper_44 :: "real  real"
  where "arctan_upper_44 
         λx. pi/2 - (15159+147455*x^2+345345*x^4+225225*x^6)*x /
                 (35*(35+1260*x^2+6930*x^4+12012*x^6+6435*x^8))"

definition diff_delta_arctan_upper_44 :: "real  real"
  where "diff_delta_arctan_upper_44 
    λx. -16384 / ((35+1260*x^2+6930*x^4+12012*x^6+6435*x^8)^2*(1+x^2))"

lemma d_delta_arctan_upper_44:
  "((λx. arctan_upper_44 x - arctan x) has_field_derivative diff_delta_arctan_upper_44 x) (at x)"
unfolding arctan_upper_44_def diff_delta_arctan_upper_44_def
apply (intro derivative_eq_intros | simp add: add_nonneg_eq_0_iff)+
apply (simp add: divide_simps add_nonneg_eq_0_iff, algebra)
done

lemma d_delta_arctan_upper_44_pos: "diff_delta_arctan_upper_44 x < 0"
unfolding diff_delta_arctan_upper_44_def
apply (auto simp: divide_simps add_nonneg_eq_0_iff zero_less_mult_iff)
using power2_less_0 [of x]
apply arith
done

lemma arctan_upper_44:
  assumes "x > 0"
    shows "arctan(x) < arctan_upper_44 x"
proof -
  have "((λx. arctan_upper_44 x - arctan x)  pi / 2 - 0 - pi / 2) at_top"
    unfolding arctan_upper_44_def
    apply (intro tendsto_intros tendsto_arctan_at_top, auto)
    apply (rule tendsto_0_le [where f = inverse and K=1])
    apply (metis tendsto_inverse_0 at_top_le_at_infinity tendsto_mono)
    apply (simp add: eventually_at_top_linorder)
    apply (rule_tac x=1 in exI)
    apply (auto simp: zero_le_mult_iff divide_simps not_le[symmetric] power_eq_if algebra_simps)
    done
  then have *: "((λx. arctan_upper_44 x - arctan x)  0) at_top"
    by simp
  have "0 < arctan_upper_44 x - arctan x"
    apply (rule DERIV_neg_imp_decreasing_at_top [OF _ *])
    apply (metis d_delta_arctan_upper_44 d_delta_arctan_upper_44_pos)
    done
  then show ?thesis
    by auto
qed

section ‹Lower Bound 4›

definition arctan_lower_41 :: "real  real"
  where "arctan_lower_41 
     λx. -(pi/2) - (15159+147455*x^2+345345*x^4+225225*x^6)*x /
                   (35*(35+1260*x^2+6930*x^4+12012*x^6+6435*x^8))"

lemma arctan_lower_41:
  assumes "x < 0"
    shows "arctan(x) > arctan_lower_41 x"
    using arctan_upper_44 [of "-x"] assms
    by (auto simp: arctan_upper_44_def arctan_lower_41_def arctan_minus)

abbreviation "arctan_lower_42  arctan_upper_43"

lemma arctan_lower_42:
  assumes "x  0"
    shows "arctan(x)  arctan_lower_42 x"
    using arctan_upper_43 [of "-x"] assms
    by (auto simp: arctan_upper_43_def arctan_minus)

abbreviation "arctan_lower_43  arctan_upper_42"

lemma arctan_lower_43:
  assumes "x  0"
    shows "arctan(x)  arctan_lower_43 x"
    using arctan_upper_42 [of "-x"] assms
    by (auto simp: arctan_upper_42_def arctan_minus)

definition arctan_lower_44 :: "real  real"
  where "arctan_lower_44 
    λx. pi/2 - (256+5943*x^2+19250*x^4+15015*x^6) /
               (35*x*(35+315*x^2+693*x^4+429*x^6))"

lemma arctan_lower_44:
  assumes "x > 0"
    shows "arctan(x) > arctan_lower_44 x"
    using arctan_upper_41 [of "-x"] assms
    by (auto simp: arctan_upper_41_def arctan_lower_44_def arctan_minus)

end

Theory Exp_Bounds

chapter ‹Exp Upper and Lower Bounds›

theory Exp_Bounds
imports Bounds_Lemmas
        "HOL-Library.Sum_of_Squares"
        Sturm_Sequences.Sturm

begin

text‹Covers all bounds used in exp-upper.ax, exp-lower.ax and exp-extended.ax.›

section ‹Taylor Series Bounds›

textexp_positive› is the theorem @{thm Transcendental.exp_ge_zero}

textexp_lower_taylor_1› is the theorem @{thm Transcendental.exp_ge_add_one_self}

text‹All even approximants are lower bounds.›
lemma exp_lower_taylor_even: 
  fixes x::real
  shows "even n  (m<n. (x ^ m) / (fact m))  exp x"
  using Maclaurin_exp_le [of x n]
  by (auto simp add: zero_le_even_power)

lemma exp_upper_taylor_even:
  fixes x::real
  assumes n: "even n"
      and pos: "(m<n. ((-x) ^ m) / (fact m)) > 0"  (is "?sum > 0")
    shows "exp x  inverse ?sum"
  using exp_lower_taylor_even [OF n, of "-x"]
  by (metis exp_minus inverse_inverse_eq le_imp_inverse_le pos)

text‹3 if the previous lemma is expressed in terms of @{term "2*m"}.›
lemma exp_lower_taylor_3:
  fixes x::real
  shows "1 + x + (1/2)*x^2 + (1/6)*x^3 + (1/24)*x^4 + (1/120)*x^5  exp x"
  by (rule order_trans [OF _ exp_lower_taylor_even [of 6]])
     (auto simp: lessThan_nat_numeral fact_numeral)

lemma exp_lower_taylor_3_cubed:
  fixes x::real
  shows "(1 + x/3 + (1/2)*(x/3)^2 + (1/6)*(x/3)^3 + (1/24)*(x/3)^4 + (1/120)*(x/3)^5)^3  exp x"
proof -
  have "(1 + x/3 + (1/2)*(x/3)^2 + (1/6)*(x/3)^3 + (1/24)*(x/3)^4 + (1/120)*(x/3)^5) ^ 3
         exp (x/3) ^ 3"
    by (metis power_mono_odd odd_numeral exp_lower_taylor_3)
 also have "... = exp x"
   by (simp add: exp_of_nat_mult [symmetric])
 finally show ?thesis .
qed

lemma exp_lower_taylor_2:
  fixes x::real
  shows "1 + x + (1/2)*x^2 + (1/6)*x^3  exp x"
proof -
  have "even (4::nat)" by simp
  then have "(m<4. x ^ m / (fact m))  exp x"
    by (rule exp_lower_taylor_even)
  then show ?thesis by (auto simp add: numeral_eq_Suc)
qed

lemma exp_upper_bound_case_3:
  fixes x::real
  assumes "x  3.19"
  shows "exp x  2304 / (-(x^3) + 6*x^2 - 24*x + 48)^2"
proof -
  have "(1/48)*(-(x^3) + 6*x^2 - 24*x + 48) = (1 + (-x/2) + (1/2)*(-x/2)^2 + (1/6)*(-x/2)^3)"
    by (simp add: field_simps power2_eq_square power3_eq_cube)
  also have "...  exp (-x/2)"
    by (rule exp_lower_taylor_2)
  finally have 1: "(1/48)*(-(x^3) + 6*x^2 - 24*x + 48)  exp (-x/2)" .
  have "(-(x^3) + 6*x^2 - 24*x + 48)^2 / 2304 = ((1/48)*(-(x^3) + 6*x^2 - 24*x + 48))^2"
    by (simp add: field_simps power2_eq_square power3_eq_cube)
  also have "...  (exp (-x/2))^2"
    apply (rule power_mono [OF 1])
    apply (simp add: algebra_simps)
    using assms
    apply (sos "((R<1 + ((R<1 * ((R<1323/13 * [~15/49*x + 1]^2) + (R<1/637 * [x]^2))) + (((A<0 * R<1) * (R<50/13 * [1]^2)) + ((A<=0 * R<1) * ((R<56/13 * [~5/56*x + 1]^2) + (R<199/728 * [x]^2)))))))")
    done
  also have "... = inverse (exp x)"
    by (metis exp_minus mult_exp_exp power2_eq_square field_sum_of_halves)
  finally have 2: "(-(x^3) + 6*x^2 - 24*x + 48)^2 / 2304  inverse (exp x)" .
  have "6 * x2 - x ^ 3 - 24 * x + 48  0" using assms
    by (sos "((R<1 + (([~400/13] * A=0) + ((R<1 * ((R<1323/13 * [~15/49*x + 1]^2) + (R<1/637 * [x]^2))) + ((A<=0 * R<1) * ((R<56/13 * [~5/56*x + 1]^2) + (R<199/728 * [x]^2)))))))")
  then show ?thesis
    using Fields.linordered_field_class.le_imp_inverse_le [OF 2]
    by simp
qed

lemma exp_upper_bound_case_5:
  fixes x::real
  assumes "x  6.36"
  shows "exp x  21743271936 / (-(x^3) + 12*x^2 - 96*x + 384)^4"
proof -
  have "(1/384)*(-(x^3) + 12*x^2 - 96*x + 384) = (1 + (-x/4) + (1/2)*(-x/4)^2 + (1/6)*(-x/4)^3)"
    by (simp add: field_simps power2_eq_square power3_eq_cube)
  also have "...  exp (-x/4)"
    by (rule exp_lower_taylor_2)
  finally have 1: "(1/384)*(-(x^3) + 12*x^2 - 96*x + 384)  exp (-x/4)" .
  have "(-(x^3) + 12*x^2 - 96*x + 384)^4 / 21743271936 = ((1/384)*(-(x^3) + 12*x^2 - 96*x + 384))^4"
    by (simp add: divide_simps)
  also have "...  (exp (-x/4))^4"
    apply (rule power_mono [OF 1])
    apply (simp add: algebra_simps)
    using assms
    apply (sos "((R<1 + ((R<1 * ((R<1777/32 * [~539/3554*x + 1]^2) + (R<907/227456 * [x]^2))) + (((A<0 * R<1) * (R<25/1024 * [1]^2)) + ((A<=0 * R<1) * ((R<49/32 * [~2/49*x + 1]^2) + (R<45/1568 * [x]^2)))))))")
    done
  also have "... = inverse (exp x)"
    by (simp add: exp_of_nat_mult [symmetric] exp_minus [symmetric])
  finally have 2: "(-(x^3) + 12*x^2 - 96*x + 384)^4 / 21743271936  inverse (exp x)" .
  have "12 * x2 - x ^ 3 - 96 * x + 384  0" using assms
    by (sos "((R<1 + (([~25/32] * A=0) + ((R<1 * ((R<1777/32 * [~539/3554*x + 1]^2) + (R<907/227456 * [x]^2))) + ((A<=0 * R<1) * ((R<49/32 * [~2/49*x + 1]^2) + (R<45/1568 * [x]^2)))))))")
  then show ?thesis
    using Fields.linordered_field_class.le_imp_inverse_le [OF 2]
    by simp
qed


section ‹Continued Fraction Bound 2›

definition exp_cf2 :: "real  real"
  where "exp_cf2  λx. (x^2 + 6*x + 12) / (x^2 - 6*x + 12)"

lemma denom_cf2_pos: fixes x::real shows "x2 - 6 * x + 12 > 0"
  by (sos "((R<1 + ((R<1 * ((R<5 * [~3/10*x + 1]^2) + (R<1/20 * [x]^2))) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))")

lemma numer_cf2_pos: fixes x::real shows "x2 + 6 * x + 12 > 0"
  by (sos "((R<1 + ((R<1 * ((R<5 * [3/10*x + 1]^2) + (R<1/20 * [x]^2))) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))")

lemma exp_cf2_pos: "exp_cf2 x > 0"
  unfolding exp_cf2_def
  by (auto simp add: divide_simps denom_cf2_pos numer_cf2_pos)

definition diff_delta_lnexp_cf2 :: "real  real"
  where "diff_delta_lnexp_cf2  λx. - (x^4) / ((x^2 - 6*x + 12) * (x^2 + 6*x + 12))"

lemma d_delta_lnexp_cf2_nonpos: "diff_delta_lnexp_cf2 x  0"
unfolding diff_delta_lnexp_cf2_def
by (sos "(((R<1 + ((R<1 * ((R<5/4 * [~3/40*x^2 + 1]^2) + (R<11/1280 * [x^2]^2))) +
      ((A<1 * R<1) * (R<1/64 * [1]^2))))) & ((R<1 + ((R<1 * ((R<5/4 * [~3/40*x^2 + 1]^2) + (R<11/1280 * [x^2]^2))) + ((A<1 * R<1) * (R<1/64 * [1]^2))))))")

lemma d_delta_lnexp_cf2:
    "((λx. ln (exp_cf2 x) - x) has_field_derivative diff_delta_lnexp_cf2 x) (at x)"
  unfolding exp_cf2_def diff_delta_lnexp_cf2_def
  apply (intro derivative_eq_intros | simp)+
  apply (metis exp_cf2_def exp_cf2_pos)
  apply (simp_all add: )
  using denom_cf2_pos [of x] numer_cf2_pos [of x]
  apply (auto simp: divide_simps)
  apply algebra
  done

text‹Upper bound for non-positive x›
lemma ln_exp_cf2_upper_bound_neg:
  assumes "x  0"
    shows "x  ln (exp_cf2 x)"
  by (rule gen_upper_bound_decreasing [OF assms d_delta_lnexp_cf2 d_delta_lnexp_cf2_nonpos])
     (simp add: exp_cf2_def)

theorem exp_cf2_upper_bound_neg: "x0  exp(x)  exp_cf2 x"
  by (metis ln_exp_cf2_upper_bound_neg exp_cf2_pos exp_le_cancel_iff exp_ln_iff)

text‹Lower bound for non-negative x›
lemma ln_exp_cf2_lower_bound_pos:
  assumes "0x"
    shows "ln (exp_cf2 x)  x"
  by (rule gen_lower_bound_increasing [OF assms d_delta_lnexp_cf2 d_delta_lnexp_cf2_nonpos])
     (simp add: exp_cf2_def)

theorem exp_cf2_lower_bound_pos: "0x  exp_cf2 x  exp x"
  by (metis exp_cf2_pos exp_le_cancel_iff exp_ln ln_exp_cf2_lower_bound_pos)


section ‹Continued Fraction Bound 3›

text‹This bound crosses the X-axis twice, causing complications.›

definition numer_cf3 :: "real  real"
  where "numer_cf3  λx. x^3 + 12*x^2 + 60*x + 120"

definition exp_cf3 :: "real  real"
  where "exp_cf3  λx. numer_cf3 x / numer_cf3 (-x)"

lemma numer_cf3_pos: "-4.64  x  numer_cf3 x > 0"
  unfolding numer_cf3_def
  by sturm

lemma exp_cf3_pos: "numer_cf3 x > 0  numer_cf3 (-x) > 0  exp_cf3 x > 0"
  by (simp add: exp_cf3_def)

definition diff_delta_lnexp_cf3 :: "real  real"
  where "diff_delta_lnexp_cf3  λx. (x^6) / (numer_cf3 (-x) * numer_cf3 x)"

lemma d_delta_lnexp_cf3_nonneg: "numer_cf3 x > 0  numer_cf3 (-x) > 0  diff_delta_lnexp_cf3 x  0"
  unfolding diff_delta_lnexp_cf3_def
  by (auto simp: mult_less_0_iff intro: divide_nonneg_neg)

lemma d_delta_lnexp_cf3:
  assumes "numer_cf3 x > 0" "numer_cf3 (-x) > 0"
  shows "((λx. ln (exp_cf3 x) - x) has_field_derivative diff_delta_lnexp_cf3 x) (at x)"
unfolding exp_cf3_def numer_cf3_def diff_delta_lnexp_cf3_def
apply (intro derivative_eq_intros | simp)+
using assms numer_cf3_pos [of x] numer_cf3_pos [of "-x"]
apply (auto simp: numer_cf3_def)
apply (auto simp add: divide_simps add_nonneg_eq_0_iff)
apply algebra
done

lemma numer_cf3_mono: "y  x  numer_cf3 y  numer_cf3 x"
  unfolding numer_cf3_def
  by (sos "(((A<0 * R<1) + ((A<=0 * R<1) * ((R<60 * [1/10*x + 1/10*y + 1]^2) +
                ((R<2/5 * [x + ~1/4*y]^2) + (R<3/8 * [y]^2))))))")

text‹Upper bound for non-negative x›
lemma ln_exp_cf3_upper_bound_nonneg:
  assumes x0: "0  x" and xless: "numer_cf3 (-x) > 0"
    shows "x  ln (exp_cf3 x)"
proof -
  have ncf3: "y. 0  y  y  x  numer_cf3 (-y) > 0"
    by (metis neg_le_iff_le numer_cf3_mono order.strict_trans2 xless)
  show ?thesis
    apply (rule gen_upper_bound_increasing [OF x0 d_delta_lnexp_cf3 d_delta_lnexp_cf3_nonneg])
    apply (auto simp add: ncf3 assms numer_cf3_pos)
    apply (simp add: exp_cf3_def numer_cf3_def)
    done
qed

theorem exp_cf3_upper_bound_pos: "0  x  numer_cf3 (-x) > 0  exp x  exp_cf3 x"
  using ln_exp_cf3_upper_bound_nonneg [of x] exp_cf3_pos [of x] numer_cf3_pos [of x]
  by auto (metis exp_le_cancel_iff exp_ln_iff)

corollary "0  x  x  4.64  exp x  exp_cf3 x"
  by (metis numer_cf3_pos neg_le_iff_le exp_cf3_upper_bound_pos)


text‹Lower bound for negative x, provided @{term"exp_cf3 x > 0"}]›
lemma ln_exp_cf3_lower_bound_neg:
  assumes x0: "x  0" and xgtr: "numer_cf3 x > 0"
    shows "ln (exp_cf3 x)  x"
proof -
  have ncf3: "y. x  y  y  0  numer_cf3 y > 0"
    by (metis dual_order.strict_trans1 numer_cf3_mono xgtr)
  show ?thesis
    apply (rule gen_lower_bound_decreasing [OF x0 d_delta_lnexp_cf3 d_delta_lnexp_cf3_nonneg])
    apply (auto simp add: ncf3 assms numer_cf3_pos)
    apply (simp add: exp_cf3_def numer_cf3_def)
    done
qed

theorem exp_cf3_lower_bound_pos:
  assumes "x  0" shows "exp_cf3 x  exp x"
proof (cases "numer_cf3 x > 0")
  case True
  then have "exp_cf3 x > 0"
    using assms numer_cf3_pos [of "-x"]
    by (auto simp: exp_cf3_pos)
  then show ?thesis
  using ln_exp_cf3_lower_bound_neg [of x] assms True
    by auto (metis exp_le_cancel_iff exp_ln_iff)
next
  case False
  then have "exp_cf3 x  0"
    using assms numer_cf3_pos [of "-x"]
    unfolding exp_cf3_def
    by (simp add: divide_nonpos_pos)
  then show ?thesis
    by (metis exp_ge_zero order.trans)
qed


section ‹Continued Fraction Bound 4›

text ‹Here we have the extended exp continued fraction bounds›

definition numer_cf4 :: "real  real"
  where "numer_cf4  λx. x^4 + 20*x^3 + 180*x^2 + 840*x + 1680"

definition exp_cf4 :: "real  real"
  where "exp_cf4  λx. numer_cf4 x / numer_cf4 (-x)"

lemma numer_cf4_pos: fixes x::real shows "numer_cf4 x > 0"
unfolding numer_cf4_def
by (sos "((R<1 + ((R<1 * ((R<4469/256 * [1135/71504*x^2 + 4725/17876*x + 1]^2) + ((R<3728645/18305024 * [536265/2982916*x^2 + x]^2) + (R<106265/24436047872 * [x^2]^2)))) + ((A<=0 * R<1) * (R<45/4096 * [1]^2)))))")

lemma exp_cf4_pos: "exp_cf4 x > 0"
  unfolding exp_cf4_def
  by (auto simp add: divide_simps numer_cf4_pos)

definition diff_delta_lnexp_cf4 :: "real  real"
  where "diff_delta_lnexp_cf4  λx. - (x^8) / (numer_cf4 (-x) * numer_cf4 x)"

lemma d_delta_lnexp_cf4_nonpos: "diff_delta_lnexp_cf4 x  0"
  unfolding diff_delta_lnexp_cf4_def
  using numer_cf4_pos [of x] numer_cf4_pos [of "-x"]
  by (simp add: zero_le_divide_iff zero_le_mult_iff)

lemma d_delta_lnexp_cf4:
    "((λx. ln (exp_cf4 x) - x) has_field_derivative diff_delta_lnexp_cf4 x) (at x)"
  unfolding exp_cf4_def numer_cf4_def diff_delta_lnexp_cf4_def
  apply (intro derivative_eq_intros | simp)+
  using exp_cf4_pos
  apply (simp add: exp_cf4_def numer_cf4_def)
  apply (simp_all add: )
  using numer_cf4_pos [of x]  numer_cf4_pos [of "-x"]
  apply (auto simp: divide_simps numer_cf4_def)
  apply algebra
  done

text‹Upper bound for non-positive x›
lemma ln_exp_cf4_upper_bound_neg:
  assumes "x  0"
    shows "x  ln (exp_cf4 x)"
  by (rule gen_upper_bound_decreasing [OF assms d_delta_lnexp_cf4 d_delta_lnexp_cf4_nonpos])
     (simp add: exp_cf4_def numer_cf4_def)

theorem exp_cf4_upper_bound_neg: "x0  exp(x)  exp_cf4 x"
  by (metis ln_exp_cf4_upper_bound_neg exp_cf4_pos exp_le_cancel_iff exp_ln_iff)

text‹Lower bound for non-negative x›
lemma ln_exp_cf4_lower_bound_pos:
  assumes "0x"
    shows "ln (exp_cf4 x)  x"
  by (rule gen_lower_bound_increasing [OF assms d_delta_lnexp_cf4 d_delta_lnexp_cf4_nonpos])
     (simp add: exp_cf4_def numer_cf4_def)

theorem exp_cf4_lower_bound_pos: "0x  exp_cf4 x  exp x"
  by (metis exp_cf4_pos exp_le_cancel_iff exp_ln ln_exp_cf4_lower_bound_pos)


section ‹Continued Fraction Bound 5›

text‹This bound crosses the X-axis twice, causing complications.›

definition numer_cf5 :: "real  real"
  where "numer_cf5  λx. x^5 + 30*x^4 + 420*x^3 + 3360*x^2 + 15120*x + 30240"

definition exp_cf5 :: "real  real"
  where "exp_cf5  λx. numer_cf5 x / numer_cf5 (-x)"

lemma numer_cf5_pos: "-7.293  x  numer_cf5 x > 0"
  unfolding numer_cf5_def
  by sturm

lemma exp_cf5_pos: "numer_cf5 x > 0  numer_cf5 (-x) > 0  exp_cf5 x > 0"
  unfolding exp_cf5_def numer_cf5_def
  by (simp add: divide_neg_neg)

definition diff_delta_lnexp_cf5 :: "real  real"
  where "diff_delta_lnexp_cf5  λx. (x^10) / (numer_cf5 (-x) * numer_cf5 x)"

lemma d_delta_lnexp_cf5_nonneg: "numer_cf5 x > 0  numer_cf5 (-x) > 0  diff_delta_lnexp_cf5 x  0"
  unfolding diff_delta_lnexp_cf5_def
  by (auto simp add: mult_less_0_iff intro: divide_nonneg_neg )

lemma d_delta_lnexp_cf5:
  assumes "numer_cf5 x > 0" "numer_cf5 (-x) > 0"
  shows "((λx. ln (exp_cf5 x) - x) has_field_derivative diff_delta_lnexp_cf5 x) (at x)"
unfolding exp_cf5_def numer_cf5_def diff_delta_lnexp_cf5_def
apply (intro derivative_eq_intros | simp)+
using assms numer_cf5_pos [of x] numer_cf5_pos [of "-x"]
apply (auto simp: numer_cf5_def)
apply (auto simp add: divide_simps add_nonneg_eq_0_iff)
apply algebra
done

subsection‹Proving monotonicity via a non-negative derivative›

definition numer_cf5_deriv :: "real  real"
  where "numer_cf5_deriv  λx. 5*x^4 + 120*x^3 + 1260*x^2 + 6720*x + 15120"

lemma numer_cf5_deriv:
  shows "(numer_cf5 has_field_derivative numer_cf5_deriv x) (at x)"
  unfolding numer_cf5_def numer_cf5_deriv_def
  by (intro derivative_eq_intros | simp)+

lemma numer_cf5_deriv_pos: "numer_cf5_deriv x  0"
  unfolding numer_cf5_deriv_def
  by (sos "((R<1 + ((R<1 * ((R<185533/8192 * [73459/5937056*x^2 + 43050/185533*x + 1]^2) + ((R<4641265253/24318181376 * [700850925/4641265253*x^2 + x]^2) + (R<38142496079/38933754831437824 * [x^2]^2)))) + ((A<0 * R<1) * (R<205/131072 * [1]^2)))))")

lemma numer_cf5_mono: "y  x  numer_cf5 y  numer_cf5 x"
  by (auto intro: DERIV_nonneg_imp_nondecreasing numer_cf5_deriv numer_cf5_deriv_pos)

subsection‹Results›

text‹Upper bound for non-negative x›
lemma ln_exp_cf5_upper_bound_nonneg:
  assumes x0: "0  x" and xless: "numer_cf5 (-x) > 0"
    shows "x  ln (exp_cf5 x)"
proof -
  have ncf5: "y. 0  y  y  x  numer_cf5 (-y) > 0"
    by (metis neg_le_iff_le numer_cf5_mono order.strict_trans2 xless)
  show ?thesis
    apply (rule gen_upper_bound_increasing [OF x0 d_delta_lnexp_cf5 d_delta_lnexp_cf5_nonneg])
    apply (auto simp add: ncf5 assms numer_cf5_pos)
    apply (simp add: exp_cf5_def numer_cf5_def)
    done
qed

theorem exp_cf5_upper_bound_pos: "0  x  numer_cf5 (-x) > 0  exp x  exp_cf5 x"
  using ln_exp_cf5_upper_bound_nonneg [of x] exp_cf5_pos [of x] numer_cf5_pos [of x]
  by auto (metis exp_le_cancel_iff exp_ln_iff)

corollary "0  x  x  7.293  exp x  exp_cf5 x"
  by (metis neg_le_iff_le numer_cf5_pos exp_cf5_upper_bound_pos)

text‹Lower bound for negative x, provided @{term"exp_cf5 x > 0"}]›
lemma ln_exp_cf5_lower_bound_neg:
  assumes x0: "x  0" and xgtr: "numer_cf5 x > 0"
    shows "ln (exp_cf5 x)  x"
proof -
  have ncf5: "y. x  y  y  0  numer_cf5 y > 0"
    by (metis dual_order.strict_trans1 numer_cf5_mono xgtr)
  show ?thesis
    apply (rule gen_lower_bound_decreasing [OF x0 d_delta_lnexp_cf5 d_delta_lnexp_cf5_nonneg])
    apply (auto simp add: ncf5 assms numer_cf5_pos)
    apply (simp add: exp_cf5_def numer_cf5_def)
    done
qed

theorem exp_cf5_lower_bound_pos:
  assumes "x  0" shows "exp_cf5 x  exp x"
proof (cases "numer_cf5 x > 0")
  case True
  then have "exp_cf5 x > 0"
    using assms numer_cf5_pos [of "-x"]
    by (auto simp: exp_cf5_pos)
  then show ?thesis
  using ln_exp_cf5_lower_bound_neg [of x] assms True
    by auto (metis exp_le_cancel_iff exp_ln_iff)
next
  case False
  then have "exp_cf5 x  0"
    using assms numer_cf5_pos [of "-x"]
    unfolding exp_cf5_def numer_cf5_def
    by (simp add: divide_nonpos_pos)
  then show ?thesis
    by (metis exp_ge_zero order.trans)
qed


section ‹Continued Fraction Bound 6›

definition numer_cf6 :: "real  real"
  where "numer_cf6  λx. x^6 + 42*x^5 + 840*x^4 + 10080*x^3 + 75600*x^2 + 332640*x + 665280"

definition exp_cf6 :: "real  real"
  where "exp_cf6  λx. numer_cf6 x / numer_cf6 (-x)"

lemma numer_cf6_pos: fixes x::real shows "numer_cf6 x > 0"
  unfolding numer_cf6_def
  by sturm

lemma exp_cf6_pos: "exp_cf6 x > 0"
  unfolding exp_cf6_def
  by (auto simp add: divide_simps numer_cf6_pos)

definition diff_delta_lnexp_cf6 :: "real  real"
  where "diff_delta_lnexp_cf6  λx. - (x^12) / (numer_cf6 (-x) * numer_cf6 x)"

lemma d_delta_lnexp_cf6_nonpos: "diff_delta_lnexp_cf6 x  0"
  unfolding diff_delta_lnexp_cf6_def
  using numer_cf6_pos [of x]  numer_cf6_pos [of "-x"]
  by (simp add: zero_le_divide_iff zero_le_mult_iff)

lemma d_delta_lnexp_cf6:
    "((λx. ln (exp_cf6 x) - x) has_field_derivative diff_delta_lnexp_cf6 x) (at x)"
  unfolding exp_cf6_def diff_delta_lnexp_cf6_def numer_cf6_def
  apply (intro derivative_eq_intros | simp)+
  using exp_cf6_pos
  apply (simp add: exp_cf6_def numer_cf6_def)
  apply (simp_all add: )
  using numer_cf6_pos [of x]  numer_cf6_pos [of "-x"]
  apply (auto simp: divide_simps numer_cf6_def)
  apply algebra
  done

text‹Upper bound for non-positive x›
lemma ln_exp_cf6_upper_bound_neg:
  assumes "x  0"
    shows "x  ln (exp_cf6 x)"
  by (rule gen_upper_bound_decreasing [OF assms d_delta_lnexp_cf6 d_delta_lnexp_cf6_nonpos])
     (simp add: exp_cf6_def numer_cf6_def)

theorem exp_cf6_upper_bound_neg: "x0  exp(x)  exp_cf6 x"
  by (metis ln_exp_cf6_upper_bound_neg exp_cf6_pos exp_le_cancel_iff exp_ln_iff)

text‹Lower bound for non-negative x›
lemma ln_exp_cf6_lower_bound_pos:
  assumes "0x"
    shows "ln (exp_cf6 x)  x"
  by (rule gen_lower_bound_increasing [OF assms d_delta_lnexp_cf6 d_delta_lnexp_cf6_nonpos])
     (simp add: exp_cf6_def numer_cf6_def)

theorem exp_cf6_lower_bound_pos: "0x  exp_cf6 x  exp x"
  by (metis exp_cf6_pos exp_le_cancel_iff exp_ln ln_exp_cf6_lower_bound_pos)

  
section ‹Continued Fraction Bound 7›

text‹This bound crosses the X-axis twice, causing complications.›

definition numer_cf7 :: "real  real"
  where "numer_cf7  λx. x^7 + 56*x^6 + 1512*x^5 + 25200*x^4 + 277200*x^3 + 1995840*x^2 + 8648640*x + 17297280"

definition exp_cf7 :: "real  real"
  where "exp_cf7  λx. numer_cf7 x / numer_cf7 (-x)"

lemma numer_cf7_pos: "-9.943  x  numer_cf7 x > 0"
  unfolding numer_cf7_def
  by sturm

lemma exp_cf7_pos: "numer_cf7 x > 0  numer_cf7 (-x) > 0  exp_cf7 x > 0"
  by (simp add: exp_cf7_def)

definition diff_delta_lnexp_cf7 :: "real  real"
  where "diff_delta_lnexp_cf7  λx. (x^14) / (numer_cf7 (-x) * numer_cf7 x)"

lemma d_delta_lnexp_cf7_nonneg: "numer_cf7 x > 0  numer_cf7 (-x) > 0  diff_delta_lnexp_cf7 x  0"
  unfolding diff_delta_lnexp_cf7_def
  by (auto simp: mult_less_0_iff intro: divide_nonneg_neg)

lemma d_delta_lnexp_cf7:
  assumes "numer_cf7 x > 0" "numer_cf7 (-x) > 0"
  shows "((λx. ln (exp_cf7 x) - x) has_field_derivative diff_delta_lnexp_cf7 x) (at x)"
unfolding exp_cf7_def numer_cf7_def diff_delta_lnexp_cf7_def
apply (intro derivative_eq_intros | simp)+
using assms numer_cf7_pos [of x] numer_cf7_pos [of "-x"]
apply (auto simp: numer_cf7_def)
apply (auto simp: divide_simps add_nonneg_eq_0_iff)
apply algebra
done

subsection‹Proving monotonicity via a non-negative derivative›

definition numer_cf7_deriv :: "real  real"
  where "numer_cf7_deriv  λx. 7*x^6 + 336*x^5 + 7560*x^4 + 100800*x^3 + 831600*x^2 + 3991680*x + 8648640"

lemma numer_cf7_deriv:
  shows "(numer_cf7 has_field_derivative numer_cf7_deriv x) (at x)"
  unfolding numer_cf7_def numer_cf7_deriv_def
  by (intro derivative_eq_intros | simp)+

lemma numer_cf7_deriv_pos: "numer_cf7_deriv x  0"
  unfolding numer_cf7_deriv_def
  apply (rule order.strict_implies_order)  ― ‹FIXME should not be necessary›
  by sturm

lemma numer_cf7_mono: "y  x  numer_cf7 y  numer_cf7 x"
  by (auto intro: DERIV_nonneg_imp_nondecreasing numer_cf7_deriv numer_cf7_deriv_pos)

subsection‹Results›

text‹Upper bound for non-negative x›
lemma ln_exp_cf7_upper_bound_nonneg:
  assumes x0: "0  x" and xless: "numer_cf7 (-x) > 0"
    shows "x  ln (exp_cf7 x)"
proof -
  have ncf7: "y. 0  y  y  x  numer_cf7 (-y) > 0"
    by (metis neg_le_iff_le numer_cf7_mono order.strict_trans2 xless)
  show ?thesis
    apply (rule gen_upper_bound_increasing [OF x0 d_delta_lnexp_cf7 d_delta_lnexp_cf7_nonneg])
    apply (auto simp add: ncf7 assms numer_cf7_pos)
    apply (simp add: exp_cf7_def numer_cf7_def)
    done
qed

theorem exp_cf7_upper_bound_pos: "0  x  numer_cf7 (-x) > 0  exp x  exp_cf7 x"
  using ln_exp_cf7_upper_bound_nonneg [of x] exp_cf7_pos [of x] numer_cf7_pos [of x]
  by auto (metis exp_le_cancel_iff exp_ln_iff)

corollary "0  x  x  9.943  exp x  exp_cf7 x"
  by (metis neg_le_iff_le numer_cf7_pos exp_cf7_upper_bound_pos)

text‹Lower bound for negative x, provided @{term"exp_cf7 x > 0"}]›
lemma ln_exp_cf7_lower_bound_neg:
  assumes x0: "x  0" and xgtr: "numer_cf7 x > 0"
    shows "ln (exp_cf7 x)  x"
proof -
  have ncf7: "y. x  y  y  0  numer_cf7 y > 0"
    by (metis dual_order.strict_trans1 numer_cf7_mono xgtr)
  show ?thesis
    apply (rule gen_lower_bound_decreasing [OF x0 d_delta_lnexp_cf7 d_delta_lnexp_cf7_nonneg])
    apply (auto simp add: ncf7 assms numer_cf7_pos)
    apply (simp add: exp_cf7_def numer_cf7_def)
    done
qed

theorem exp_cf7_lower_bound_pos:
  assumes "x  0" shows "exp_cf7 x  exp x"
proof (cases "numer_cf7 x > 0")
  case True
  then have "exp_cf7 x > 0"
    using assms numer_cf7_pos [of "-x"]
    by (auto simp: exp_cf7_pos)
  then show ?thesis
  using ln_exp_cf7_lower_bound_neg [of x] assms True
    by auto (metis exp_le_cancel_iff exp_ln_iff)
next
  case False
  then have "exp_cf7 x  0"
    using assms numer_cf7_pos [of "-x"]
    unfolding exp_cf7_def
    by (simp add: divide_nonpos_pos)
  then show ?thesis
    by (metis exp_ge_zero order.trans)
qed

end

Theory Log_CF_Bounds

chapter ‹Log Upper and Lower Bounds›

theory Log_CF_Bounds
imports Bounds_Lemmas

begin

theorem ln_upper_1: "0<x  ln(x::real)  x - 1"
by (rule ln_le_minus_one)

definition ln_lower_1 :: "real  real"
  where "ln_lower_1  λx. 1 - (inverse x)"

corollary ln_lower_1: "0<x  ln_lower_1 x  ln x"
  unfolding ln_lower_1_def
  by (metis ln_inverse ln_le_minus_one positive_imp_inverse_positive minus_diff_eq minus_le_iff)

theorem ln_lower_1_eq: "0<x  ln_lower_1 x = (x - 1)/x"
  by (auto simp: ln_lower_1_def divide_simps)

section ‹Upper Bound 3›

definition ln_upper_3 :: "real  real"
  where "ln_upper_3  λx. (x + 5)*(x - 1) / (2*(2*x + 1))"

definition diff_delta_ln_upper_3 :: "real  real"
  where "diff_delta_ln_upper_3  λx. (x - 1)^3 / ((2*x + 1)^2 * x)"

lemma d_delta_ln_upper_3: "x > 0 
    ((λx. ln_upper_3 x - ln x) has_field_derivative diff_delta_ln_upper_3 x) (at x)"
unfolding ln_upper_3_def diff_delta_ln_upper_3_def
apply (intro derivative_eq_intros | simp)+
apply (simp add: divide_simps add_nonneg_eq_0_iff, algebra)
done

text‹Strict inequalities also possible›
lemma ln_upper_3_pos:
  assumes "1  x" shows "ln(x)  ln_upper_3 x"
apply (rule gen_upper_bound_increasing [OF assms d_delta_ln_upper_3])
apply (auto simp: diff_delta_ln_upper_3_def ln_upper_3_def)
done

lemma ln_upper_3_neg:
  assumes "0 < x" and x1: "x  1" shows "ln(x)  ln_upper_3 x"
apply (rule gen_upper_bound_decreasing [OF x1 d_delta_ln_upper_3])
using assms
apply (auto simp: diff_delta_ln_upper_3_def divide_simps ln_upper_3_def)
done

theorem ln_upper_3: "0<x  ln(x)  ln_upper_3 x"
by (metis le_less_linear less_eq_real_def ln_upper_3_neg ln_upper_3_pos)

definition ln_lower_3 :: "real  real"
  where "ln_lower_3  λx. - ln_upper_3 (inverse x)"

corollary ln_lower_3: "0<x  ln_lower_3 x  ln x"
  unfolding ln_lower_3_def
  by (metis ln_inverse inverse_positive_iff_positive minus_le_iff ln_upper_3)

theorem ln_lower_3_eq: "0<x  ln_lower_3 x = (1/2)*(1 + 5*x)*(x - 1) / (x*(2 + x))"
  unfolding ln_lower_3_def ln_upper_3_def
  by (simp add: divide_simps) algebra


section ‹Upper Bound 5›

definition ln_upper_5 :: "real  real"
  where "ln_upper_5 x  (x^2 + 19*x + 10)*(x - 1) / (3*(3*x^2 + 6*x + 1))"

definition diff_delta_ln_upper_5 :: "real  real"
  where "diff_delta_ln_upper_5  λx. (x - 1)^5 / ((3*x^2 + 6*x + 1)^2*x)"

lemma d_delta_ln_upper_5: "x > 0 
    ((λx. ln_upper_5 x - ln x) has_field_derivative diff_delta_ln_upper_5 x) (at x)"
  unfolding ln_upper_5_def diff_delta_ln_upper_5_def
  apply (intro derivative_eq_intros | simp add: add_nonneg_eq_0_iff)+
  apply (simp add: divide_simps add_nonneg_eq_0_iff, algebra)
  done

lemma ln_upper_5_pos:
  assumes "1  x" shows "ln(x)  ln_upper_5 x"
apply (rule gen_upper_bound_increasing [OF assms d_delta_ln_upper_5])
apply (auto simp: diff_delta_ln_upper_5_def ln_upper_5_def)
done

lemma ln_upper_5_neg:
  assumes "0 < x" and x1: "x  1" shows "ln(x)  ln_upper_5 x"
apply (rule gen_upper_bound_decreasing [OF x1 d_delta_ln_upper_5])
using assms
apply (auto simp: diff_delta_ln_upper_5_def divide_simps ln_upper_5_def mult_less_0_iff)
done

theorem ln_upper_5: "0<x  ln(x)  ln_upper_5 x"
by (metis le_less_linear less_eq_real_def ln_upper_5_neg ln_upper_5_pos)

definition ln_lower_5 :: "real  real"
  where "ln_lower_5  λx. - ln_upper_5 (inverse x)"

corollary ln_lower_5: "0<x  ln_lower_5 x  ln x"
  unfolding ln_lower_5_def
  by (metis ln_inverse inverse_positive_iff_positive minus_le_iff ln_upper_5)

theorem ln_lower_5_eq: "0<x 
    ln_lower_5 x = (1/3)*(10*x^2 + 19*x + 1)*(x - 1) / (x*(x^2 + 6*x + 3))"
  unfolding ln_lower_5_def ln_upper_5_def
  by (simp add: zero_less_mult_iff add_pos_pos dual_order.strict_implies_not_eq divide_simps)
     algebra


section ‹Upper Bound 7›

definition ln_upper_7 :: "real  real"
  where "ln_upper_7 x  (3*x^3 + 131*x^2 + 239*x + 47)*(x - 1) / (12*(4*x^3 + 18*x^2 + 12*x + 1))"

definition diff_delta_ln_upper_7 :: "real  real"
  where "diff_delta_ln_upper_7  λx. (x - 1)^7 / ((4*x^3 + 18*x^2 + 12*x + 1)^2 * x)"

lemma d_delta_ln_upper_7: "x > 0 
    ((λx. ln_upper_7 x - ln x) has_field_derivative diff_delta_ln_upper_7 x) (at x)"
unfolding ln_upper_7_def diff_delta_ln_upper_7_def
apply (intro derivative_eq_intros | simp)+
apply auto
apply (auto simp: add_pos_pos dual_order.strict_implies_not_eq divide_simps, algebra)
done

lemma ln_upper_7_pos:
  assumes "1  x" shows "ln(x)  ln_upper_7 x"
apply (rule gen_upper_bound_increasing [OF assms d_delta_ln_upper_7])
apply (auto simp: diff_delta_ln_upper_7_def ln_upper_7_def)
done

lemma ln_upper_7_neg:
  assumes "0 < x" and x1: "x  1" shows "ln(x)  ln_upper_7 x"
apply (rule gen_upper_bound_decreasing [OF x1 d_delta_ln_upper_7])
using assms
apply (auto simp: diff_delta_ln_upper_7_def divide_simps ln_upper_7_def mult_less_0_iff)
done

theorem ln_upper_7: "0 < x  ln(x)  ln_upper_7 x"
  by (metis le_less_linear less_eq_real_def ln_upper_7_neg ln_upper_7_pos)

definition ln_lower_7 :: "real  real"
  where "ln_lower_7  λx. - ln_upper_7 (inverse x)"

corollary ln_lower_7: "0 < x  ln_lower_7 x  ln x"
  unfolding ln_lower_7_def
  by (metis ln_inverse inverse_positive_iff_positive minus_le_iff ln_upper_7)

theorem ln_lower_7_eq: "0 < x 
  ln_lower_7 x = (1/12)*(47*x^3 + 239*x^2 + 131*x + 3)*(x - 1) / (x*(x^3 + 12*x^2 + 18*x + 4))"
  unfolding ln_lower_7_def ln_upper_7_def
  by (simp add: zero_less_mult_iff add_pos_pos dual_order.strict_implies_not_eq divide_simps)
     algebra


section ‹Upper Bound 9›

definition ln_upper_9 :: "real  real"
  where "ln_upper_9 x  (6*x^4 + 481*x^3 + 1881*x^2 + 1281*x + 131)*(x - 1) /
                         (30 * (5*x^4 + 40*x^3 + 60*x^2 + 20*x + 1))"

definition diff_delta_ln_upper_9 :: "real  real"
  where "diff_delta_ln_upper_9  λx. (x - 1)^9 / (((5*x^4 + 40*x^3 + 60*x^2 + 20*x + 1)^2) * x)"

lemma d_delta_ln_upper_9: "x > 0 
    ((λx. ln_upper_9 x - ln x) has_field_derivative diff_delta_ln_upper_9 x) (at x)"
unfolding ln_upper_9_def diff_delta_ln_upper_9_def
apply (intro derivative_eq_intros | simp)+
apply auto
apply (auto simp: add_pos_pos dual_order.strict_implies_not_eq divide_simps, algebra)
done

lemma ln_upper_9_pos:
  assumes "1  x" shows "ln(x)  ln_upper_9 x"
apply (rule gen_upper_bound_increasing [OF assms d_delta_ln_upper_9])
apply (auto simp: diff_delta_ln_upper_9_def ln_upper_9_def)
done

lemma ln_upper_9_neg:
  assumes "0 < x" and x1: "x  1" shows "ln(x)  ln_upper_9 x"
apply (rule gen_upper_bound_decreasing [OF x1 d_delta_ln_upper_9])
using assms
apply (auto simp: diff_delta_ln_upper_9_def divide_simps ln_upper_9_def mult_less_0_iff)
done

theorem ln_upper_9: "0<x  ln(x)  ln_upper_9 x"
by (metis le_less_linear less_eq_real_def ln_upper_9_neg ln_upper_9_pos)


definition ln_lower_9 :: "real  real"
  where "ln_lower_9  λx. - ln_upper_9 (inverse x)"

corollary ln_lower_9: "0 < x  ln_lower_9 x  ln x"
  unfolding ln_lower_9_def
  by (metis ln_inverse inverse_positive_iff_positive minus_le_iff ln_upper_9)

theorem ln_lower_9_eq: "0 < x 
      ln_lower_9 x = (1/30)*(6 + 481*x + 1881*x^2 + 1281*x^3 + 131*x^4)*(x - 1) /
                     (x*(5 + 40*x + 60*x^2 + 20*x^3 + x^4))"
  unfolding ln_lower_9_def ln_upper_9_def
  by (simp add: zero_less_mult_iff add_pos_pos dual_order.strict_implies_not_eq divide_simps)
     algebra


section ‹Upper Bound 11›

text‹Extended bounds start here›

definition ln_upper_11 :: "real  real"
  where "ln_upper_11 x 
           (5*x^5 + 647*x^4 + 4397*x^3 + 6397*x^2 + 2272*x + 142) * (x - 1) /
           (30*(6*x^5 + 75*x^4 + 200*x^3 + 150*x^2 + 30*x + 1))"

definition diff_delta_ln_upper_11 :: "real  real"
  where "diff_delta_ln_upper_11  λx. (x - 1)^11 / ((6*x^5 + 75*x^4 + 200*x^3 + 150*x^2 + 30*x + 1)^2 * x)"

lemma d_delta_ln_upper_11: "x > 0 
    ((λx. ln_upper_11 x - ln x) has_field_derivative diff_delta_ln_upper_11 x) (at x)"
unfolding ln_upper_11_def diff_delta_ln_upper_11_def
apply (intro derivative_eq_intros | simp)+
apply auto
apply (auto simp: add_pos_pos dual_order.strict_implies_not_eq divide_simps, algebra)
done

lemma ln_upper_11_pos:
  assumes "1  x" shows "ln(x)  ln_upper_11 x"
apply (rule gen_upper_bound_increasing [OF assms d_delta_ln_upper_11])
apply (auto simp: diff_delta_ln_upper_11_def ln_upper_11_def)
done

lemma ln_upper_11_neg:
  assumes "0 < x" and x1: "x  1" shows "ln(x)  ln_upper_11 x"
apply (rule gen_upper_bound_decreasing [OF x1 d_delta_ln_upper_11])
using assms
apply (auto simp: diff_delta_ln_upper_11_def divide_simps ln_upper_11_def mult_less_0_iff)
done

theorem ln_upper_11: "0<x  ln(x)  ln_upper_11 x"
by (metis le_less_linear less_eq_real_def ln_upper_11_neg ln_upper_11_pos)

definition ln_lower_11 :: "real  real"
  where "ln_lower_11  λx. - ln_upper_11 (inverse x)"

corollary ln_lower_11: "0<x  ln_lower_11 x  ln x"
  unfolding ln_lower_11_def
  by (metis ln_inverse inverse_positive_iff_positive minus_le_iff ln_upper_11)

theorem ln_lower_11_eq: "0<x 
    ln_lower_11 x = (1/30)*(142*x^5 + 2272*x^4 + 6397*x^3 + 4397*x^2 + 647*x + 5)*(x - 1) /
                    (x*(x^5 + 30*x^4 + 150*x^3 + 200*x^2 + 75*x + 6))"
  unfolding ln_lower_11_def ln_upper_11_def
  by (simp add: zero_less_mult_iff add_pos_pos dual_order.strict_implies_not_eq divide_simps)
     algebra


section ‹Upper Bound 13›

definition ln_upper_13 :: "real  real"
  where "ln_upper_13 x  (353 + 8389*x + 20149*x^4 + 50774*x^3 + 38524*x^2 + 1921*x^5 + 10*x^6) * (x - 1)
                          / (70*(1 + 42*x + 525*x^4 + 700*x^3 + 315*x^2 + 126*x^5 + 7*x^6))"

definition diff_delta_ln_upper_13 :: "real  real"
  where "diff_delta_ln_upper_13  λx. (x - 1)^13 /
                     ((1 + 42*x + 525*x^4 + 700*x^3 + 315*x^2 + 126*x^5 + 7*x^6)^2*x)"

lemma d_delta_ln_upper_13: "x > 0 
    ((λx. ln_upper_13 x - ln x) has_field_derivative diff_delta_ln_upper_13 x) (at x)"
unfolding ln_upper_13_def diff_delta_ln_upper_13_def
apply (intro derivative_eq_intros | simp)+
apply auto
apply (auto simp: add_pos_pos dual_order.strict_implies_not_eq divide_simps, algebra)
done

lemma ln_upper_13_pos:
  assumes "1  x" shows "ln(x)  ln_upper_13 x"
apply (rule gen_upper_bound_increasing [OF assms d_delta_ln_upper_13])
apply (auto simp: diff_delta_ln_upper_13_def ln_upper_13_def)
done

lemma ln_upper_13_neg:
  assumes "0 < x" and x1: "x  1" shows "ln(x)  ln_upper_13 x"
apply (rule gen_upper_bound_decreasing [OF x1 d_delta_ln_upper_13])
using assms
apply (auto simp: diff_delta_ln_upper_13_def divide_simps ln_upper_13_def mult_less_0_iff)
done

theorem ln_upper_13: "0<x  ln(x)  ln_upper_13 x"
  by (metis le_less_linear less_eq_real_def ln_upper_13_neg ln_upper_13_pos)

definition ln_lower_13 :: "real  real"
  where "ln_lower_13  λx. - ln_upper_13 (inverse x)"

corollary ln_lower_13: "0<x  ln_lower_13 x  ln x"
  unfolding ln_lower_13_def
  by (metis ln_inverse inverse_positive_iff_positive minus_le_iff ln_upper_13)

theorem ln_lower_13_eq: "0<x 
    ln_lower_13 x = (1/70)*(10 + 1921*x + 20149*x^2 + 50774*x^3 + 38524*x^4 + 8389*x^5 + 353*x^6)*(x - 1) /
                    (x*(7 + 126*x + 525*x^2 + 700*x^3 + 315*x^4 + 42*x^5 + x^6))"
  unfolding ln_lower_13_def ln_upper_13_def
  by (simp add: zero_less_mult_iff add_pos_pos dual_order.strict_implies_not_eq divide_simps)
     algebra


section ‹Upper Bound 15›

definition ln_upper_15 :: "real  real"
  where "ln_upper_15 x 
           (1487 + 49199*x + 547235*x^4 + 718735*x^3 + 334575*x^2 + 141123*x^5 + 35*x^7 + 9411*x^6)*(x - 1) /
           (280*(1 + 56*x + 2450*x^4 + 1960*x^3 + 588*x^2 + 1176*x^5 + 8*x^7 + 196*x^6))"

definition diff_delta_ln_upper_15 :: "real  real"
  where "diff_delta_ln_upper_15
          λx. (x - 1)^15 / ((1+56*x+2450*x^4+1960*x^3+588*x^2+8*x^7+196*x^6+1176*x^5)^2 * x)"

lemma d_delta_ln_upper_15: "x > 0 
    ((λx. ln_upper_15 x - ln x) has_field_derivative diff_delta_ln_upper_15 x) (at x)"
unfolding ln_upper_15_def diff_delta_ln_upper_15_def
apply (intro derivative_eq_intros | simp)+
apply auto
apply (auto simp: add_pos_pos dual_order.strict_implies_not_eq divide_simps, algebra)
done

lemma ln_upper_15_pos:
  assumes "1  x" shows "ln(x)  ln_upper_15 x"
apply (rule gen_upper_bound_increasing [OF assms d_delta_ln_upper_15])
apply (auto simp: diff_delta_ln_upper_15_def ln_upper_15_def)
done

lemma ln_upper_15_neg:
  assumes "0 < x" and x1: "x  1" shows "ln(x)  ln_upper_15 x"
apply (rule gen_upper_bound_decreasing [OF x1 d_delta_ln_upper_15])
using assms
apply (auto simp: diff_delta_ln_upper_15_def divide_simps ln_upper_15_def mult_less_0_iff)
done

theorem ln_upper_15: "0<x  ln(x)  ln_upper_15 x"
  by (metis le_less_linear less_eq_real_def ln_upper_15_neg ln_upper_15_pos)


definition ln_lower_15 :: "real  real"
  where "ln_lower_15  λx. - ln_upper_15 (inverse x)"

corollary ln_lower_15: "0<x  ln_lower_15 x  ln x"
  unfolding ln_lower_15_def
  by (metis ln_inverse inverse_positive_iff_positive minus_le_iff ln_upper_15)

theorem ln_lower_15_eq: "0<x 
    ln_lower_15 x = (1/280)*(35 + 9411*x + 141123*x^2 + 547235*x^3 + 718735*x^4 + 334575*x^5 + 49199*x^6 + 1487*x^7)*(x - 1) /
                    (x*(8 + 196*x + 1176*x^2 + 2450*x^3 + 1960*x^4 + 588*x^5 + 56*x^6 + x^7))"
  unfolding ln_lower_15_def ln_upper_15_def
  by (simp add: zero_less_mult_iff add_pos_pos dual_order.strict_implies_not_eq
              divide_simps) algebra

end

Theory Sin_Cos_Bounds

chapter ‹Sine and Cosine Upper and Lower Bounds›

theory Sin_Cos_Bounds
imports Bounds_Lemmas

begin

section‹Simple base cases›

text‹Upper bound for @{term"x0"}
lemma sin_le_arg:
  fixes x :: real
    shows "0  x  sin x  x"
  by (fact sin_x_le_x)

lemma cos_ge_1_arg:
  fixes x :: real
  assumes "0  x"
    shows "1 - x  cos x"
  apply (rule gen_lower_bound_increasing [OF assms])
  apply (intro derivative_eq_intros, auto)
  done

lemmas sin_Taylor_0_upper_bound_pos = sin_le_arg ― ‹MetiTarski bound›

lemma cos_Taylor_1_lower_bound:
  fixes x :: real
  assumes "0  x"
    shows "(1 - x^2 / 2)  cos x"
  apply (rule gen_lower_bound_increasing [OF assms])
  apply (intro derivative_eq_intros)
  apply (rule refl | simp add: sin_le_arg)+
  done

lemma sin_Taylor_1_lower_bound:
  fixes x :: real
  assumes "0  x"
    shows "(x - x ^ 3 / 6)  sin x"
  apply (rule gen_lower_bound_increasing [OF assms])
  apply (intro derivative_eq_intros)
  apply (rule refl | simp add: cos_Taylor_1_lower_bound)+
  done

section‹Taylor series approximants›

definition sinpoly :: "[nat,real]  real"
  where "sinpoly n = (λx. k<n. sin_coeff k * x ^ k)"

definition cospoly :: "[nat,real]  real"
  where "cospoly n = (λx. k<n. cos_coeff k * x ^ k)"

(*sin upper bounds have the form 4*n+2; lower bounds, 4*n
sinpoly 2 x = x                                      (upper)
sinpoly 4 x = x - (x^3)/6                            (lower)
sinpoly 6 x = x - (x^3)/6 + (x^5)/120                (upper)
sinpoly 8 x = x - (x^3)/6 + (x^5)/120 - (x^7)/5040   (lower)

cos upper bounds have the form 4*n+1; lower bounds, 4*n+3
cospoly 1 x = 1                                                             (upper)
cospoly 3 x = 1 - (x^2)/2                                                   (lower)
cospoly 5 x = 1 - (x^2)/2 + (x^4)/24 - x^6/720 + x^8/40320                  (upper)
cospoly 7 x = 1 - (x^2)/2 + (x^4)/24 - x^6/720 + x^8/40320 - x^10/3628800   (lower)
*)

lemma sinpoly_Suc: "sinpoly (Suc n) = (λx. sinpoly n x + sin_coeff n * x ^ n)"
  by (simp add: sinpoly_def)

lemma cospoly_Suc: "cospoly (Suc n) = (λx. cospoly n x + cos_coeff n * x ^ n)"
  by (simp add: cospoly_def)

lemma sinpoly_minus [simp]: "sinpoly n (-x) = - sinpoly n x"
  by (induct n) (auto simp: sinpoly_def sin_coeff_def)

lemma cospoly_minus [simp]: "cospoly n (-x) = cospoly n x"
  by (induct n) (auto simp: cospoly_def cos_coeff_def)

lemma d_sinpoly_cospoly:
    "(sinpoly (Suc n) has_field_derivative cospoly n x) (at x)"
proof (induction n)
  case 0 show ?case
    by (simp add: sinpoly_def cospoly_def)
next
  case (Suc n) show ?case
  proof (cases "n=0")
    case True then show ?thesis
      by (simp add: sinpoly_def sin_coeff_def cospoly_def)
  next
    case False then
    have xn: "x ^ (n - Suc 0) * x = x ^ n"
      by (metis Suc_pred mult.commute not_gr0 power_Suc)
    show ?thesis using Suc False
      apply (simp add: sinpoly_Suc [of "Suc n"] cospoly_def)
      apply (intro derivative_eq_intros | simp)+
      apply (simp add: xn mult.assoc sin_coeff_def cos_coeff_def divide_simps del: fact_Suc)
      apply (simp add: algebra_simps)
      done
  qed
qed

lemma d_cospoly_sinpoly:
    "(cospoly (Suc n) has_field_derivative -sinpoly n x) (at x)"
proof (induction n)
  case 0 show ?case
    by (simp add: sinpoly_def cospoly_def)
next
  case (Suc n) show ?case
  proof (cases "n=0")
    case True then show ?thesis
      by (simp add: sinpoly_def cospoly_def cos_coeff_def)
  next
    case False then
    have xn: "x ^ (n - Suc 0) * x = x ^ n"
      by (metis Suc_pred mult.commute not_gr0 power_Suc)
    have m1: "odd n  (-1 :: real) ^ ((n - Suc 0) div 2) = - ((-1) ^ (Suc n div 2))"
      by (cases n) simp_all
    show ?thesis using Suc False
      apply (simp add: cospoly_Suc [of "Suc n"] sinpoly_def)
      apply (intro derivative_eq_intros | simp)+
      apply (simp add: xn mult.assoc sin_coeff_def cos_coeff_def m1 divide_simps del: fact_Suc)
      apply (simp add: algebra_simps)
      done
  qed
qed


section‹Inductive proof of sine inequalities›

lemma sinpoly_lb_imp_cospoly_ub:
  assumes x0: "0  x" and k0: "k>0" and "x. 0  x  sinpoly (k - 1) x  sin x"
    shows "cos x  cospoly k x"
  apply (rule gen_lower_bound_increasing [OF x0])
  apply (intro derivative_eq_intros | simp)+
  using d_cospoly_sinpoly [of "k - 1"] assms
  apply auto
  apply (simp add: cospoly_def)
  done

lemma cospoly_ub_imp_sinpoly_ub:
  assumes x0: "0  x" and k0: "k>0" and "x. 0  x  cos x  cospoly (k - 1) x"
    shows "sin x  sinpoly k x"
  apply (rule gen_lower_bound_increasing [OF x0])
  apply (intro derivative_eq_intros | simp)+
  using d_sinpoly_cospoly [of "k - 1"] assms
  apply auto
  apply (simp add: sinpoly_def)
  done

lemma sinpoly_ub_imp_cospoly_lb:
  assumes x0: "0  x" and k0: "k>0" and "x. 0  x  sin x  sinpoly (k - 1) x"
    shows "cospoly k x  cos x"
  apply (rule gen_lower_bound_increasing [OF x0])
  apply (intro derivative_eq_intros | simp)+
  using d_cospoly_sinpoly [of "k - 1"] assms
  apply auto
  apply (simp add: cospoly_def)
  done

lemma cospoly_lb_imp_sinpoly_lb:
  assumes x0: "0  x" and k0: "k>0" and "x. 0  x  cospoly (k - 1) x  cos x"
    shows "sinpoly k x  sin x"
  apply (rule gen_lower_bound_increasing [OF x0])
  apply (intro derivative_eq_intros | simp)+
  using d_sinpoly_cospoly [of "k - 1"] assms
  apply auto
  apply (simp add: sinpoly_def)
  done

lemma
  assumes "0  x"
    shows sinpoly_lower_nonneg: "sinpoly (4 * Suc n) x  sin x"        (is ?th1)
      and sinpoly_upper_nonneg: "sin x  sinpoly (Suc (Suc (4*n))) x"  (is ?th2)
proof -
  have "sinpoly (4 * Suc n) x  sin x    sin x  sinpoly (Suc (Suc (4*n))) x"
    using assms
    apply (induction n arbitrary: x)
    apply (simp add: sinpoly_def sin_coeff_def sin_Taylor_1_lower_bound sin_Taylor_0_upper_bound_pos lessThan_nat_numeral fact_numeral)
    apply (auto simp: cospoly_lb_imp_sinpoly_lb sinpoly_ub_imp_cospoly_lb cospoly_ub_imp_sinpoly_ub sinpoly_lb_imp_cospoly_ub)
    done
  then show ?th1 ?th2
    using assms
    by auto
qed


section‹Collecting the results›

corollary sinpoly_upper_nonpos:
     "x  0  sin x  sinpoly (4 * Suc n) x"
  using sinpoly_lower_nonneg [of "-x" n]
  by simp

corollary sinpoly_lower_nonpos:
     "x  0  sinpoly (Suc (Suc (4*n))) x  sin x"
  using sinpoly_upper_nonneg [of "-x" n]
  by simp

corollary cospoly_lower_nonneg:
     "0  x  cospoly (Suc (Suc (Suc (4*n)))) x  cos x"
by (auto simp: sinpoly_upper_nonneg sinpoly_ub_imp_cospoly_lb)

lemma cospoly_lower:
     "cospoly (Suc (Suc (Suc (4*n)))) x  cos x"
proof (cases rule: le_cases [of 0 x])
  case le then show ?thesis
    by (simp add: cospoly_lower_nonneg)
next
  case ge then show ?thesis using cospoly_lower_nonneg [of "-x"]
    by simp
qed

lemma cospoly_upper_nonneg:
  assumes "0  x"
    shows "cos x  cospoly (Suc (4*n)) x"
proof (cases n)
  case 0 then show ?thesis
    by (simp add: cospoly_def)
next
  case (Suc m)
  then show ?thesis
    using sinpoly_lower_nonneg [of _ m] assms
    by (auto simp: sinpoly_lb_imp_cospoly_ub)
qed

lemma cospoly_upper:
  "cos x  cospoly (Suc (4*n)) x"
proof (cases rule: le_cases [of 0 x])
  case le then show ?thesis
    by (simp add: cospoly_upper_nonneg)
next
  case ge then show ?thesis using cospoly_upper_nonneg [of "-x"]
    by simp
qed

end

Theory Sqrt_Bounds

chapter ‹Square Root Upper and Lower Bounds›

theory Sqrt_Bounds
imports Bounds_Lemmas
        "HOL-Library.Sum_of_Squares"

begin

text‹Covers all bounds used in sqrt-upper.ax, sqrt-lower.ax and sqrt-extended.ax.›

section‹Upper bounds›

primrec sqrtu :: "[real,nat]  real" where
  "sqrtu x 0 = (x+1)/2"
| "sqrtu x (Suc n) = (sqrtu x n + x/sqrtu x n) / 2"

lemma sqrtu_upper: "x  sqrtu x n ^ 2"
proof (induction n)
  case 0 show ?case
    apply (simp add: power2_eq_square)
    apply (sos "(((A<0 * R<1) + (R<1 * (R<1 * [~1*x + 1]^2))))")
    done
next
  case (Suc n)
  have xy: "y. x  y * y; y  0  x * (2 * (y * y))  x * x + y * (y * (y * y))"
    by (sos "(((((A<0 * A<1) * R<1) + ((A<0 * R<1) * (R<1 * [~1*y^2 + x]^2)))) &
                   ((((A<0 * A<1) * R<1) + ((A<0 * R<1) * (R<1 * [~1*y^2 + x]^2)))))")
  show ?case using Suc
    by (auto simp: power2_eq_square algebra_simps divide_simps xy)
qed

lemma sqrtu_numeral:
  "sqrtu x (numeral n) = (sqrtu x (pred_numeral n) + x/sqrtu x (pred_numeral n)) / 2"
  by (simp add: numeral_eq_Suc)

lemma sqrtu_gt_0: "x  0  sqrtu x n > 0"
apply (induct n)
apply (auto simp: field_simps)
by (metis add_strict_increasing2 mult_zero_left not_real_square_gt_zero)

theorem gen_sqrt_upper: "0  x  sqrt x  sqrtu x n"
using real_sqrt_le_mono [OF sqrtu_upper [of x n]]
by auto (metis abs_of_nonneg dual_order.strict_iff_order sqrtu_gt_0)

lemma sqrt_upper_bound_0:
  assumes "x  0" shows "sqrt x  (x+1)/2" (is "_  ?rhs")
proof -
  have "sqrt x  sqrtu x 0"
    by (metis assms gen_sqrt_upper)
  also have "... = ?rhs"
    by (simp add: divide_simps)
  finally show ?thesis .
qed

lemma sqrt_upper_bound_1:
  assumes "x  0" shows "sqrt x  (1/4)*(x^2+6*x+1) / (x+1)" (is "_  ?rhs")
proof -
  have "sqrt x  sqrtu x 1"
    by (metis assms gen_sqrt_upper)
  also have "... = ?rhs"
    by (simp add: divide_simps) algebra
  finally show ?thesis .
qed

lemma sqrtu_2_eq:
   "sqrtu x 2 = (1/8)*(x^4 + 28*x^3 + 70*x^2 + 28*x + 1) / ((x + 1)*(x^2 + 6*x + 1))"
  by (simp add: sqrtu_numeral divide_simps) algebra

lemma sqrt_upper_bound_2:
  assumes "x  0"
    shows "sqrt x  (1/8)*(x^4 + 28*x^3 + 70*x^2 + 28*x + 1) / ((x + 1)*(x^2 + 6*x + 1))"
  by (metis assms gen_sqrt_upper sqrtu_2_eq)

lemma sqrtu_4_eq:
   "x  0 
    sqrtu x 4 = (1/32)*(225792840*x^6+64512240*x^5+601080390*x^8+471435600*x^7+496*x+1+35960*x^2+906192*x^3+10518300*x^4+x^16+906192*x^13+10518300*x^12+496*x^15+35960*x^14+471435600*x^9+225792840*x^10+64512240*x^11)
             / ((x+1)*(x^2+6*x+1)*(x^4+28*x^3+70*x^2+28*x+1)*(1820*x^6+8008*x^5+x^8+120*x^7+120*x+1+1820*x^2+8008*x^3+12870*x^4))"
  by (simp add: sqrtu_numeral divide_simps add_nonneg_eq_0_iff) algebra

lemma sqrt_upper_bound_4:
  assumes "x  0"
    shows "sqrt x  (1/32)*(225792840*x^6+64512240*x^5+601080390*x^8+471435600*x^7+496*x+1+35960*x^2+906192*x^3+10518300*x^4+x^16+906192*x^13+10518300*x^12+496*x^15+35960*x^14+471435600*x^9+225792840*x^10+64512240*x^11)
             / ((x+1)*(x^2+6*x+1)*(x^4+28*x^3+70*x^2+28*x+1)*(1820*x^6+8008*x^5+x^8+120*x^7+120*x+1+1820*x^2+8008*x^3+12870*x^4))"
  by (metis assms gen_sqrt_upper sqrtu_4_eq)

lemma gen_sqrt_upper_scaled:
  assumes "0  x" "0 < u"
    shows "sqrt x  sqrtu (x*u^2) n / u"
proof -
  have "sqrt x = sqrt x * sqrt (u^2) / u"
    using assms
    by simp
  also have "... = sqrt (x*u^2) / u"
    by (metis real_sqrt_mult)
  also have "...  sqrtu (x*u^2) n / u"
    using assms
    by (simp add: divide_simps) (metis gen_sqrt_upper zero_le_mult_iff zero_le_power2)
  finally show ?thesis .
qed

lemma sqrt_upper_bound_2_small:
  assumes "0  x"
    shows "sqrt x  (1/32)*(65536*x^4 + 114688*x^3 + 17920*x^2 + 448*x + 1) / ((16*x + 1)*(256*x^2 + 96*x + 1))"
apply (rule order_trans [OF gen_sqrt_upper_scaled [of x 4 2] eq_refl])
using assms
apply (auto simp: sqrtu_2_eq )
apply (simp add: divide_simps)
apply algebra
done

lemma sqrt_upper_bound_2_large:
  assumes "0  x"
    shows "sqrt x  (1/32)*(65536 + 114688*x + 17920*x^2 + 448*x^3 + x^4) / ((x + 16)*(256 + 96*x + x^2))"
apply (rule order_trans [OF gen_sqrt_upper_scaled [of x "1/4" 2] eq_refl])
using assms
apply (auto simp: sqrtu_2_eq )
apply (simp add: divide_simps)
apply algebra
done

section‹Lower bounds›

lemma sqrt_lower_bound_id:
  assumes "0  x" "x  1"
    shows "x  sqrt x"
proof -
  have "x^2  x" using assms
    by (metis one_le_numeral power_decreasing power_one_right)
  then show ?thesis
    by (metis real_le_rsqrt)
qed

definition sqrtl :: "[real,nat]  real" where
  "sqrtl x n = x/sqrtu x n"

lemma sqrtl_lower: "0  x  sqrtl x n ^ 2  x"
  unfolding sqrtl_def using sqrtu_upper [of x n]
  by (auto simp: power2_eq_square divide_simps mult_left_mono)

theorem gen_sqrt_lower:  "0  x  sqrtl x n  sqrt x"
using real_sqrt_le_mono [OF sqrtl_lower [of x n]]
by auto

lemma sqrt_lower_bound_0:
  assumes "x  0" shows "2*x/(x+1)  sqrt x" (is "?lhs  _")
proof -
  have "?lhs = sqrtl x 0"
    by (simp add: sqrtl_def)
  also have "...  sqrt x"
    by (metis assms gen_sqrt_lower)
  finally show ?thesis .
qed

lemma sqrt_lower_bound_1:
  assumes "x  0" shows "4*x*(x+1) / (x^2+6*x+1)  sqrt x" (is "?lhs  _")
proof -
  have "?lhs = sqrtl x 1" using assms
    by (simp add: sqrtl_def power_eq_if algebra_simps divide_simps)
  also have "...  sqrt x"
    by (metis assms gen_sqrt_lower)
  finally show ?thesis .
qed

lemma sqrtl_2_eq: "sqrtl x 2 =
    8*x*(x + 1)*(x^2 + 6*x + 1) / (x^4 + 28*x^3 + 70*x^2 + 28*x + 1)"
  using sqrtu_gt_0 [of x 2]
  by (simp add: sqrtl_def sqrtu_2_eq)

lemma sqrt_lower_bound_2:
  assumes "x  0"
    shows "8*x*(x + 1)*(x^2 + 6*x + 1) / (x^4 + 28*x^3 + 70*x^2 + 28*x + 1)  sqrt x"
  by (metis assms sqrtl_2_eq gen_sqrt_lower)

lemma sqrtl_4_eq: "x  0 
  sqrtl x 4
    = (32*x*(x+1)*(x^2+6*x+1)*(x^4+28*x^3+70*x^2+28*x+1)*(1820*x^6+8008*x^5+x^8+120*x^7+120*x+1+1820*x^2+8008*x^3+12870*x^4))
    / (225792840*x^6+64512240*x^5+601080390*x^8+471435600*x^7+496*x+1+35960*x^2+906192*x^3+10518300*x^4+x^16+906192*x^13+10518300*x^12+496*x^15+35960*x^14+471435600*x^9+225792840*x^10+64512240*x^11)"
  using sqrtu_gt_0 [of x 4]
  by (simp add: sqrtl_def sqrtu_4_eq)

lemma sqrt_lower_bound_4:
  assumes "x  0"
    shows "(32*x*(x+1)*(x^2+6*x+1)*(x^4+28*x^3+70*x^2+28*x+1)*(1820*x^6+8008*x^5+x^8+120*x^7+120*x+1+1820*x^2+8008*x^3+12870*x^4))
           / (225792840*x^6+64512240*x^5+601080390*x^8+471435600*x^7+496*x+1+35960*x^2+906192*x^3+10518300*x^4+x^16+906192*x^13+10518300*x^12+496*x^15+35960*x^14+471435600*x^9+225792840*x^10+64512240*x^11)
            sqrt x"
  by (metis assms sqrtl_4_eq gen_sqrt_lower)

lemma gen_sqrt_lower_scaled:
  assumes "0  x" "0 < u"
    shows "sqrtl (x*u^2) n / u  sqrt x"
proof -
  have "sqrtl (x*u^2) n / u  sqrt (x*u^2) / u"
    using assms
    by (simp add: divide_simps) (metis gen_sqrt_lower zero_le_mult_iff zero_le_power2)
  also have "... = sqrt x * sqrt (u^2) / u"
    by (metis real_sqrt_mult)
  also have "... = sqrt x"
    using assms
    by simp
  finally show ?thesis .
qed

lemma sqrt_lower_bound_2_small:
  assumes "0  x"
    shows "32*x*(16*x + 1)*(256*x^2 + 96*x + 1) / (65536*x^4 + 114688*x^3 + 17920*x^2 + 448*x + 1)  sqrt x"
apply (rule order_trans [OF eq_refl gen_sqrt_lower_scaled [of x 4 2]])
using assms
apply (auto simp: sqrtl_2_eq )
apply (simp add: divide_simps)
apply algebra
done

lemma sqrt_lower_bound_2_large:
  assumes "0  x"
    shows "32*x*(x + 16)*(x^2 + 96*x + 256) / (x^4 + 448*x^3 + 17920*x^2 + 114688*x + 65536)  sqrt x"
apply (rule order_trans [OF eq_refl gen_sqrt_lower_scaled [of x "1/4" 2]])
using assms
apply (auto simp: sqrtl_2_eq)
apply (simp add: divide_simps)
done

end