# Theory RealLib

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory RealLib = Complex + RingLib + FiniteLib + SetsAndFunctions:

(*  Title:      RealLib.thy
Authors:    Jeremy Avigad and Kevin Donnelly
*)

theory RealLib = Complex + RingLib + FiniteLib + SetsAndFunctions:
-- {* Clean this up! *}
-- {* Eliminate duplicates *}
-- {* Generalize theorems about reals to rings *}

subsection {* Casting to reals *}

lemma real_eq_of_nat: "real = of_nat";
apply (rule ext);
apply (unfold real_of_nat_def);
apply (rule refl);
done;

lemma real_eq_of_int: "real = of_int";
apply (rule ext);
apply (unfold real_of_int_def);
apply (rule refl);
done;

lemma real_nat_zero [simp]: "real (0::nat) = 0";

lemma real_nat_one [simp]: "real (1::nat) = 1";
by simp;

lemma le_imp_real_of_nat_le: "(x::nat) <= y ==>
real x <= real y";
by auto;

lemma divide_div_aux: "0 < d ==> (real (x::nat)) / (real d) =
real (x div d) + (real (x mod d)) / (real d)";
proof -;
assume "0 < d";
have "x = (x div d) * d + x mod d";
by auto;
then have "real x = real (x div d) * real d + real(x mod d)";
by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym]);
then have "real x / real d = … / real d";
by simp;
then show ?thesis;
qed;

lemma nat_dvd_real_div: "0 < (d::nat) ==> d dvd n ==>
real(n div d) = real n / real d";
apply (frule divide_div_aux [of d n]);
apply simp;
apply (subst dvd_eq_mod_eq_0 [THEN sym]);
apply assumption;
done;

subsection {* Misc theorems about limits and infinite sums *}

lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
apply (subgoal_tac "%n. (f n - b) == %n. (f n - (%n. b) n)")
apply (subgoal_tac "(%n. b) ----> b")
by (auto simp add: LIMSEQ_diff LIMSEQ_const)

lemma LIMSEQ_ignore_initial_segment: "f ----> a
==> (%n. f(n + k)) ----> a"
apply (unfold LIMSEQ_def)
apply (clarify)
apply (drule_tac x = r in spec)
apply (clarify)
apply (rule_tac x = "no + k" in exI)
by auto

lemma LIMSEQ_offset: "(%x. f (x + k)) ----> a ==>
f ----> a";
apply (unfold LIMSEQ_def);
apply clarsimp;
apply (drule_tac x = r in spec);
apply clarsimp;
apply (rule_tac x = "no + k" in exI);
apply clarsimp;
apply (drule_tac x = "n - k" in spec);
apply (frule mp);
apply arith;
apply simp;
done;

lemma LIMSEQ_diff_approach_zero:
"g ----> L ==> (%x. f x - g x) ----> 0  ==>
f ----> L";
apply assumption;
apply simp;
done;

lemma LIMSEQ_diff_approach_zero2:
"f ----> L ==> (%x. f x - g x) ----> 0  ==>
g ----> L";
apply (drule LIMSEQ_diff);
apply assumption;
apply simp;
done;

lemma sums_split_initial_segment: "f sums s ==>
(%n. f(n + k)) sums (s - sumr 0 k f)"
apply (unfold sums_def)
apply (rule LIMSEQ_diff_const)
apply (rule LIMSEQ_ignore_initial_segment)
by assumption

lemma summable_ignore_initial_segment: "summable f ==>
summable (%n. f(n + k))"
apply (unfold summable_def)
by (auto intro: sums_split_initial_segment)

lemma suminf_minus_initial_segment: "summable f ==>
suminf f = s ==> suminf (%n. f(n + k)) = s - sumr 0 k f"
apply (frule summable_ignore_initial_segment)
apply (rule sums_unique [THEN sym])
apply (frule summable_sums)
apply (rule sums_split_initial_segment)
by auto

lemma suminf_split_initial_segment: "summable f ==>
suminf f = sumr 0 k f + suminf (%n. f(n + k))"

lemma sums_const_times: "f sums a ==> (%x. c * f x) sums (c * a)";
apply (unfold sums_def);
apply (subgoal_tac "(λn. sumr 0 n (λx. c * f x)) = (%n. c * sumr 0 n f)");
apply (erule ssubst);
apply (rule LIMSEQ_mult);
apply (rule LIMSEQ_const);
apply assumption;
apply (rule ext);
apply (rule sumr_mult [THEN sym]);
done;

lemma summable_const_times: "summable f ==> summable (%x. c * f x)";
apply (unfold summable_def);
apply (auto intro: sums_const_times);
done;

lemma suminf_const_times: "summable f ==> suminf (%x. c * f x) = c * suminf f";
apply (rule sym);
apply (rule sums_unique);
apply (rule sums_const_times);
apply (erule summable_sums);
done;

subsection {* Facts about sumr, setsum, and setprod *}

lemma sumr_cong [rule_format]: "(ALL y. (y < x --> f y = g y)) -->
sumr 0 x f = sumr 0 x g";
by (induct x, simp_all);

lemma sumr_cong [rule_format]: "(ALL y. (y < x --> f y = g y)) -->
sumr 0 x f = sumr 0 x g";
by (induct x, simp_all);

lemma sumr_le_cong [rule_format]: "(ALL y. (y < x --> f y <= g y)) -->
sumr 0 x f <= sumr 0 x g";
apply (induct x);
apply simp;
apply auto;
apply auto;
done;

lemma sumr_ge_zero_cong [rule_format]: "(ALL y. (y < x --> 0 <= g y))
--> 0 <= sumr 0 x g";
apply (subgoal_tac "sumr 0 x (%x. 0) = 0");
apply (erule subst);
apply (clarify);
apply (rule sumr_le_cong);
apply auto;
done;

lemma sumr_split_add_le: "n <= p ==> sumr 0 n f + sumr n p f = sumr 0 p f";
apply(case_tac "n < p");
apply(subgoal_tac "n = p");
by(auto);

lemma setsum_sumr: "setsum f {0..x::nat(} = sumr 0 x f";
apply (induct_tac x);
apply (auto);
done;

