Up to index of Isabelle/HOL/HOL-Complex/NumberTheory
theory RealLnSum = NatIntLib + LnSum1a + LnSum5:(* Title: RealLnSum.thy
Author: Jeremy Avigad
*)
header {* Transfering asymptotic functions from nats to reals *}
theory RealLnSum = NatIntLib + LnSum1a + LnSum5:
subsection {* Sum of one over n *}
lemma bigo_real_inverse_nat_inverse: "O(%x. 1 / (abs(x) + 1)) =
O(%x. 1 / (real(natfloor(abs(x))) + 1))";
proof (rule equalityI);
show "O(%x. 1 / (abs x +1)) <= O(%x. 1 / (real (natfloor(abs x)) + 1))";
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule order_less_imp_le);
apply (rule real_one_over_pos);
apply arith;
apply (rule allI);
apply (rule real_one_div_le_anti_mono);
apply force;
apply (rule add_right_mono);
apply (rule real_natfloor_le);
apply force;
done;
next show "O(%x. 1 / (real (natfloor (abs x)) + 1)) <=
O(%x. 1 / (abs x + 1))";
apply (rule bigo_elt_subset);
apply (rule bigo_bounded_alt);
apply (rule allI);
apply (rule order_less_imp_le);
apply (rule real_one_over_pos);
apply arith;
apply (rule allI);
apply simp;
apply (rule real_fraction_le);
apply arith;
apply force;
apply (simp add: ring_distrib);
apply (subgoal_tac "abs x + 1 <= 2 * real(natfloor(abs x)) + 2");
apply assumption;
apply auto;
apply (subgoal_tac "abs x <= real(natfloor (abs x)) + 1");
apply force;
apply (rule real_natfloor_plus_one_ge);
done;
qed;
lemma ln_real_approx_ln_nat: "(%x. ln(abs(x) + 1)) =o
(%x. ln(real(natfloor(abs(x))) + 1)) +o O(%x. 1 / (abs(x) + 1))";
proof (rule set_minus_imp_plus);
have "(%x. ln (abs(x) + 1)) - (%x. ln (real (natfloor(abs(x))) + 1)) =
(%x. ln((abs(x) + 1) / (real(natfloor(abs(x))) + 1)))";
apply (simp add: func_diff);
apply (rule ext);
apply (subst ln_div);
apply arith;
apply force;
apply (rule refl);
done;
also have "(%x. ln ((abs(x) + 1) / (real(natfloor(abs(x))) + 1))) =
(%x. ln (1 + (abs(x) - real(natfloor(abs(x)))) /
(real(natfloor(abs(x))) + 1)))";
apply (rule ext);
apply (rule arg_cong);back;
apply (simp add: add_ac mult_ac nonzero_eq_divide_eq
nonzero_divide_eq_eq right_distrib);
done;
also have "... =o O(%x. 1 / (real(natfloor(abs(x))) + 1))";
apply (rule bigo_bounded);
apply (rule allI);
apply (rule ln_ge_zero);
apply simp;
apply (subst pos_le_divide_eq);
apply force;
apply simp;
apply (rule real_natfloor_le);
apply force;
apply (rule allI);
apply (subst add_commute);
apply (rule order_trans);
apply (rule ln_add_one_self_le_self);
apply (subst pos_le_divide_eq);
apply force;
apply simp;
apply (rule real_natfloor_le);
apply force;
apply (rule divide_right_mono);
apply (simp add: compare_rls);
apply (subst add_commute);
apply (rule real_natfloor_plus_one_ge);
apply force;
done;
also have "... = O(%x. 1 / (abs x + 1))";
by (rule bigo_real_inverse_nat_inverse [THEN sym]);
finally show "(%x. ln (abs x + 1)) - (%x. ln (real (natfloor (abs x)) + 1))
: O(%x. 1 / (abs x + 1))";.;
qed;
lemma better_ln_theorem2_real: "(%x. ln(abs x + 1)) =o
((%x. sumr 0 (natfloor(abs x)+1) (%n. 1 / (real n + 1))) + (%x. gamma)) +o
O(%x. 1 / (abs x + 1))" (is "?LHS =o ?RHS");
proof -;
have "?LHS =o (%x. ln(real(natfloor(abs x)) + 1)) +o
O(%x. 1 / (abs x + 1))";
by (rule ln_real_approx_ln_nat);
also have "... <=
((%x. sumr 0 ((natfloor(abs x)) + 1) (%n. 1 / (real n + 1))) +
(%x. gamma)) +o O(%x. 1 / (real (natfloor(abs x)) + 1))
+ O(%x. 1 / (abs(x) + 1))";
apply (rule set_plus_mono3);
apply (insert better_ln_theorem2);
apply (simp only: func_plus);
apply (erule bigo_compose2);
done;
also have "... =
(((%x. sumr 0 ((natfloor(abs x)) + 1) (%n. 1 / (real n + 1))) +
(%x. gamma))) +o (O(%x. 1 / (real (natfloor(abs x)) + 1)) +
O(%x. 1 / (abs(x) + 1)))";
by (simp add: set_plus_rearranges add_ac);
also have "O(%x. 1 / (real (natfloor(abs x)) + 1)) +
O(%x. 1 / (abs(x) + 1)) = O(%x. 1 / (abs(x) + 1))";
apply (subst bigo_real_inverse_nat_inverse [THEN sym]);
apply simp;
done;
finally show ?thesis;.;
qed;
subsection {* Sum of ln *}
lemma identity_three_cor: "(%n. sumr 0 (n + 1) (%i. ln (real i + 1)))
=o ((%n. (real n + 1) * ln (real n + 1)) +o O(%n. real n))";
proof -;
note identity_three;
also have "((%n. (real n + 1) * ln (real n + 1)) - real) +o
O(%n. ln (real n + 1)) = (%n. (real n + 1) * ln (real n + 1)) +o
(- real +o O(%n. ln (real n + 1)))";
by (simp add: set_plus_rearranges add_ac diff_minus);
also have "... <= ((%n. (real (n::nat) + 1) * ln (real n + 1)) +o
O(%n. real n))";
apply (rule set_plus_mono);
apply (subst bigo_plus_idemp [THEN sym]);
apply (rule set_plus_mono5);
apply (rule bigo_minus);
apply (rule bigo_refl);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule ln_ge_zero);
apply force;
apply (rule allI);
apply (subst add_commute);
apply (rule ln_add_one_self_le_self);
apply force;
done;
finally show ?thesis;.;
qed;
lemma natfloor_bigo: "(%x. real (natfloor (abs x)) + 1) : O(%x. abs x + 1)";
apply (rule bigo_bounded);
apply force;
apply auto;
apply (rule real_natfloor_le);
apply force;
done;
lemma identity_three_cor_real: "(%x. sumr 0 (natfloor(abs x) + 1)
(%i. ln (real i + 1)))
=o (%x. (real (natfloor (abs x) + 1)) *
ln (abs x + 1)) +o O(%x. (abs x) + 1)";
proof -;
note bigo_compose2 [OF identity_three_cor, of "%x. natfloor(abs x)"];
also have "(%x. (real (natfloor (abs x)) + 1) *
ln (real (natfloor (abs x)) + 1)) = (%x. (real (natfloor(abs x)) + 1) *
ln (abs x + 1)) + (%x. (real (natfloor(abs x)) + 1) *
(ln (real (natfloor (abs x))+1) - ln(abs x + 1)))";
by (simp add: func_plus diff_minus ring_eq_simps);
also; have "... +o O(%x. real(natfloor(abs x))) =
(%x. (real (natfloor(abs x)) + 1) *
ln (abs x + 1)) +o ((%x. (real (natfloor(abs x)) + 1) *
(ln (real (natfloor (abs x))+1) - ln(abs x + 1))) +o
O(%x. real(natfloor(abs x))))";
by (simp add: set_plus_rearranges);
also have "... <= (%x. (real (natfloor(abs x)) + 1) *
ln (abs x + 1)) +o O(%x. abs x + 1)";
apply (rule set_plus_mono);
apply (subst bigo_plus_idemp [THEN sym]);
apply (rule set_plus_mono5);
apply (subgoal_tac "O(%x. abs x + (1::real)) =
O(%x. abs x + 1) * O(%x. 1)");
apply (erule ssubst);
apply (subgoal_tac "(%x. (real (natfloor (abs x)) + 1) *
(ln (real (natfloor (abs x)) + 1) - ln (abs x + 1))) =
(%x. (real (natfloor (abs x)) + 1)) *
(%x. (ln (real (natfloor (abs x)) + 1) - ln (abs x + 1)))");
apply (erule ssubst);
apply (rule set_times_intro);
apply (rule natfloor_bigo);
apply (subgoal_tac "O(%x. 1 / (abs x + 1)) <= O(%x. 1)");
apply (erule subsetD);
apply (subst func_diff [THEN sym]);back;
apply (rule set_plus_imp_minus);
apply (rule bigo_add_commute_imp);
apply (rule ln_real_approx_ln_nat);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply simp;
apply arith;
apply (rule allI);
apply (rule real_le_mult_imp_div_pos_le);
apply arith;
apply simp;
apply (simp add: func_times);
apply (subst bigo_mult8 [THEN sym]);
apply arith;
apply (simp add: func_times);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (rule order_trans);
apply (rule real_natfloor_le);
apply force;
apply force;
done;
also have "(%x. (real (natfloor (abs x)) + 1) * ln (abs x + 1)) =
(%x. (real (natfloor (abs x) + 1)) * ln (abs x + 1))";
by (rule ext, simp);
finally show ?thesis;.;
qed;
subsection {* Misc bigo calculations *}
lemma natfloor_bigo: "(%x. abs x - real (natfloor (abs x))) : O(%x. 1)";
apply (rule bigo_bounded);
apply auto;
apply (rule real_natfloor_le);
apply simp;
apply (subgoal_tac "abs x <= real(natfloor (abs x)) + 1");
apply force;
apply (rule real_natfloor_plus_one_ge);
done;
lemma x_times_ln_x_real_nat_approx: "(%x. (abs x + 1) * ln (abs x + 1)) =o
(%x. (real (natfloor (abs x)) + 1) * ln(real (natfloor (abs x)) + 1)) +o
O(%x. ln(abs x + 1) + 1)";
proof (rule set_minus_imp_plus);
have "(%x. (abs x + 1) * ln (abs x + 1)) -
(%x. (real (natfloor (abs x)) + 1) * ln (real (natfloor (abs x)) + 1)) =
(%x. (abs x + 1) - (real (natfloor (abs x)) + 1)) *
(%x. ln(abs x + 1)) + (%x. (real (natfloor (abs x))) + 1) *
(%x. ln(abs x + 1) - ln(real (natfloor (abs x)) + 1))";
apply (simp add: func_plus func_diff func_times);
apply (rule ext);
apply (simp add: ring_eq_simps);
done;
also have "... =o (%x. ln (abs x + 1)) *o O(%x. 1) + O(%x. abs x + 1) *
O(%x. 1 / (abs x + 1))";
apply (rule set_plus_intro);
apply (simp only: mult_commute);
apply (rule set_times_intro2);
apply (simp add: diff_minus [THEN sym]);
apply (rule natfloor_bigo);
apply (rule set_times_intro);
apply (rule bigo_bounded);
apply force;
apply auto;
apply (rule real_natfloor_le);
apply force;
apply (subst func_diff [THEN sym]);back;
apply (rule set_plus_imp_minus);
apply (rule ln_real_approx_ln_nat);
done;
also have "... <= O(%x. ln(abs x + 1)) + O(%x. 1)";
apply (rule set_plus_mono2);
apply (rule order_trans);
apply (rule bigo_mult2);
apply (simp add: func_times);
apply (rule order_trans);
apply (rule bigo_mult);
apply (simp add: func_times);
apply (subgoal_tac "(%x. (abs x + 1) / (abs x + 1)) = (%x. 1)");
apply (erule ssubst);
apply simp;
apply (rule ext);
apply simp;
apply arith;
done;
also have "... <= O(%x. ln(abs x + 1) + 1)";
apply (subst bigo_plus_subset6 [THEN sym]);
apply force;
apply force;
apply (simp add: func_plus);
done;
finally show "(%x. (abs x + 1) * ln (abs x + 1)) -
(%x. (real (natfloor (abs x)) + 1) * ln (real (natfloor (abs x)) + 1))
: O(%x. ln (abs x + 1) + 1)";.;
qed;
lemma ln_x_squared_real_nat_approx: "(%x. (ln(abs x + 1))^2) =o
(%x. (ln(real (natfloor (abs x)) + 1))^2) +o
O(%x. (ln (abs x + 1)) / (abs x + 1))";
proof (rule set_minus_imp_plus);
have "(%x. ln (abs x + 1) ^ 2) - (%x. ln (real (natfloor (abs x)) + 1) ^ 2)
= (%x. ln(abs x + 1) - ln(real (natfloor (abs x))+1)) *
(%x. ln(abs x + 1) + ln(real (natfloor (abs x))+1))";
by (simp add: func_diff func_times realpow_two2 [THEN sym]
ring_eq_simps diff_minus);
also have "... =o O(%x. 1 / (abs x + 1)) * O(%x. ln(abs x + 1))";
apply (rule set_times_intro);
apply (subst func_diff [THEN sym]);back;
apply (rule set_plus_imp_minus);
apply (rule ln_real_approx_ln_nat);
apply (rule_tac c = 2 in bigo_bounded_alt);
apply (rule allI);
apply (rule nonneg_plus_nonneg);
apply (rule ln_ge_zero);
apply force;
apply (rule ln_ge_zero);
apply force;
apply (rule allI);
apply (subgoal_tac "ln(real (natfloor (abs x)) + 1) <=
ln(abs x + 1)");
apply force;
apply (subst ln_le_cancel_iff);
apply auto;
apply arith;
apply (rule real_natfloor_le);
apply force;
done;
also have "... <= O(%x. ln(abs x + 1) / (abs x + 1))";
apply (rule order_trans);
apply (rule bigo_mult);
apply (simp add: func_times);
done;
finally show "(%x. ln (abs x + 1) ^ 2) -
(%x. ln (real (natfloor (abs x)) + 1) ^ 2)
: O(%x. ln (abs x + 1) / (abs x + 1))";.;
qed;
lemma x_times_ln_x_squared_real_nat_approx:
"(%x. (abs x + 1) * (ln(abs x + 1))^2) =o
(%x.(real( natfloor(abs x)) + 1) *
(ln(real (natfloor (abs x)) + 1))^2) +o
O(%x. ln(abs x + 1) + (ln(abs x + 1))^2)";
proof (rule set_minus_imp_plus);
have "(%x. (abs x + 1) * ln (abs x + 1) ^ 2) -
(%x. (real (natfloor (abs x)) + 1) *
ln (real (natfloor (abs x)) + 1) ^ 2) =
(%x. (abs x + 1)) *
(%x. ln (abs x + 1)^2 - ln(real (natfloor (abs x)) + 1)^2) +
(%x. (abs x - real (natfloor (abs x)))) *
(%x. ln(real (natfloor (abs x)) + 1)^2)";
by (simp add: func_diff func_times func_plus ring_eq_simps
add_ac diff_minus);
also have "... =o (%x. abs x + 1) *o O(%x. ln (abs x + 1) / (abs x + 1)) +
O(%x. 1) * O(%x. ln (abs x + 1)^2)";
apply (rule set_plus_intro);
apply (rule set_times_intro2);
apply (subst func_diff [THEN sym]);back;
apply (rule set_plus_imp_minus);
apply (rule ln_x_squared_real_nat_approx);
apply (rule set_times_intro);
apply (rule bigo_bounded);
apply auto;
apply (rule real_natfloor_le);
apply force;
apply (subgoal_tac "abs x <= real (natfloor (abs x)) + 1");
apply force;
apply (rule real_natfloor_plus_one_ge);
apply (rule bigo_bounded);
apply auto;
apply (rule power_mono);
apply (subst ln_le_cancel_iff);
apply auto;
apply arith;
apply (rule real_natfloor_le);
apply force;
done;
also have "... <= O(%x. ln(abs x + 1)) + O(%x. ln(abs x + 1)^2)";
apply (rule set_plus_mono2);
apply (rule order_trans);
apply (rule bigo_mult2);
apply (subst func_times);
apply (subgoal_tac "(%u. (abs u + 1) * (ln (abs u + 1) / (abs u + 1))) =
(%u. ln (abs u + 1))");
apply simp;
apply (rule ext);
apply simp;
apply arith;
apply (rule order_trans);
apply (rule bigo_mult);
apply (simp add: func_times);
done;
also have "... <= O(%x. ln(abs x + 1) + ln(abs x + 1)^2)";
apply (subst bigo_plus_subset6 [THEN sym]);
apply force;
apply force;
apply (simp add: func_plus);
done;
finally show "(%x. (abs x + 1) * ln (abs x + 1) ^ 2) -
(%x. (real (natfloor (abs x)) + 1) *
ln (real (natfloor (abs x)) + 1) ^ 2)
=o O(%x. ln (abs x + 1) + ln (abs x + 1) ^ 2)";.;
qed;
lemma bigo_fix: "f =o O(g) ==> ALL x. 0 <= g x ==> ALL x. 0 <= h x ==>
ALL x. x < (a::'a::linorder) --> f x = 0 ==> 0 < c ==>
ALL x. a <= x --> g x <= c * (h x) ==>
f =o O(h)";
apply (subst bigo_def);
apply (simp only: bigo_alt_def);
apply auto;
apply (rule_tac x = "c * ca" in exI);
apply (rule allI);
apply (case_tac "x < a");
apply (subgoal_tac "f x = 0");
apply simp;
apply (rule nonneg_times_nonneg);
apply (rule nonneg_times_nonneg);
apply (erule order_less_imp_le)+;
apply (erule spec);
apply force;
apply (rule order_trans);
apply (subgoal_tac "abs (f x) <= ca * g x");
apply assumption;
apply (erule spec);
apply (subgoal_tac "c * ca * h x = ca * (c * h x)");
apply (erule ssubst);
apply (rule mult_left_mono);
apply (subgoal_tac "a <= x");
apply blast;
apply (subst linorder_not_less [THEN sym]);
apply assumption;
apply (rule order_less_imp_le);
apply assumption;
apply (simp add: mult_ac);
done;
lemma id_real_nat_approx_bigo: "(%x. abs x) =o
(%x. real (natfloor (abs x))) +o O(%x. 1)";
apply (rule set_minus_imp_plus);
apply (subst func_diff);
apply (rule bigo_bounded);
apply auto;
apply (rule real_natfloor_le);
apply force;
apply (subgoal_tac "abs x <= real(natfloor (abs x)) + 1");
apply force;
apply (rule real_natfloor_plus_one_ge);
done;
lemma one_plus_ln_plus_ln_squared_bigo:
"(%x. 1 + ln (abs x + 1) + ln(abs x + 1)^2) =o
O(%x. 1 + ln (abs x + 1)^2)";
apply (rule_tac c = "2 + ln (exp 1 + 1)" in bigo_bounded_alt);
apply (rule allI);
apply (subgoal_tac "0 <= ln(abs x + 1)");
apply (subgoal_tac "0 <= ln(abs x + 1)^2");
apply arith;
apply (rule zero_le_power);
apply (rule ln_ge_zero);
apply force;
apply (rule ln_ge_zero);
apply force;
apply (rule allI);
apply (simp add: ring_distrib);
apply (subst realpow_two2 [THEN sym]);
apply (case_tac "exp 1 <= abs x");
apply (subgoal_tac "ln (abs x + 1) <= ln(abs x + 1) * ln(abs x + 1)");
apply (subgoal_tac "0 <= (1 + (ln (exp 1 + 1) +
ln (exp 1 + 1) * (ln (abs x + 1) * ln (abs x + 1))))");
apply arith;
apply (rule nonneg_plus_nonneg);
apply force;
apply (rule nonneg_plus_nonneg);
apply force;
apply (rule nonneg_times_nonneg);
apply force;
apply force;
apply (subgoal_tac "ln (abs x + 1) * 1<= ln (abs x + 1) * ln (abs x + 1)");
apply simp;
apply (rule mult_left_mono);
apply (subgoal_tac "ln (exp 1) <= ln (abs x + 1)");
apply simp;
apply (subst ln_le_cancel_iff);
apply auto;
apply arith;
apply (subgoal_tac "0 + ln(abs x + 1) <= ln (abs x + 1) * ln (abs x + 1) +
(1 + (ln (exp 1 + 1) +
ln (exp 1 + 1) * (ln (abs x + 1) * ln (abs x + 1))))");
apply simp;
apply (rule add_mono);
apply force;
apply (subgoal_tac "0 + ln(abs x + 1) <= 1 + (ln (exp 1 + 1) +
ln (exp 1 + 1) * (ln (abs x + 1) * ln (abs x + 1)))");
apply simp;
apply (rule add_mono);
apply force;
apply (subgoal_tac "ln (abs x + 1) + 0 <= ln (exp 1 + 1) +
ln (exp 1 + 1) * (ln (abs x + 1) * ln (abs x + 1))");
apply simp;
apply (rule add_mono);
apply (subst ln_le_cancel_iff);
apply arith;
apply arith;
apply arith;
apply (rule nonneg_times_nonneg);
apply force;
apply (rule nonneg_times_nonneg);
apply auto;
done;
lemma identity_six_real: "(%x. sumr 0 (natfloor (abs x) + 1)
(%i. ln (real i + 1) ^ 2)) =o
((%x. (abs x + 1) * ln (abs x + 1) ^ 2) -
(%x. 2 * (abs x + 1) * ln (abs x + 1)) +
(%x. 2 * (abs x + 1))) +o O(%x. 1 + ln (abs x + 1) ^ 2)";
proof -;
have "(%x. sumr 0 (natfloor (abs x) + 1)
(%i. ln (real i + 1) ^ 2)) =o
((%x. (real (natfloor (abs x)) + 1) *
ln (real (natfloor (abs x)) + 1) ^ 2) -
(%x. 2) * (%x. (real (natfloor (abs x)) + 1) *
ln (real (natfloor (abs x)) + 1)) +
(%x. 2) * (%x. real (natfloor (abs x)))) +o
O(%x. ln (real (natfloor (abs x)) + 1) ^ 2)";
apply (insert bigo_compose2 [OF identity_six, of "%x. natfloor(abs x)"]);
apply (simp add: func_plus func_diff func_times func_minus ring_eq_simps);
done;
also have "... <=
(((%x. (abs x + 1) * ln(abs x + 1)^2) +o O(%x. ln(abs x + 1) +
ln(abs x + 1)^2)) +
((%x. 2) *o (-(%x. (abs x + 1) * ln(abs x + 1)) +o
O(%x. ln (abs x + 1) + 1))) +
((%x. 2) *o ((%x. abs x + 1) +o O(%x. 1)))) + O(%x. ln(abs x + 1)^2)";
apply (rule set_plus_mono5);
apply (rule set_plus_intro);
apply (simp add: diff_minus);
apply (rule set_plus_intro);
apply (rule bigo_add_commute_imp);
apply (rule x_times_ln_x_squared_real_nat_approx);
apply (subgoal_tac "- ((%x. 2) *
(%x. (real (natfloor (abs x)) + 1) *
ln (real (natfloor (abs x)) + 1))) =
(%x. 2) * -(%x. (real (natfloor (abs x)) + 1) *
ln (real (natfloor (abs x)) + 1))");
apply (erule ssubst);
apply (rule set_times_intro2);
apply (rule bigo_minus2);
apply (rule bigo_add_commute_imp);
apply (rule x_times_ln_x_real_nat_approx);
apply simp;
apply (rule set_times_intro2);
apply (rule bigo_add_commute_imp);
apply (rule set_minus_imp_plus);
apply (subst func_diff);
apply (rule_tac c = 2 in bigo_bounded_alt);
apply (rule allI);
apply (subgoal_tac "real( natfloor (abs x)) <= abs x");
apply arith;
apply (rule real_natfloor_le);
apply force;
apply (rule allI);
apply (subgoal_tac "abs x <= real(natfloor (abs x)) + 1");
apply simp;
apply (rule real_natfloor_plus_one_ge);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (rule power_mono);
apply (subst ln_le_cancel_iff);
apply force;
apply arith;
apply simp;
apply (rule real_natfloor_le);
apply simp;
apply force;
done;
also have "... = ((%x. (abs x + 1) * ln(abs x + 1)^2) -
(%x. 2 * (abs x + 1) * ln(abs x + 1)) +
(%x. 2 * (abs x + 1))) +o (
O(%x. 1) +
O(%x. ln (abs x + 1) + 1) +
O(%x. ln(abs x + 1) + ln(abs x + 1)^2) +
O(%x. ln(abs x + 1)^2))";
by (simp add: set_plus_rearranges ring_distrib plus_ac0 mult_ac
func_times func_minus set_times_plus_distribs diff_minus func_plus);
also have "... <= ((%x. (abs x + 1) * ln(abs x + 1)^2) -
(%x. 2 * (abs x + 1) * ln(abs x + 1)) +
(%x. 2 * (abs x + 1))) +o O(%x. 1 + ln(abs x + 1) + ln(abs x + 1)^2)";
apply (rule set_plus_mono);
apply (rule bigo_useful_intro)+;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (subgoal_tac "0 <= ln(abs x + 1)");
apply (subgoal_tac "0 <= ln(abs x + 1)^2");
apply arith;
apply (rule zero_le_power);
apply (rule ln_ge_zero);
apply force;
apply (rule ln_ge_zero);
apply force;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (subgoal_tac "0 <= ln(abs x + 1)");
apply arith;
apply (rule ln_ge_zero);
apply force;
apply (rule allI);
apply force;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (subgoal_tac "0 <= ln(abs x + 1)");
apply (subgoal_tac "0 <= ln(abs x + 1)^2");
apply arith;
apply (rule zero_le_power);
apply (rule ln_ge_zero);
apply force;
apply (rule ln_ge_zero);
apply force;
apply force;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (subgoal_tac "0 <= ln(abs x + 1)");
apply arith;
apply (rule ln_ge_zero);
apply arith;
done;
also; have "... <= ((%x. (abs x + 1) * ln (abs x + 1) ^ 2) -
(%x. 2 * (abs x + 1) * ln (abs x + 1)) +
(%x. 2 * (abs x + 1))) +o O(%x. 1 + ln(abs x + 1)^2)";
apply (rule set_plus_mono);
apply (rule bigo_elt_subset);
apply (rule one_plus_ln_plus_ln_squared_bigo);
done;
finally show ?thesis;.;
qed;
lemma better_ln_theorem2_real_cor: "(%x. ln(abs x + 1)) =o
(%x. sumr 0 (natfloor(abs x)+1) (%n. 1 / (real n + 1))) +o O(%x. 1)";
proof -;
note better_ln_theorem2_real;
also have "((%x. sumr 0 (natfloor (abs x) + 1) (%n. 1 / (real n + 1))) +
(%x. gamma)) +o O(%x. 1 / (abs x + 1)) =
(%x. sumr 0 (natfloor (abs x) + 1) (%n. 1 / (real n + 1))) +o
((%x. gamma) +o O(%x. 1 / (abs x + 1)))";
by (simp add: set_plus_rearranges);
also have "... <=
(%x. sumr 0 (natfloor (abs x) + 1) (%n. 1 / (real n + 1))) +o
(O(%x. 1) + O(%x. 1))";
apply (rule set_plus_mono);
apply (rule set_plus_mono5);
apply (rule bigo_const1);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply arith;
apply (rule allI);
apply (rule real_le_mult_imp_div_pos_le);
apply arith;
apply simp;
done;
also have "O(%x. 1) + O(%x. 1) = O(%x. 1)";
by (rule bigo_plus_idemp);
finally show ?thesis;.;
qed;
lemma identity_three_real: "(%x. sumr 0 (natfloor(abs x) + 1)
(%i. ln (real i + 1))) =o
((%x. (abs x + 1) * ln (abs x + 1)) - (%x. abs x + 1)) +o
O(%x. 1 + ln (abs x + 1))";
proof -;
have "(%x. sumr 0 (natfloor (abs x) + 1) (%i. ln (real i + 1))) =o
((%x. (real (natfloor(abs x)) + 1) *
(ln(real (natfloor (abs x)) + 1))) + -
(%x. (real (natfloor(abs x))))) +o
O(%x. ln(real(natfloor(abs x)) + 1))";
apply (insert bigo_compose2 [OF identity_three, of "%x. natfloor(abs x)"]);
apply (simp add: func_plus func_minus diff_minus ring_eq_simps);
done;
also have "... <=
((%x. (abs x + 1) * ln (abs x + 1)) +o O(%x. ln(abs x + 1) + 1)) +
((-(%x. abs x + 1)) +o O(%x. 1)) +
O(%x. ln(abs x + 1))";
apply (rule set_plus_mono5);
apply (rule set_plus_intro);
apply (rule bigo_add_commute_imp);
apply (rule x_times_ln_x_real_nat_approx);
apply (rule bigo_minus2);
apply (rule bigo_add_commute_imp);
apply (rule set_minus_imp_plus);
apply (subst func_diff);
apply (rule_tac c = 2 in bigo_bounded_alt);
apply clarsimp;
apply (subgoal_tac "real(natfloor (abs x)) <= abs x");
apply simp;
apply (rule real_natfloor_le);
apply force;
apply clarsimp;
apply (subgoal_tac "abs x <= real(natfloor (abs x)) + 1");
apply arith;
apply (rule real_natfloor_plus_one_ge);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (subst ln_le_cancel_iff);
apply auto;
apply arith;
apply (rule real_natfloor_le);
apply force;
done;
also have "... = ((%x. (abs x + 1) * ln (abs x + 1)) - (%x. abs x + 1)) +o
(O(%x. ln(abs x + 1) + 1) + (O(%x. ln(abs x + 1)) + O(%x. 1)))";
by (simp add: diff_minus set_plus_rearranges plus_ac0);
also have "... <= ((%x. (abs x + 1) * ln (abs x + 1)) - (%x. abs x + 1)) +o
O(%x. ln(abs x + 1) + 1)";
apply (rule set_plus_mono);
apply (rule bigo_useful_intro);
apply simp;
apply (subst bigo_plus_subset6 [THEN sym]);
apply force;
apply force;
apply (simp add: func_plus);
done;
also have "(%x. ln(abs x + 1) + 1) = (%x. 1 + ln(abs x + 1))";
by (simp add: add_ac);
finally show ?thesis;.;
qed;
lemma sum_ln_x_div_x_squared_real_bigo: "(%x. sumr 0 (natfloor (abs x) + 1)
(%i. ln ((abs x + 1) / (real i + 1))^2)) =o (%x. 2 * (abs x + 1))
+o O(%x. 1 + ln(abs x + 1) + ln(abs x + 1)^2)";
proof -;
have "(%x. sumr 0 (natfloor (abs x) + 1)
(%i. ln ((abs x + 1) / (real i + 1))^2))
= (%x. sumr 0 (natfloor (abs x) + 1)
(%i. ln (abs x + 1)^2 - 2 * ln(abs x + 1) * ln(real i + 1) +
ln (real i + 1)^2))";
apply (rule ext);
apply (rule sumr_cong);
apply (subst ln_div);
apply arith;
apply force;
apply (simp add: realpow_two2 [THEN sym] ring_eq_simps
ring_distrib);
done;
also have "... = (%x. sumr 0 (natfloor (abs x) + 1)
(%i. ln(abs x + 1)^2)) +
(-(%x. 2 * ln(abs x + 1))) * (%x. sumr 0 (natfloor (abs x) + 1)
(%i. ln(real i + 1))) +
(%x. sumr 0 (natfloor (abs x) + 1)
(%i. ln(real i + 1)^2))";
apply (simp only: func_plus func_minus func_times);
apply (rule ext);
apply (subst sumr_mult);
apply (subst sumr_add);
apply (subst sumr_add);
apply (rule sumr_cong);
apply (simp add: diff_minus);
done;
also have "... =o
((%x. (abs x + 1) * ln(abs x + 1)^2) +o O(%x. ln(abs x + 1)^2)) +
((-(%x. 2 * ln(abs x + 1))) *o (((%x. (abs x + 1) * ln (abs x + 1)) -
(%x. abs x + 1)) +o O(%x. 1 + ln (abs x + 1)))) +
(((%x. (abs x + 1) * ln (abs x + 1) ^ 2) -
(%x. 2 * (abs x + 1) * ln (abs x + 1)) +
(%x. 2 * (abs x + 1))) +o O(%x. 1 + ln (abs x + 1) ^ 2))";
apply (rule set_plus_intro);
apply (rule set_plus_intro);
apply (rule bigo_add_commute_imp);
apply (rule set_minus_imp_plus);
apply (subst func_diff);
apply (simp only: sumr_const);
apply (simp only: left_diff_distrib [THEN sym]);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule nonneg_times_nonneg);
apply (subgoal_tac "real( natfloor (abs x)) <= abs x");
apply arith;
apply (rule real_natfloor_le);
apply force;
apply force;
apply (rule allI);
apply (subgoal_tac "?t <= 1 * ln(abs x + 1)^2");
apply simp;
apply (rule mult_right_mono);
apply simp;
apply (subgoal_tac "abs x <= real(natfloor(abs x)) + 1");
apply force;
apply (rule real_natfloor_plus_one_ge);
apply force;
apply (rule set_times_intro2);
apply (rule identity_three_real);
apply (rule identity_six_real);
done;
also have "... = (%x. 2 * (abs x + 1)) +o
(O(%x. ln (1 + abs x)^2) + O(%x. 1 + ln (1 + abs x)^2) +
(((%x. -2) * (%x. (ln (1 + abs x)))) *o
O(%x. 1 + ln (1 + abs x))))";
apply (simp add: set_plus_rearranges set_times_plus_distribs plus_ac0
func_plus func_times func_diff func_minus ring_eq_simps ring_distrib
mult_ac realpow_two2 [THEN sym]);
apply (subgoal_tac "(%x. - (ln (1 + abs x) * 2)) =
(%x. -2 * ln (1 + abs x))");
apply (erule ssubst, rule refl);
apply (rule ext);
apply simp;
done;
also have "... <= (%x. 2 * (abs x + 1)) +o O(%x. 1 + ln(1 + abs x)
+ ln(1 + abs x)^2)";
apply (rule set_plus_mono);
apply (rule bigo_useful_intro);
apply (rule bigo_useful_intro);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply clarsimp;
apply (subgoal_tac "0 <= ln(1 + abs x)");
apply arith;
apply (rule ln_ge_zero);
apply arith;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule nonneg_plus_nonneg);
apply force;
apply force;
apply (rule allI);
apply clarsimp;
apply (subgoal_tac "((%x. -2) * (%x. ln (1 + abs x))) *o
O(%x. 1 + ln (1 + abs x)) =
(%x. -2) *o ((%x. ln (1 + abs x)) *o O(%x. 1 + ln (1 + abs x)))");
apply (erule ssubst);
apply (rule order_trans);
prefer 2;
apply (subgoal_tac "(%x. -2) *o ?t <= ?t");
apply assumption;
apply (rule bigo_const_mult6);
apply (rule set_times_mono);
apply (rule order_trans);
apply (rule bigo_mult2);
apply (simp add: func_times ring_distrib realpow_two2 [THEN sym]);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule nonneg_plus_nonneg);
apply (rule ln_ge_zero);
apply arith;
apply (rule nonneg_times_nonneg);
apply (rule ln_ge_zero, arith)+;
apply arith;
apply (simp add: set_times_rearranges times_ac1);
done;
finally show ?thesis;
by (simp add: add_ac);
qed;
lemma power_ln_bigo: "(%x. ln(abs x + 1) ^ n) =o
O(%x. abs x + 1)";
apply (case_tac "n = 0");
apply (erule ssubst);
apply (rule bigo_bounded);
apply force;
apply force;
apply (rule_tac c = "(real n) powr (real n)" in bigo_bounded_alt);
apply (rule allI);
apply (rule zero_le_power);
apply (rule ln_ge_zero);
apply arith;
apply (rule allI);
apply (subst powr_realpow2);
apply (rule ln_ge_zero);
apply arith;
apply force;
apply (case_tac "x = 0");
apply simp;
apply (subgoal_tac "ln(abs x + 1) ~= 0");
apply simp;
apply (rule ln_powr_bound2);
apply arith;
apply force;
apply (subgoal_tac "0 < ln(abs x + 1)");
apply force;
apply (rule ln_gt_zero);
apply arith;
done;
lemma sum_ln_x_div_x_squared_real_bigo_cor:
"(%x. sumr 0 (natfloor (abs x) + 1)
(%i. ln ((abs x + 1) / (real i + 1))^2)) =o O(%x. abs x + 1)";
proof -;
note sum_ln_x_div_x_squared_real_bigo;
also have "(%x. 2 * (abs x + 1)) +o O(%x. 1 + ln (abs x + 1) +
ln (abs x + 1) ^ 2) <=
O(%x. (abs x + 1)) + (O(%x. 1) + O(%x. ln(abs x + 1)) +
O(%x. ln (abs x + 1)^2))";
apply (rule set_plus_mono5);
apply (rule_tac c = 2 in bigo_bounded_alt);
apply (rule allI);
apply simp;
apply arith;
apply force;
apply (rule order_trans);
prefer 2;
apply (rule set_plus_mono2);
apply (rule bigo_plus_subset);
apply force;
apply (subst func_plus);
apply (rule order_trans);
prefer 2;
apply (rule bigo_plus_subset);
apply (subst func_plus);
apply simp;
done;
also have "... <= O(%x. abs x + 1)";
apply (rule bigo_useful_intro);
apply simp;
apply (rule bigo_useful_intro);
apply (rule bigo_useful_intro);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply arith;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (rule ln_bound);
apply arith;
apply (rule bigo_elt_subset);
apply (rule power_ln_bigo);
done;
finally show ?thesis;.;
qed;
lemma telescoping_sum_aux: "(∑n = 1..x+1. f n - f (n - 1)) =
f (x+1) - (f::(nat => 'a::ordered_ring)) 0";
apply (induct x);
apply simp;
apply (subgoal_tac "{1..Suc n + 1} = {1..n + 1} Un {Suc n + 1}");
apply (erule ssubst);back;
apply (subst setsum_Un_disjoint);
apply force;
apply force;
apply force;
apply (erule ssubst);
apply (simp add: compare_rls plus_ac0);
apply auto;
done;
lemma telescoping_sum: "1 <= x ==> (∑n = 1..x. f n - f (n - 1)) =
f x - (f::(nat => 'a::ordered_ring)) 0";
apply (subgoal_tac "x = (x - 1) + 1");
apply (erule ssubst);
apply (rule telescoping_sum_aux);
apply simp;
done;
lemma ln_one_plus_one_over_x_bigo:
"(%x. ln (1 + 1 / (real x + 1))) =o O(%x. 1 / (real (x::nat) + 1))";
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (rule ln_add_one_self_le_self);
apply force;
done;
lemma identity_four_real: "(%x. sumr 0 (natfloor(abs x))
(%i. ln (real i + 1) / (real i + 1))) =o
(%x. ln(abs x + 1)^2 / 2) +o O(%x. 1)"
(is "?LHS =o ?RHS");
proof -;
have "?LHS =o (%x. ln (real(natfloor(abs x)) + 1) ^ 2 / 2) +o O(%x. 1)";
by (rule bigo_compose2 [OF identity_four]);
also have "... <= ?RHS + O(%x. 1)";
apply (rule set_plus_mono3);
apply (rule set_minus_imp_plus);
apply (subgoal_tac "(%x. ln (real (natfloor (abs x)) + 1) ^ 2 / 2) -
(%x. ln (abs x + 1) ^ 2 / 2) = (%x. 1 / 2) *
((%x. ln (real (natfloor (abs x)) + 1) ^ 2) -
(%x. ln (abs x + 1) ^ 2))");
apply (erule ssubst);
apply (subgoal_tac "O(%x. 1) = (%x. 1 / 2) *o O(%x. 1)");
apply (erule ssubst);
apply (rule set_times_intro2);
apply (rule set_plus_imp_minus);
apply (rule bigo_add_commute_imp);
apply (rule subsetD);
prefer 2;
apply (rule ln_x_squared_real_nat_approx);
apply (rule set_plus_mono);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply arith;
apply (rule allI);
apply (rule real_le_mult_imp_div_pos_le);
apply arith;
apply simp;
apply (rule ln_bound);
apply force;
apply (rule bigo_const_mult5 [THEN sym]);
apply force;
apply (simp add: func_times func_diff);
apply (rule ext);
apply simp;
done;
also have "... <= ?RHS";
by (simp add: set_plus_rearranges);
finally show ?thesis;.;
qed;
lemma identity_four_real_b: "(%x. ∑i=1..natfloor(abs x).
ln (real i) / (real i)) =o
(%x. ln(abs x + 1)^2 / 2) +o O(%x. 1)";
apply (subgoal_tac "(%x. ∑i=1..natfloor(abs x).
ln (real i) / (real i)) = ?temp");
apply (erule ssubst);
apply (rule identity_four_real);
apply (rule ext);
apply (subst setsum_sumr4);
apply (rule sumr_cong);
apply (subgoal_tac "real(y + 1) = real y + 1");
apply (erule ssubst);
apply (rule refl);
apply simp;
done;
lemma identity_four_real_b_cor: "(%x. ∑i=1..natfloor(abs x)+1.
ln (real i) / (real i)) =o
(%x. ln(abs x + 1)^2 / 2) +o O(%x. 1)";
proof -;
have "(%x. ∑i=1..natfloor(abs x)+1.
ln (real i) / (real i)) = (%x. ∑i=1..natfloor(abs x).
ln (real i) / (real i)) + (%x. ln (real (natfloor(abs x)+1)) /
(real (natfloor(abs x)+1)))";
apply (subst func_plus);
apply (rule ext);
apply (case_tac "natfloor(abs x) = 0");
apply simp;
apply (rule setsum_range_plus_one_nat);
apply force;
done;
also have "... =o ((%x. ln(abs x + 1)^2 / 2) +o O(%x. 1)) + O(%x. 1)";
apply (rule set_plus_intro);
apply (rule identity_four_real_b);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (rule real_le_mult_imp_div_pos_le);
apply auto;
apply (rule ln_bound);
apply auto;
done;
finally show ?thesis by (simp add: set_plus_rearranges);
qed;
lemma ln_sum_real2: "(%x. ln(abs x + 1)) =o
(%x. ∑i=1..natfloor(abs x)+1. 1 / (real i)) +o
O(%x. 1)";
proof -;
have "(%x. ln (abs x + 1)) =o
((%x. sumr 0 (natfloor (abs x) + 1) (%n. 1 / (real n + 1))) +
(%x. gamma)) +o O(%x. 1 / (abs x + 1))";
by (rule better_ln_theorem2_real);
also have "(%x. sumr 0 (natfloor (abs x) + 1) (%n. 1 / (real n + 1)))
= (%x. ∑i=1..natfloor(abs x)+1. 1 / (real i))";
apply (rule ext);
apply (subst setsum_sumr4);
apply (rule sumr_cong);
apply simp;
done;
also; have "((%x. ∑ i = 1..natfloor (abs x) + 1. 1 / real i) +
(%x. gamma)) +o O(%x. 1 / (abs x + 1)) =
(%x. ∑ i = 1..natfloor (abs x) + 1. 1 / real i) +o
((%x. gamma) +o O(%x. 1 / (abs x + 1)))";
by (simp add: set_plus_rearranges);
also have "... <= (%x. ∑ i = 1..natfloor (abs x) + 1. 1 / real i) +o
O(%x. 1)";
apply (rule set_plus_mono);
apply (rule bigo_plus_absorb2);
apply (rule bigo_const1);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply arith;
apply (rule allI);
apply (rule real_le_mult_imp_div_pos_le);
apply arith;
apply auto;
done;
finally show ?thesis;.;
qed;
lemma bigo_one_subset_bigo_one_plus_ln:
"O(%x. 1) <= O(%x. 1 + ln (abs x + 1))";
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply auto;
done;
lemma bigo_ln_subset_bigo_one_plus_ln:
"O(%x. ln (abs x + 1)) <= O(%x. 1 + ln (abs x + 1))";
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply auto;
done;
declare One_nat_def [simp del];
lemma one_over_natfloor_one_over_bigo:
"(%x. 1 / real (natfloor (abs x) + 1)) =o O(%x. 1 / (abs x + 1))";
apply (rule_tac c = 2 in bigo_bounded_alt);
apply force;
apply (rule allI);
apply simp;
apply (rule real_fraction_le);
apply arith;
apply force;
apply simp;
apply (subgoal_tac "abs x <= real(natfloor(abs x)) + 1");
apply arith;
apply (rule real_natfloor_plus_one_ge);
done;
declare One_nat_def [simp add];
subsection {* Not needed? *}
lemma divides_div_bigo: "(%d. real x / real (d + (1::nat))) =o
(%d. real(x div (d + 1))) +o O(%d. 1)";
apply (rule set_minus_imp_plus);
apply (subst func_diff);
apply (rule bigo_bounded);
apply clarify;
apply (rule real_mult_le_imp_le_div_pos);
apply force;
apply (subst real_of_nat_mult [THEN sym]);
apply (rule le_imp_real_of_nat_le);
apply (rule nat_div_times_le);
apply (rule allI);
apply (subst divide_div_aux);
apply force;
apply simp;
apply (rule real_le_mult_imp_div_pos_le);
apply auto;
apply (rule order_less_imp_le);
apply auto;
done;
end;
lemma bigo_real_inverse_nat_inverse:
O(%x. 1 / (¦x¦ + 1)) = O(%x. 1 / (real (natfloor ¦x¦) + 1))
lemma ln_real_approx_ln_nat:
(%x. ln (¦x¦ + 1)) ∈ (%x. ln (real (natfloor ¦x¦) + 1)) + O(%x. 1 / (¦x¦ + 1))
lemma better_ln_theorem2_real:
(%x. ln (¦x¦ + 1)) ∈ ((%x. sumr 0 (natfloor ¦x¦ + 1) (%n. 1 / (real n + 1))) + (%x. gamma)) + O(%x. 1 / (¦x¦ + 1))
lemma identity_three_cor:
(%n. sumr 0 (n + 1) (%i. ln (real i + 1))) ∈ (%n. (real n + 1) * ln (real n + 1)) + O(real)
lemma natfloor_bigo:
(%x. real (natfloor ¦x¦) + 1) ∈ O(%x. ¦x¦ + 1)
lemma identity_three_cor_real:
(%x. sumr 0 (natfloor ¦x¦ + 1) (%i. ln (real i + 1))) ∈ (%x. real (natfloor ¦x¦ + 1) * ln (¦x¦ + 1)) + O(%x. ¦x¦ + 1)
lemma natfloor_bigo:
(%x. ¦x¦ - real (natfloor ¦x¦)) ∈ O(%x. 1)
lemma x_times_ln_x_real_nat_approx:
(%x. (¦x¦ + 1) * ln (¦x¦ + 1)) ∈ (%x. (real (natfloor ¦x¦) + 1) * ln (real (natfloor ¦x¦) + 1)) + O(%x. ln (¦x¦ + 1) + 1)
lemma ln_x_squared_real_nat_approx:
(%x. (ln (¦x¦ + 1))²) ∈ (%x. (ln (real (natfloor ¦x¦) + 1))²) + O(%x. ln (¦x¦ + 1) / (¦x¦ + 1))
lemma x_times_ln_x_squared_real_nat_approx:
(%x. (¦x¦ + 1) * (ln (¦x¦ + 1))²) ∈ (%x. (real (natfloor ¦x¦) + 1) * (ln (real (natfloor ¦x¦) + 1))²) + O(%x. ln (¦x¦ + 1) + (ln (¦x¦ + 1))²)
lemma bigo_fix:
[| f ∈ O(g); ∀x. (0::'b) ≤ g x; ∀x. (0::'b) ≤ h x; ∀x<a. f x = (0::'b); (0::'b) < c; ∀x. a ≤ x --> g x ≤ c * h x |] ==> f ∈ O(h)
lemma id_real_nat_approx_bigo:
abs ∈ (%x. real (natfloor ¦x¦)) + O(%x. 1)
lemma one_plus_ln_plus_ln_squared_bigo:
(%x. 1 + ln (¦x¦ + 1) + (ln (¦x¦ + 1))²) ∈ O(%x. 1 + (ln (¦x¦ + 1))²)
lemma identity_six_real:
(%x. sumr 0 (natfloor ¦x¦ + 1) (%i. (ln (real i + 1))²)) ∈ ((%x. (¦x¦ + 1) * (ln (¦x¦ + 1))²) - (%x. 2 * (¦x¦ + 1) * ln (¦x¦ + 1)) + (%x. 2 * (¦x¦ + 1))) + O(%x. 1 + (ln (¦x¦ + 1))²)
lemma better_ln_theorem2_real_cor:
(%x. ln (¦x¦ + 1)) ∈ (%x. sumr 0 (natfloor ¦x¦ + 1) (%n. 1 / (real n + 1))) + O(%x. 1)
lemma identity_three_real:
(%x. sumr 0 (natfloor ¦x¦ + 1) (%i. ln (real i + 1))) ∈ ((%x. (¦x¦ + 1) * ln (¦x¦ + 1)) - (%x. ¦x¦ + 1)) + O(%x. 1 + ln (¦x¦ + 1))
lemma sum_ln_x_div_x_squared_real_bigo:
(%x. sumr 0 (natfloor ¦x¦ + 1) (%i. (ln ((¦x¦ + 1) / (real i + 1)))²)) ∈ (%x. 2 * (¦x¦ + 1)) + O(%x. 1 + ln (¦x¦ + 1) + (ln (¦x¦ + 1))²)
lemma power_ln_bigo:
(%x. ln (¦x¦ + 1) ^ n) ∈ O(%x. ¦x¦ + 1)
lemma sum_ln_x_div_x_squared_real_bigo_cor:
(%x. sumr 0 (natfloor ¦x¦ + 1) (%i. (ln ((¦x¦ + 1) / (real i + 1)))²)) ∈ O(%x. ¦x¦ + 1)
lemma telescoping_sum_aux:
(∑n = 1..x + 1. f n - f (n - 1)) = f (x + 1) - f 0
lemma telescoping_sum:
1 ≤ x ==> (∑n = 1..x. f n - f (n - 1)) = f x - f 0
lemma ln_one_plus_one_over_x_bigo:
(%x. ln (1 + 1 / (real x + 1))) ∈ O(%x. 1 / (real x + 1))
lemma identity_four_real:
(%x. sumr 0 (natfloor ¦x¦) (%i. ln (real i + 1) / (real i + 1))) ∈ (%x. (ln (¦x¦ + 1))² / 2) + O(%x. 1)
lemma identity_four_real_b:
(%x. ∑i = 1..natfloor ¦x¦. ln (real i) / real i) ∈ (%x. (ln (¦x¦ + 1))² / 2) + O(%x. 1)
lemma identity_four_real_b_cor:
(%x. ∑i = 1..natfloor ¦x¦ + 1. ln (real i) / real i) ∈ (%x. (ln (¦x¦ + 1))² / 2) + O(%x. 1)
lemma ln_sum_real2:
(%x. ln (¦x¦ + 1)) ∈ (%x. ∑i = 1..natfloor ¦x¦ + 1. 1 / real i) + O(%x. 1)
lemma bigo_one_subset_bigo_one_plus_ln:
O(%x. 1) ⊆ O(%x. 1 + ln (¦x¦ + 1))
lemma bigo_ln_subset_bigo_one_plus_ln:
O(%x. ln (¦x¦ + 1)) ⊆ O(%x. 1 + ln (¦x¦ + 1))
lemma one_over_natfloor_one_over_bigo:
(%x. 1 / real (natfloor ¦x¦ + 1)) ∈ O(%x. 1 / (¦x¦ + 1))
lemma divides_div_bigo:
(%d. real x / real (d + 1)) ∈ (%d. real (x div (d + 1))) + O(%d. 1)