lemma setsum_sumr2: "setsum f {0..x} = sumr 0 (x+1) f";
apply (subgoal_tac "{0..x} = {0..x+1(}");
apply (erule ssubst);
apply (rule setsum_sumr);
apply auto;
done;

lemma setsum_sumr3: "setsum f {)0..x} = sumr 0 x (%n. f(n + 1))";
apply (subgoal_tac "setsum f {)0..x} = setsum (%n. f(n+1)) {0..x(}");
apply (erule ssubst);
apply (rule setsum_sumr);
apply (rule setsum_reindex_cong');
prefer 4;
apply simp;
apply simp;
apply (rule_tac x = "xa - 1" in bexI);
apply auto;
apply arith;
done;

lemma setsum_sumr4: "(∑i=1..n. f i) = sumr 0 n (%i. f(i + 1))";
apply (subst setsum_sumr3 [THEN sym]);
apply (rule setsum_cong);
apply auto;
done;

lemma setsum_sumr5_aux: "(∑i=a..a+c. f i) = sumr a (a+c+1) f";
apply (induct_tac c);
apply simp;
apply simp;
apply (subgoal_tac "{a..Suc(a+n)} = {a..a+n} Un {Suc(a+n)}");
apply (erule ssubst);back;
apply (subst setsum_Un_disjoint);
apply auto;
done;

lemma setsum_sumr5: "(∑i=a..b. f i) = sumr a (b+1) f";
apply (case_tac "b < a");
apply (subgoal_tac "{a..b} = {}");
apply simp;
apply simp;
apply (subgoal_tac "b = a + (b - a)");
apply (erule ssubst);
apply (rule setsum_sumr5_aux);
apply arith;
done;

lemma setsum_singleton: "setsum f {n} =  f n";
apply auto;
done;

lemma setsum_bound: "finite A ==> ALL x:A. (f(x) <= c) ==>
setsum f A <= c * card A";
apply (induct set: Finites, auto);
done;

lemma real_of_nat_setsum: "real (setsum (f::'a => nat) A) =
setsum (real o f) A";
apply (subst real_eq_of_nat);
apply (rule setsum_of_nat);
done;

lemma real_card_eq_setsum: "finite A ==> real (card A) = setsum (%x.1) A";
apply (subst card_eq_setsum);
apply assumption;
apply (subst real_of_nat_setsum);
apply (unfold o_def);
apply simp;
done;

lemma setprod_real_of_int: "real (setprod (f::'a => int) A) =
setprod (%x. real(f x)) A";
apply (subst real_eq_of_int);
done;

lemma sumr_shift: "sumr 0 n (%n. f(m + n)) = sumr m (m + n) f";
by (induct_tac n, simp_all);

lemma sumr_zero_to_two: "sumr 0 2 f = f 0 + f 1"
proof -
have "2 = Suc (Suc 0)"
by simp
hence "sumr 0 2 f = sumr 0 (Suc (Suc 0)) f"
by (rule subst, simp)
thus ?thesis
by simp
qed

lemma sums_zero: "(%x. 0) sums 0";
apply (unfold sums_def);
apply simp;
apply (rule LIMSEQ_const);
done;

lemma suminf_zero: "suminf (%x. 0) = 0";
apply (rule sym);
apply (rule sums_unique);
apply (rule sums_zero);
done;

lemma summable_zero: "summable (%x. 0)";
apply (rule sums_summable);
apply (rule sums_zero);
done;

lemma sums_neg: "f sums s ==> (- f) sums (- s)";
by (simp add: sums_def func_minus sumr_minus LIMSEQ_minus);

lemma summable_neg: "summable f ==> summable (- f)";
by (auto simp add: summable_def intro: sums_neg);

lemma summable_neg2: "summable f ==> summable (%x. - f x)";
by (frule summable_neg, unfold func_minus);

lemma suminf_neg: "summable f ==> suminf (- f) = - (suminf f)";
apply (rule sym);
apply (rule sums_unique);
apply (rule sums_neg);
apply (erule summable_sums);
done;

subsection {* Help for calculations with reals (a mess!) *}

lemma realpow_two2: "(x::real) * x = x^2"
proof -
have "(x::real) * x = x^(Suc (Suc 0))"
by (rule realpow_two [THEN sym])
also have "... = x^2"
proof -
have "Suc (Suc 0) = 2" by simp
thus ?thesis by (rule ssubst, simp)
qed
finally show ?thesis .
qed

lemma real_mult_le_one_le: assumes "0 <= (x::real)" and "0 <= y" and "y <= 1"
shows "x * y <= x"
proof -
from prems have "x * y <= x * 1"
by (intro mult_left_mono);
thus ?thesis by auto
qed

lemma real_le_one_mult_le: assumes "0 <= (x::real)" and "0 <= y" and "y <= 1"
shows "y * x <= x"
proof -
from prems have "y * x <= 1 * x"
by (intro mult_right_mono);
thus ?thesis by auto
qed

lemma real_mult_less_one_less:
"(0::real) < x ==> x < 1 ==> 0 < y ==> y * x < y"
proof -
assume "(0::real) < x" and "x < 1" and "0 < y"
have "y * x < y * 1"
by (auto simp only: real_mult_less_mono2 prems)
thus ?thesis
by simp
qed

lemma real_less_one_mult_less:
"(0::real) < x ==> x < 1 ==> 0 < y ==> x * y < y"
proof -
assume "(0::real) < x" and "x < 1" and "0 < y"
have "x * y < 1 * y"
by (auto simp only: mult_strict_right_mono prems)
thus ?thesis
by simp
qed

lemma real_inverse_le_swap: "0 < (r::real) ==> r <= x ==>
inverse x <= inverse r"
proof -
assume "0 < (r::real)"
assume "r <= x"
then have "r < x | r = x"
by auto
with prems show "inverse x <= inverse r"
proof (elim disjE)
assume "0 < r" and "r < x"
then have "inverse x < inverse r"
by (intro less_imp_inverse_less);
then show ?thesis by auto
next assume "r = x"
thus "inverse x <= inverse r" by auto
qed
qed

lemma real_inverse_nat_le_one: "1 <= (n::nat) ==> inverse (real n) <= 1"
proof -
assume "1 <= (n::nat)"
then have "real (1::nat) <= real n"
by (auto simp only: real_of_nat_le_iff)
then have "1 <= real n" by simp
then have "inverse (real n) <= inverse 1"
by (simp only: real_inverse_le_swap)
thus ?thesis by auto
qed

lemma real_le_mult_imp_div_pos_le: assumes a: "0 < y" and
b: "(x::real) <= y * z" shows "x / y <= z"
proof -
from b have "x <= y * z" .
also from a have "x = y * (x / y)"
by auto
finally have "y * (x / y) <= y * z" .
with a show ?thesis
by (simp only: real_mult_le_cancel_iff2)
qed

lemma real_mult_le_imp_le_div_pos: assumes a: "0 < y" and
b: "(x::real) * y <= z" shows "x <= z / y"
proof -
from b a have "x * y  <= (z / y) * y" by auto
with a show ?thesis
by (simp only: real_mult_le_cancel_iff1)
qed

lemma real_le_mult_imp_le_div_pos2: assumes a: "0 < y" and
b: "y * (x::real) <= z" shows "x <= z / y"
proof -
from b a have "y * x  <= y * (z / y)" by auto
with a show ?thesis
by (simp only: real_mult_le_cancel_iff2)
qed

lemma real_mult_less_imp_less_div_pos: assumes a: "0 < y" and
b: "(x::real) * y < z" shows "x < z / y"
proof -
from b a have c: "x * y < (z / y) * y"
by simp
show ?thesis;
apply (rule  mult_right_less_imp_less);
apply (rule c);
apply (rule order_less_imp_le, rule a);
done;
qed

lemma real_div_pos_le_mono: "(x::real) <= y ==> 0 < z ==> x / z <= y / z"
by (unfold real_divide_def, auto)

lemma real_div_neg_le_anti_mono: "(x::real) <= y ==> z < 0 ==>
y / z <= x / z"

lemma real_div_pos_less_mono: "(x::real) < y ==> 0 < z ==> x / z < y / z"

lemma real_pos_div_less_anti_mono: "0 < (x::real) ==> x < y ==> 0 < z
==> z / y < z / x"
apply (unfold real_divide_def);
apply (rule real_mult_inverse_cancel2)
apply auto;
done;

lemma real_pos_div_le_mono: "0 < (x::real) ==> x <= y ==> 0 <= z
==> z / y <= z / x"
apply (unfold real_divide_def)
apply (rule mult_left_mono);
apply (rule le_imp_inverse_le);
by (assumption+)

lemma real_one_div_le_anti_mono: "0 < (x::real) ==> x <= y ==>
1 / y <= 1 / x"
by (rule real_pos_div_le_mono [of x y 1], auto)

lemma real_ge_zero_plus_gt_zero_is_gt_zero: "(0::real) <= x ==>
0 < y ==> 0 < x + y"
proof -
assume a: "(0::real) <= x" and b: "(0::real) < y"
have "(0::real) = 0 + 0" by simp
also from a b have "... < x + y"
finally show ?thesis .
qed

lemma real_gt_zero_plus_ge_zero_is_gt_zero: "(0::real) < x ==>
0 <= y ==> 0 < x + y"
proof -
assume a: "(0::real) < x" and b: "(0::real) <= y"
have "(0::real) = 0 + 0" by simp
also from a b have "... < x + y"
finally show ?thesis .
qed

lemma real_ge_zero_div_gt_zero [simp]: "(0::real) <= x ==> 0 < y ==>
0 <= x/y"
by (rule real_mult_le_imp_le_div_pos, auto)

lemma real_div_mult_simp: "(z::real) ~= 0
==> (x / z = y) = (x = z * y)"
by auto

lemma real_div_mult_simp2: "(z::real) ~= 0
==> (y = x / z) = (x = z * y)"
by auto

lemma real_minus_divide_distrib: "((x::real) - y) / z = x / z - y / z"
proof -
have "x - y = x + -y"
by auto
then have "(x - y) / z = (x + -y) / z"
by (rule ssubst, simp)
also have "... = x / z + (-y) / z"
also have "... = x / z - y / z"
by simp
finally show ?thesis .
qed

lemma real_mult_div_cancel2: "(k::real) ~= 0 ==> (m * k) / (n * k) = m / n"
proof -
assume "k ~= 0"
have "m * k = k * m" by auto
moreover have "n * k = k * n" by auto
ultimately have "(m * k) / (n * k) = (k * m) / (k * n)"
by (auto simp only:)
also have "... = m / n"
by (rule mult_divide_cancel_left);
finally show ?thesis .
qed

lemma unused1: "((x::real) / y) / z = (x / z) / y"
by auto

lemma unused2: "0 < x ==> ((x::real) / y) / x = 1 / y"
by auto

lemma real_neg_squared_eq_pos_squared: "(- (x::real))^2 = x^2"
by (auto simp add: realpow_two2 [THEN sym])

lemma real_x_times_x_squared: "(x::real) * x^2 = x^3"
proof -
have "3 = Suc 2" by auto
hence "x^3 = x^(Suc 2)" by simp
also have "... = x * x^2" by (rule realpow_Suc)
finally show ?thesis by simp
qed

lemma real_one_over_pow: "(x::real) ~= 0 ==> 1 / x^n = (1 / x)^n";
by (rule power_inverse);

lemma real_nat_ge_zero [simp]: "0 ≤ real (n::nat)";
by auto;

lemma real_nat_plus_one_gt_zero [simp]: "0 < real (n::nat) + 1";
apply (rule real_ge_zero_plus_gt_zero_is_gt_zero);
by auto;

lemma real_one_over_nat_plus_one_gt_zero [simp]: "0 < 1 / (real (n::nat) + 1)";
apply (rule real_mult_less_imp_less_div_pos);
apply (rule real_nat_plus_one_gt_zero);
by simp;

lemma real_one_over_nat_plus_one_ge_zero [simp]:
"0 ≤ 1 / (real (n::nat) + 1)";
apply (rule order_less_imp_le);
by (rule real_one_over_nat_plus_one_gt_zero);

lemma real_nat_plus_one: "real ((n::nat) + 1) = real n + 1";
by (auto intro: real_of_nat_Suc);

lemma real_frac_add: "[|b ~= 0;d ~= 0|] ==> a/b + c/(d::real) = ((a*d + c*b) / (d*b))";

lemma div_ge_1: "[|0 < a;a <= (b::real)|] ==> 1 <= b / a";
apply(rotate_tac 1);
apply(rule order_trans[of 1 "a * inverse a"]);
apply (rule mult_right_mono);
apply auto;
done;

lemma real_one_over_pos: "0 < (x::real) ==> 0 < 1 / x";
by (rule real_mult_less_imp_less_div_pos, auto);

lemma real_fraction_le: "0 < (w::real) ==> 0 < z ==> x * w <= y * z ==>
x / z <= y / w";
apply (rule real_le_mult_imp_div_pos_le);
apply assumption;
apply simp;
apply (rule real_mult_le_imp_le_div_pos);
apply assumption;
done;

lemma real_fraction_le2: "0 <= x ==> (x::real) <= y ==> 0 < w ==> w <= z  ==>
x / z <= y / w";
apply (rule real_fraction_le);
apply auto;
apply (rule mult_mono);
apply auto;
done;

subsection {* Casting quotients to real *}

theorem nat_div_real_div[rule_format]:
"0 <= real (n::nat) / real (x) - real (n div x) &
real (n) / real (x) - real (n div x) <= 1";
apply(auto);
apply(case_tac "x = 0");
apply(force simp add: DIVISION_BY_ZERO_DIV real_divide_def INVERSE_ZERO);
apply(rule real_mult_le_imp_le_div_pos);
apply force;
apply simp;
apply (subst real_of_nat_mult [THEN sym]);
apply (subst real_of_nat_le_iff);
apply (subst mult_commute);
apply (subst mult_div_cancel);
apply force;
apply(case_tac "x = 0");
apply simp;
apply (rule real_le_mult_imp_div_pos_le);
apply force;
apply (subst real_of_nat_mult [THEN sym]);
apply (subst real_of_nat_le_iff);
apply (subst mult_div_cancel);
apply (subgoal_tac "n mod x <= x");
apply arith;
apply (rule order_less_imp_le);
apply (erule mod_less_divisor);
done;

theorems nat_div_real_div1 = nat_div_real_div [THEN conjunct1];
theorems nat_div_real_div2 = nat_div_real_div [THEN conjunct2];

lemma real_nat_div_le_real_div: "real (n div x) <= real (n::nat) / real x";
apply (insert nat_div_real_div1 [of n x]);
apply simp;
done;

subsection {* Floor and ceiling *}

lemma floor_bound: "real(x::nat) <= k ==> x <= nat(floor(k))";
apply (drule floor_le2);
apply (simp only: floor_real_of_nat);
apply (subgoal_tac "nat (int x) <= nat (floor k)");
apply (case_tac "x = 0");
apply (subgoal_tac "0 <= k");
apply (subgoal_tac "int x = 0");
apply (simp add: real_of_int_le_iff [THEN sym]);
apply (subgoal_tac "real(floor k) <= k");
apply (erule order_trans);
apply simp;
apply (subgoal_tac "nat(int x) <= nat(floor k)");
apply (subgoal_tac "0 < int x | 0 <= floor k");
apply (frule nat_le_eq_zle [THEN sym]);
apply force;
apply force;
done;

lemma real_int_nat1: "real(int(nat(x))) = real(nat(x))";
apply (simp only: real_of_int_real_of_nat);
done;

lemma real_int_nat: "0 <= x ==> real(x) = real(nat(x))"
apply (subgoal_tac "real(int(nat(x))) = real(nat(x))");
apply force;
apply (rule real_int_nat1);
done;

lemma real_nat_floor: "0 <= x ==> real(nat(floor(x))) <= x";
apply (subgoal_tac "0 <= floor(x)");
apply (subgoal_tac "real(nat(floor(x))) = real(floor(x))");
apply (erule ssubst);
apply (subgoal_tac "floor 0 <= floor x");
apply (rule floor_le2);
by simp;

lemma real_upper_bound: "0 < r ==> r <= real(nat(ceiling(r)))";
apply (subgoal_tac "real(nat(ceiling(r))) = real(ceiling(r))");
apply simp;
apply (subgoal_tac "real(ceiling(r)) = real(int(nat(ceiling(r))))");
apply (erule ssubst);
apply (subst real_of_int_real_of_nat);
apply (rule refl);
apply simp;
apply (insert real_of_int_ceiling_ge [of r]);
apply (subgoal_tac "0 <= real(ceiling(r))");
apply simp;
apply (subgoal_tac "0 < real(ceiling(r))");
apply force;
apply (erule order_less_le_trans);
apply assumption;
done;

constdefs
natfloor :: "real => nat"
"natfloor x  ==  nat(floor x)";

lemma real_of_nat_eq_real_of_int: "0 <= x ==> real(nat x) = real x";
apply (subgoal_tac "real x = real(int(nat(x)))");
apply (erule ssubst);
apply (rule real_of_int_real_of_nat [THEN sym]);
apply simp;
done;

lemma floor_ge_zero_ge_zero: "0 <= x ==> 0 <= floor(x)";
apply (subgoal_tac "0 = floor(0)");
apply (erule ssubst);
apply (erule floor_le2);
apply simp;
done;

lemma real_natfloor_le: "0 <= x ==> real(natfloor(x)) <= x";
apply (unfold natfloor_def);
apply (subst real_of_nat_eq_real_of_int);
apply (erule floor_ge_zero_ge_zero);
apply simp;
done;

lemma real_natfloor_plus_one_ge: "x <= real(natfloor x) + 1";
apply (case_tac "0 <= x");
apply (unfold natfloor_def);
apply (subst real_of_nat_eq_real_of_int);
apply (erule floor_ge_zero_ge_zero);
apply simp;
done;

lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
apply (insert real_lb_ub_int [of r], safe)
apply (rule theI2)
apply (auto intro: lemma_floor)
done

lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
apply (insert real_of_int_floor_gt_diff_one [of r])
apply (auto simp del: real_of_int_floor_gt_diff_one)
done;

lemma real_of_nat_floor_add_one_gt [simp]: "r < real (natfloor r) + 1";
apply (unfold natfloor_def);
apply (case_tac "0 <= r");
apply (subst real_of_nat_eq_real_of_int);
apply (erule floor_ge_zero_ge_zero);
apply simp;
apply simp;
done;

lemma floor_add [simp]: "floor (x + real a) = floor x + a";
apply (subgoal_tac "floor(x + real a) <= floor x + a");
apply (subgoal_tac "floor x + a <= floor(x + real a)");
apply force;
apply (subgoal_tac "floor x + a < floor (x + real a) + 1");
apply arith;
apply (subst real_of_int_less_iff [THEN sym]);
apply simp;
apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1");
apply (subgoal_tac "real (floor x) <= x");
apply arith;
apply (rule real_of_int_floor_le);
apply (subgoal_tac "floor (x + real a) < floor x + a + 1");
apply arith;
apply (subst real_of_int_less_iff [THEN sym]);
apply simp;
apply (subgoal_tac "real(floor(x + real a)) <= x + real a");
apply (subgoal_tac "x < real(floor x) + 1");
apply arith;
apply (rule real_of_int_floor_le);
done;

lemma floor_subtract [simp]: "floor (x - real a) = floor x - a";
apply (subst diff_minus)+;
apply (subst real_of_int_minus);
done;

lemma real_le_floor [intro]: "real a <= x ==> a <= floor x";
apply (subgoal_tac "a < floor x + 1");
apply arith;
apply (subst real_of_int_less_iff [THEN sym]);
apply simp;
apply arith;
done;

lemma real_le_natfloor [intro]: "real a <= x ==> a <= natfloor x";
apply (unfold natfloor_def);
apply (subgoal_tac "nat (int a) <= nat (floor x)");
apply simp;
apply (subst nat_le_eq_zle);
apply (subgoal_tac "int 0 <= floor x");
apply force;
apply (rule real_le_floor);
apply force;
apply (rule real_le_floor);
apply simp;
done;

lemma natfloor_add [simp]: "0 <= x ==> natfloor(x + real a) = natfloor x + a";
apply (unfold natfloor_def);
apply (subgoal_tac "real a = real (int a)");
apply (erule ssubst);
apply auto;
done;

lemma natfloor_subtract [simp]: "real a <= x ==>
natfloor(x - real a) = natfloor x - a";
apply (unfold natfloor_def);
apply (subgoal_tac "real a = real (int a)");
apply (erule ssubst);
apply (subst floor_subtract);
apply (subst nat_diff_distrib);
apply auto;
done;

lemma natfloor_ge_zero_lt_one: "0 <= x ==> x < 1 ==> natfloor x = 0";
apply (subgoal_tac "0 <= natfloor x");
apply (subgoal_tac "natfloor x < 1");
apply arith;
apply (unfold natfloor_def);
apply simp;
apply (rule floor_eq4);
apply auto;
done;

lemma natfloor_div_nat: "1 <= x ==> 0 < y ==>
natfloor (x / real y) = natfloor x div y";
proof -;
assume "1 <= (x::real)" and "0 < (y::nat)";
have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y";
by simp;
then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
real((natfloor x) mod y)";
by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym]);
have "x = real(natfloor x) + (x - real(natfloor x))";
by simp;
then have "x = real ((natfloor x) div y) * real y +
real((natfloor x) mod y) + (x - real(natfloor x))";
then have "x / real y = ... / real y";
by simp;
also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
real y + (x - real(natfloor x)) / real y";
diff_divide_distrib prems);
finally have "natfloor (x / real y) = natfloor(...)"; by simp;
also have "... = natfloor(real((natfloor x) mod y) /
real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))";
also have "... = natfloor(real((natfloor x) mod y) /
real y + (x - real(natfloor x)) / real y) + (natfloor x) div y";
apply (rule nonneg_plus_nonneg);
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply (rule real_ge_zero_div_gt_zero);
apply simp;
apply (rule real_natfloor_le);
apply (insert prems, arith);
done;
also have "natfloor(real((natfloor x) mod y) /
real y + (x - real(natfloor x)) / real y) = 0";
apply (rule natfloor_ge_zero_lt_one);
apply (rule nonneg_plus_nonneg);
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply (rule real_ge_zero_div_gt_zero);
apply simp;
apply (rule real_natfloor_le);
apply (insert prems, arith);
apply (subst pos_divide_less_eq);
apply simp;
apply (subgoal_tac "real y = real y - 1 + 1");
apply (erule ssubst);
apply (subgoal_tac "real(natfloor x mod y) + 1 =
real(natfloor x mod y + 1)");
apply (erule ssubst);
apply (subst real_of_nat_le_iff);
apply (subgoal_tac "natfloor x mod y < y");
apply arith;
apply (rule mod_less_divisor);
apply assumption;
apply auto;
done;
finally show ?thesis;
by simp;
qed;

lemma nat_le_natfloor: "0 <= x ==> y <= natfloor x ==> real y <= x";
apply (rule order_trans);
apply (subgoal_tac "real y <= real (natfloor x)");
apply assumption;
apply force;
apply (rule real_natfloor_le);
apply assumption;
done;

lemma natfloor_real_id [simp]: "natfloor (real n) = n";
by (unfold natfloor_def, simp);

lemma natfloor_neg: "x <= 0 ==> natfloor x = 0";
apply (unfold natfloor_def);
apply (subgoal_tac "floor x <= 0");
apply simp;
apply (subgoal_tac "floor x < 1");
apply arith;
apply (subgoal_tac "real (floor x) < real 1");
apply force;
apply (rule order_le_less_trans);
apply (rule real_of_int_floor_le);
apply simp;
done;

lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n";
apply (subgoal_tac "z < real(natfloor z) + 1");
apply arith;
done;

lemma natfloor_zero [simp]: "natfloor 0 = 0";
apply (subgoal_tac "0 = real (0::nat)");
apply (erule ssubst);
apply (rule natfloor_real_id);
apply simp;
done;

lemma natfloor_one [simp]: "natfloor 1 = 1";
apply (subgoal_tac "1 = real (1::nat)");
apply (erule ssubst);
apply (rule natfloor_real_id);
apply simp;
done;

lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y";
apply (case_tac "0 <= x");
apply (subst natfloor_def)+;
apply (subst nat_le_eq_zle);
apply force;
apply (erule floor_le2);
apply (subst natfloor_neg);back;
apply arith;
apply force;
done;

lemma natfloor_plus_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1";
apply (subgoal_tac "natfloor (x + 1) = natfloor(x + real (1::nat))");
apply (erule ssubst);
apply simp;
done;

subsection {* powr and ln *}

lemma zero_le_powr [iff]: "0 <= x powr y";
apply (rule order_less_imp_le);
apply simp;
done;

lemma powr_realpow: "0 < x ==> x powr (real n) = x^n";
apply (induct n);
apply simp;
apply (subgoal_tac "real(Suc n) = real n + 1");
apply (erule ssubst);
apply simp;
apply simp;
done;

lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0
else x powr (real n))";
apply (case_tac "x = 0");
apply simp;
apply simp;
apply (rule powr_realpow [THEN sym]);
apply simp;
done;

lemma ln_pwr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x";
apply (unfold powr_def);
apply simp;
done;

lemma ln_bound: "1 <= x ==> ln x <= x";
apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1");
apply simp;
apply simp;
done;

lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b";
apply (case_tac "x = 1");
apply simp;
apply (case_tac "a = b");
apply simp;
apply (rule order_less_imp_le);
apply (rule powr_less_mono);
apply auto;
done;

lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a";
apply (subst powr_zero_eq_one [THEN sym]);
apply (rule powr_mono);
apply assumption+;
done;

lemma power_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a <
y powr a";
apply (unfold powr_def);
apply (rule exp_less_mono);
apply (rule mult_strict_left_mono);
apply (subst ln_less_cancel_iff);
apply assumption;
apply (rule order_less_trans);
prefer 2;
apply assumption+;
done;

lemma power_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <=
y powr a";
apply (case_tac "a = 0");
apply simp;
apply (case_tac "x = y");
apply simp;
apply (rule order_less_imp_le);
apply (rule power_less_mono2);
apply auto;
done;

lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a";
apply (rule real_le_mult_imp_le_div_pos2);
apply assumption;
apply (subst ln_pwr [THEN sym]);
apply auto;
apply (rule ln_bound);
apply (erule ge_one_powr_ge_zero);
apply (erule order_less_imp_le);
done;

lemma ln_powr_bound2: "1 < x ==> 0 < a ==> (ln x) powr a <= (a powr a) * x";
proof -;
assume "1 < x" and "0 < a";
then have "ln x <= (x powr (1 / a)) / (1 / a)";
apply (intro ln_powr_bound);
apply (erule order_less_imp_le);
apply (erule real_one_over_pos);
done;
also have "... = a * (x powr (1 / a))";
by simp;
finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a";
apply (intro power_mono2);
apply (rule order_less_imp_le, rule prems);
apply (rule ln_gt_zero);
apply (rule prems);
apply assumption;
done;
also have "... = (a powr a) * ((x powr (1 / a)) powr a)";
apply (rule powr_mult);
apply (rule prems);
apply (rule powr_gt_zero);
done;
also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)";
by (rule powr_powr);
also have "... = x";
apply simp;
apply (subgoal_tac "a ~= 0");
apply (insert prems, auto);
done;
finally show ?thesis;.;
qed;

lemma power_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a <
x powr a";
apply (unfold powr_def);
apply (rule exp_less_mono);
apply (rule mult_strict_left_mono_neg);
apply (subst ln_less_cancel_iff);
apply assumption;
apply (rule order_less_trans);
prefer 2;
apply assumption+;
done;

lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0";
apply (unfold LIMSEQ_def);
apply clarsimp;
apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI);
apply clarify;
proof -;
fix r; fix n;
assume "0 < s" and "0 < r" and "natfloor (r powr (1 / - s)) + 1 <= n";
have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1";
also have "... = real(natfloor(r powr (1 / -s)) + 1)";
by simp;
also have "... <= real n";
apply (subst real_of_nat_le_iff);
apply (rule prems);
done;
finally have "r powr (1 / - s) < real n";.;
then have "real n powr (- s) < (r powr (1 / - s)) powr - s";
apply (intro power_less_mono2_neg);
done;
also have "... = r";
by (simp add: powr_powr prems less_imp_neq [THEN not_sym]);
finally show "real n powr - s < r";.;
qed;

lemma powr_divide2: "x powr a / x powr b = x powr (a - b)";
apply (subst exp_diff [THEN sym]);
done;

lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)";
proof -;
assume "exp 1 <= x" and "x <= y";
have a: "0 < x" and b: "0 < y";
apply (insert prems);
apply (subgoal_tac "0 < exp 1");
apply arith;
apply auto;
apply (subgoal_tac "0 < exp 1");
apply arith;
apply auto;
done;
have "x * ln y - x * ln x = x * (ln y - ln x)";
also have "... = x * ln(y / x)";
apply (subst ln_div);
apply (rule b, rule a, rule refl);
done;
also have "y / x = (x + (y - x)) / x";
by simp;
also have "... = 1 + (y - x) / x";
apply (insert a, arith);
done;
also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)";
apply (rule mult_left_mono);
apply (rule real_ge_zero_div_gt_zero);
apply (rule order_less_imp_le, rule a);
done;
also have "... = y - x";
apply simp;
apply (insert a, arith);
done;
also have "... = (y - x) * ln (exp 1)";
by simp;
also have "... <= (y - x) * ln x";
apply (rule mult_left_mono);
apply (subst ln_le_cancel_iff);
apply force;
apply (rule a);
apply (rule prems);
done;
also have "... = y * ln x - x * ln x";
by (rule left_diff_distrib);
finally have "x * ln y <= y * ln x";
by arith;
then have "ln y <= (y * ln x) / x";
apply (subst pos_le_divide_eq);
apply (rule a);
done;
also have "... = y * (ln x / x)";
by simp;
finally show ?thesis;
apply (subst pos_divide_le_eq);
apply (rule b);
done;
qed;

end

### Casting to reals

lemma real_eq_of_nat:

real = of_nat

lemma real_eq_of_int:

real = of_int

lemma real_nat_zero:

real 0 = 0

lemma real_nat_one:

real 1 = 1

lemma le_imp_real_of_nat_le:

xy ==> real x ≤ real y

lemma divide_div_aux:

0 < d ==> real x / real d = real (x div d) + real (x mod d) / real d

lemma nat_dvd_real_div:

[| 0 < d; d dvd n |] ==> real (n div d) = real n / real d

### Misc theorems about limits and infinite sums

lemma LIMSEQ_diff_const:

f ----> a ==> (%n. f n - b) ----> a - b

lemma LIMSEQ_ignore_initial_segment:

f ----> a ==> (%n. f (n + k)) ----> a

lemma LIMSEQ_offset:

(%x. f (x + k)) ----> a ==> f ----> a

lemma LIMSEQ_diff_approach_zero:

[| g ----> L; (%x. f x - g x) ----> 0 |] ==> f ----> L

lemma LIMSEQ_diff_approach_zero2:

[| f ----> L; (%x. f x - g x) ----> 0 |] ==> g ----> L

lemma sums_split_initial_segment:

f sums s ==> (%n. f (n + k)) sums (s - sumr 0 k f)

lemma summable_ignore_initial_segment:

summable f ==> summable (%n. f (n + k))

lemma suminf_minus_initial_segment:

[| summable f; suminf f = s |] ==> suminf (%n. f (n + k)) = s - sumr 0 k f

lemma suminf_split_initial_segment:

summable f ==> suminf f = sumr 0 k f + suminf (%n. f (n + k))

lemma sums_const_times:

f sums a ==> (%x. c * f x) sums (c * a)

lemma summable_const_times:

summable f ==> summable (%x. c * f x)

lemma suminf_const_times:

summable f ==> suminf (%x. c * f x) = c * suminf f

### Facts about sumr, setsum, and setprod

lemma sumr_cong:

(!!y. y < x ==> f y = g y) ==> sumr 0 x f = sumr 0 x g

lemma sumr_cong:

(!!y. y < x ==> f y = g y) ==> sumr 0 x f = sumr 0 x g

lemma sumr_le_cong:

(!!y. y < x ==> f yg y) ==> sumr 0 x f ≤ sumr 0 x g

lemma sumr_ge_zero_cong:

(!!y. y < x ==> 0 ≤ g y) ==> 0 ≤ sumr 0 x g

np ==> sumr 0 n f + sumr n p f = sumr 0 p f

lemma setsum_sumr:

setsum f {0..x(} = sumr 0 x f

lemma setsum_sumr2:

setsum f {0..x} = sumr 0 (x + 1) f

lemma setsum_sumr3:

setsum f {)0..x} = sumr 0 x (%n. f (n + 1))

lemma setsum_sumr4:

setsum f {1..n} = sumr 0 n (%i. f (i + 1))

lemma setsum_sumr5_aux:

setsum f {a..a + c} = sumr a (a + c + 1) f

lemma setsum_sumr5:

setsum f {a..b} = sumr a (b + 1) f

lemma setsum_singleton:

setsum f {n} = f n

lemma setsum_bound:

[| finite A; ∀xA. f xc |] ==> setsum f Ac * card A

lemma real_of_nat_setsum:

real (setsum f A) = setsum (real ˆ f) A

lemma real_card_eq_setsum:

finite A ==> real (card A) = (∑xA. 1)

lemma setprod_real_of_int:

real (setprod f A) = (∏xA. real (f x))

lemma sumr_shift:

sumr 0 n (%n. f (m + n)) = sumr m (m + n) f

lemma sumr_zero_to_two:

sumr 0 2 f = f 0 + f 1

lemma sums_zero:

(%x. 0) sums 0

lemma suminf_zero:

suminf (%x. 0) = 0

lemma summable_zero:

summable (%x. 0)

lemma sums_neg:

f sums s ==> (- f) sums - s

lemma summable_neg:

summable f ==> summable (- f)

lemma summable_neg2:

summable f ==> summable (%x. - f x)

lemma suminf_neg:

summable f ==> suminf (- f) = - suminf f

### Help for calculations with reals (a mess!)

lemma realpow_two2:

x * x = x²

lemma

[| 0 ≤ x; 0 ≤ y; y ≤ 1 |] ==> x * yx

lemma

[| 0 ≤ x; 0 ≤ y; y ≤ 1 |] ==> y * xx

lemma real_mult_less_one_less:

[| 0 < x; x < 1; 0 < y |] ==> y * x < y

lemma real_less_one_mult_less:

[| 0 < x; x < 1; 0 < y |] ==> x * y < y

lemma real_inverse_le_swap:

[| 0 < r; rx |] ==> inverse x ≤ inverse r

lemma real_inverse_nat_le_one:

1 ≤ n ==> inverse (real n) ≤ 1

lemma

[| 0 < y; xy * z |] ==> x / yz

lemma

[| 0 < y; x * yz |] ==> xz / y

lemma

[| 0 < y; y * xz |] ==> xz / y

lemma

[| 0 < y; x * y < z |] ==> x < z / y

lemma real_div_pos_le_mono:

[| xy; 0 < z |] ==> x / zy / z

lemma real_div_neg_le_anti_mono:

[| xy; z < 0 |] ==> y / zx / z

lemma real_div_pos_less_mono:

[| x < y; 0 < z |] ==> x / z < y / z

lemma real_pos_div_less_anti_mono:

[| 0 < x; x < y; 0 < z |] ==> z / y < z / x

lemma real_pos_div_le_mono:

[| 0 < x; xy; 0 ≤ z |] ==> z / yz / x

lemma real_one_div_le_anti_mono:

[| 0 < x; xy |] ==> 1 / y ≤ 1 / x

lemma real_ge_zero_plus_gt_zero_is_gt_zero:

[| 0 ≤ x; 0 < y |] ==> 0 < x + y

lemma real_gt_zero_plus_ge_zero_is_gt_zero:

[| 0 < x; 0 ≤ y |] ==> 0 < x + y

lemma real_ge_zero_div_gt_zero:

[| 0 ≤ x; 0 < y |] ==> 0 ≤ x / y

lemma real_div_mult_simp:

z ≠ 0 ==> (x / z = y) = (x = z * y)

lemma real_div_mult_simp2:

z ≠ 0 ==> (y = x / z) = (x = z * y)

lemma real_minus_divide_distrib:

(x - y) / z = x / z - y / z

lemma real_mult_div_cancel2:

k ≠ 0 ==> m * k / (n * k) = m / n

lemma unused1:

x / y / z = x / z / y

lemma unused2:

0 < x ==> x / y / x = 1 / y

lemma real_neg_squared_eq_pos_squared:

(- x)² = x²

lemma real_x_times_x_squared:

x * x² = x ^ 3

lemma real_one_over_pow:

x ≠ 0 ==> 1 / x ^ n = (1 / x) ^ n

lemma real_nat_ge_zero:

0 ≤ real n

lemma real_nat_plus_one_gt_zero:

0 < real n + 1

lemma real_one_over_nat_plus_one_gt_zero:

0 < 1 / (real n + 1)

lemma real_one_over_nat_plus_one_ge_zero:

0 ≤ 1 / (real n + 1)

lemma real_nat_plus_one:

real (n + 1) = real n + 1

[| b ≠ 0; d ≠ 0 |] ==> a / b + c / d = (a * d + c * b) / (d * b)

lemma div_ge_1:

[| 0 < a; ab |] ==> 1 ≤ b / a

lemma real_one_over_pos:

0 < x ==> 0 < 1 / x

lemma real_fraction_le:

[| 0 < w; 0 < z; x * wy * z |] ==> x / zy / w

lemma real_fraction_le2:

[| 0 ≤ x; xy; 0 < w; wz |] ==> x / zy / w

### Casting quotients to real

theorem nat_div_real_div:

0 ≤ real n / real x - real (n div x) ∧ real n / real x - real (n div x) ≤ 1

theorems nat_div_real_div1:

0 ≤ real n_1 / real x_1 - real (n_1 div x_1)

theorems nat_div_real_div2:

real n_1 / real x_1 - real (n_1 div x_1) ≤ 1

lemma real_nat_div_le_real_div:

real (n div x) ≤ real n / real x

### Floor and ceiling

lemma floor_bound:

real xk ==> x ≤ nat ⌊k

lemma real_int_nat1:

real (int (nat x)) = real (nat x)

lemma real_int_nat:

0 ≤ x ==> real x = real (nat x)

lemma real_nat_floor:

0 ≤ x ==> real (nat ⌊x⌋) ≤ x

lemma real_upper_bound:

0 < r ==> r ≤ real (nat ⌈r⌉)

lemma real_of_nat_eq_real_of_int:

0 ≤ x ==> real (nat x) = real x

lemma floor_ge_zero_ge_zero:

0 ≤ x ==> 0 ≤ ⌊x

lemma real_natfloor_le:

0 ≤ x ==> real (natfloor x) ≤ x

lemma real_natfloor_plus_one_ge:

x ≤ real (natfloor x) + 1

lemma real_of_int_floor_gt_diff_one:

r - 1 < real ⌊r

r < real ⌊r⌋ + 1

r < real (natfloor r) + 1

x + real a⌋ = ⌊x⌋ + a

lemma floor_subtract:

x - real a⌋ = ⌊x⌋ - a

lemma real_le_floor:

real ax ==> a ≤ ⌊x

lemma real_le_natfloor:

real ax ==> a ≤ natfloor x

0 ≤ x ==> natfloor (x + real a) = natfloor x + a

lemma natfloor_subtract:

real ax ==> natfloor (x - real a) = natfloor x - a

lemma natfloor_ge_zero_lt_one:

[| 0 ≤ x; x < 1 |] ==> natfloor x = 0

lemma natfloor_div_nat:

[| 1 ≤ x; 0 < y |] ==> natfloor (x / real y) = natfloor x div y

lemma nat_le_natfloor:

[| 0 ≤ x; y ≤ natfloor x |] ==> real yx

lemma natfloor_real_id:

natfloor (real n) = n

lemma natfloor_neg:

x ≤ 0 ==> natfloor x = 0

lemma ge_natfloor_plus_one_imp_gt:

natfloor z + 1 ≤ n ==> z < real n

lemma natfloor_zero:

natfloor 0 = 0

lemma natfloor_one:

natfloor 1 = 1

lemma natfloor_mono:

xy ==> natfloor x ≤ natfloor y

lemma natfloor_plus_one:

0 ≤ x ==> natfloor (x + 1) = natfloor x + 1

### powr and ln

lemma zero_le_powr:

0 ≤ x powr y

lemma powr_realpow:

0 < x ==> x powr real n = x ^ n

lemma powr_realpow2:

[| 0 ≤ x; 0 < n |] ==> x ^ n = (if x = 0 then 0 else x powr real n)

lemma ln_pwr:

[| 0 < x; 0 < y |] ==> ln (x powr y) = y * ln x

lemma ln_bound:

1 ≤ x ==> ln xx

lemma powr_mono:

[| ab; 1 ≤ x |] ==> x powr ax powr b

lemma ge_one_powr_ge_zero:

[| 1 ≤ x; 0 ≤ a |] ==> 1 ≤ x powr a

lemma power_less_mono2:

[| 0 < a; 0 < x; x < y |] ==> x powr a < y powr a

lemma power_mono2:

[| 0 ≤ a; 0 < x; xy |] ==> x powr ay powr a

lemma ln_powr_bound:

[| 1 ≤ x; 0 < a |] ==> ln xx powr a / a

lemma ln_powr_bound2:

[| 1 < x; 0 < a |] ==> ln x powr aa powr a * x

lemma power_less_mono2_neg:

[| a < 0; 0 < x; x < y |] ==> y powr a < x powr a

lemma LIMSEQ_neg_powr:

0 < s ==> (%x. real x powr - s) ----> 0

lemma powr_divide2:

x powr a / x powr b = x powr (a - b)

lemma ln_x_over_x_mono:

[| exp 1 ≤ x; xy |] ==> ln y / y ≤ ln x / x