# Theory MuSum

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

theory MuSum = Inversion + RealLnSum + Chebyshev3:

```(*  Title:      MuSum.thy
*)

header {* Sums involving mu *}

theory MuSum = Inversion + RealLnSum + Chebyshev3:;

subsection {* Variants of inversion laws *}

constdefs mu2 :: "(nat => real)"
"mu2 d == real(mu(int(d)))";

lemma mu_inversion_nat1_real: "ALL n. (0 < n -->
f n = (∑d:{d. d dvd n}. g(n div d))) ==> 0 < (n::nat) ==>
g n = (∑d:{d. d dvd n}. (mu2 d) * f (n div d))";
apply (unfold mu2_def);
apply (subst mu_inversion_nat1a [of f g]);
apply assumption+;
apply (subst real_eq_of_int [THEN sym]);
apply (rule refl);
done;

lemma mu_inversion_nat2_real: "ALL n. (0 < n -->
g n = (∑d:{d. d dvd n}. (mu2 d) * f(n div d))) ==>
0 < (n::nat) ==> f n = (∑d:{d. d dvd n}. g (n div d))";
apply (unfold mu2_def);
apply (subst mu_inversion_nat2a [of g f]);
apply (subst real_eq_of_int [THEN sym]);
apply assumption+;
apply (rule refl);
done;

lemma mu_inversion_nat3_real: "0 < (n::nat) ==> g n =
(∑d:{)0..n}. (∑d':{)0..(n div d)}.
(mu2 d) * g((n div d) div d')))";
apply (unfold mu2_def);
apply (subst mu_inversion_nat3 [of n g]);
apply assumption;
apply (subst real_eq_of_int [THEN sym]);
apply (rule refl);
done;

lemma abs_mu2_leq_1: "abs(mu2 x) <= 1";
apply (unfold mu2_def mu_def);
apply simp;
done;

lemma mu_inversion_nat1a':
"[| ALL n. 0 < n --> f n = (∑ d | d dvd n. g d); 0 < n |]
==> g n = (∑ d | d dvd n. of_int (mu (int d)) * f (n div d))";
apply (rule mu_inversion_nat1a);
apply (clarify);
apply (subst general_inversion_nat1);
apply assumption;
apply (drule_tac x = "na" in spec);
apply simp;
apply (rule setsum_cong2);
apply (subst nat_div_div);
apply auto;
done;

lemma mu_inversion_nat1a'_real:
"[| ALL n. 0 < n --> f n = (∑ d | d dvd n. g d); 0 < n |]
==> g n = (∑ d | d dvd n. mu2 d * f (n div d))";
apply (unfold mu2_def);
apply (subst mu_inversion_nat1a' [of f g]);
apply assumption+;
apply (subst real_eq_of_int [THEN sym]);
apply (rule refl);
done;

lemma aux3: "{)0..(n::nat)} = {1..n}";
by auto;

lemma general_inversion_nat2_modified: "0 < (n::nat) ==>
(∑d=1..n. ∑d'=1..n div d. f d d') =
(∑c=1..n. ∑ d | d dvd c. f d (c div d))";
apply (subst aux3 [THEN sym]);
apply (subst general_inversion_nat2 [THEN sym]);
apply assumption;
apply (rule setsum_cong2);
apply (subst aux3);
apply (rule refl);
done;

lemma general_inversion_nat2_cor1_modified: "0 < (n::nat)
==> (∑d=1..n. ∑d'=1..n div d. f d d') =
(∑d'=1..n. ∑d=1..n div d'. f d d')";
apply (subgoal_tac "(∑d=1..n. ∑d'=1..n div d. f d d') =
(∑d:{)0..n}. ∑d':{)0..n div d}. f d d')");
apply (erule ssubst);
apply (subst general_inversion_nat2_cor1);
apply assumption;
apply (subst aux3);
apply (rule setsum_cong2);
apply (subst aux3);
apply (rule refl);
apply (subst aux3);
apply (rule setsum_cong2);
apply (subst aux3);
apply (rule refl);
done;

subsection {* Sum of mu div n *}

lemma sumr_mu_div_n_bigo: "(%x. sumr 0 (x+1) (%n. mu2(n+1) / real(n+1))) =o
O(%x. 1)";
proof -;
have "(%x. 1) = (%x. ∑d: {)0..x+1}. ∑d':{)0..(x+1) div d}. mu2 d)";
proof (rule ext);
fix x;
show "1 = (∑d: {)0..x+1}. ∑d':{)0..(x+1) div d}. mu2 d)";
proof -;
have "(∑d∈{)0..x+1}. ∑d':{)0..(x+1) div d}. mu2 d) =
(∑d∈{)0..x+1}. ∑d':{)0..(x+1) div d}. mu2 d *
1)";
by simp;
also have "... = 1";
apply (rule mu_inversion_nat3_real [of "x+1" "%x. 1", THEN sym]);
apply force;
done;
finally show ?thesis; by (rule sym);
qed;
qed;
also have "... = (%x. ∑d: {)0..x+1}. real((x+1) div d) * mu2 d)";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst real_eq_of_nat);
apply (subst setsum_constant);
apply simp;
apply simp;
done;
also have "... =
(%x. sumr 0 (x+1) (%d. real((x+1) div (d+1)) * mu2 (d+1)))";
apply (rule ext);
apply (rule setsum_sumr3);
done;
also have "... =o
(%x. sumr 0 (x+1) (%d. real (x+1) / real(d+1) * mu2(d+1)))
+o O(%x. sumr 0 (x+1) (%d. 1))" (is "?LHS =o ?term1 +o ?term2")
apply (rule bigo_compose2);
apply (rule bigo_sumr6);
apply force;
apply (rule_tac x = 1 in exI);
apply (rule allI)+;
apply (subgoal_tac "abs(real (x div (y + 1)) * mu2 (y + 1) -
real x / real (y + 1) * mu2 (y + 1)) =
abs(real(x div (y + 1)) - real x / real (y + 1)) * abs(mu2(y+1))");
apply (erule ssubst);
apply (rule mult_mono);
apply (subgoal_tac "real (x div (y + 1)) - real x / real (y + 1) <= 0");
apply simp;
apply (rule nat_div_real_div [THEN conjunct2]);
apply (subgoal_tac "0 <= real x / real (y + 1) - real(x div (y + 1))");
apply simp;
apply (rule nat_div_real_div [THEN conjunct1]);
apply simp;
apply (rule abs_mu2_leq_1);
apply force;
apply force;
apply (simp del: abs_mult add: abs_mult [THEN sym] ring_eq_simps);
done;
also have "(%x. sumr 0 (x + 1) (%d. 1)) = (%x. real(x + 1))";
apply (rule ext);
apply (subst sumr_const);
apply simp;
done;
also; have "?term1 = (%x. real (x + 1) * sumr 0 (x + 1)
(%n. mu2(n+1) / real(n+1)))";
apply (rule ext);
apply (subst sumr_mult);
apply simp;
done;
finally; have "(%x. real (x + 1) *
sumr 0 (x + 1) (%n. mu2 (n + 1) / real (n + 1))) =o
(%x. 1) +o O(%x. real(x + 1))";
also have "... <= O(%x. real(x+1))";
apply (rule bigo_plus_absorb_lemma1);
apply (rule bigo_bounded);
apply auto;
done;
finally have "(%x. real (x + 1) *
sumr 0 (x + 1) (%n. mu2 (n + 1) / real (n + 1))) =o O(%x. real(x+1))"
(is "?term3 =o ?term4");.;
then have "(%x. 1 / real (x + 1)) * ?term3 =o
(%x. 1 / real (x + 1)) *o ?term4";
by (rule set_times_intro2);
also have "... <= O((%x. (1 / real (x + 1))) * (%x. real(x + 1)))";
by (rule bigo_mult2);
finally show ?thesis;
qed;

subsection {* Sum of mu div n times ln n over n *}

lemma aux_nat_diff: "(a::nat) <= x ==> x - a + a = x";
by auto;

lemma aux: "(%x. sumr 0 (natfloor(abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / (real (y + 1)))))
=o (%x. sumr 0 (natfloor(abs x) + 1)
(%y. mu2 (y + 1) / (real (y + 1)) *
(sumr 0 (natfloor((abs x + 1) / real (y + 1)))
(%n. 1 / (real n + 1)) +
gamma))) +o O(%x. 1)"
(is "?LHS =o ?RH1 +o O(%x. 1)");
proof -;
note bigo_sumr8 [OF better_ln_theorem2_real, of
"%x. natfloor(abs x) + 1"
"%x y. mu2(y+1) / real(y+1)"
"%x y. ((abs x) + 1) / (real (y+1)) - 1"];
also have "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
ln (abs ((abs x + 1) / real (y + 1) - 1) + 1))) = ?LHS";
apply (rule ext);
apply (rule sumr_cong);
apply (subst abs_nonneg);back;back;
apply (simp del: One_nat_def);
apply (rule div_ge_1);
apply auto;
apply (subgoal_tac "real(natfloor(abs x)) <= abs x");
apply force;
apply (rule real_natfloor_le);
apply force;
done;
also have "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
((%x. sumr 0 (natfloor (abs x) + 1) (%n. 1 / (real n + 1))) +
(%x. gamma))
((abs x + 1) / real (y + 1) - 1))) = ?RH1";
apply (rule ext);
apply (rule sumr_cong);
apply (simp only: func_plus);
apply (subgoal_tac "natfloor(abs ((abs x + 1) / real (y + 1) - 1)) + 1 =
natfloor((abs x + 1) / real (y + 1))");
apply (erule ssubst);
apply (rule refl);
apply (subst abs_nonneg);back;back;
apply (simp del: One_nat_def);
apply (rule div_ge_1);
apply force;
apply simp;
apply (subgoal_tac "real y <= real (natfloor (abs x))");
apply (erule order_trans);
apply (rule real_natfloor_le);
apply force;
apply simp;
apply (subgoal_tac "1 = real 1");
apply (erule ssubst);
apply (subst natfloor_subtract);
apply simp;
apply (rule div_ge_1);
apply force;
apply (subgoal_tac "real(Suc y) = real y + 1");
apply (erule ssubst);
apply simp;
apply (subgoal_tac "real y <= real (natfloor (abs x))");
apply (erule order_trans);
apply (rule real_natfloor_le);
apply force;
apply force;
apply simp;
apply (rule aux_nat_diff);
apply (rule real_le_natfloor);
apply simp;
apply (rule div_ge_1);
apply force;
apply (subgoal_tac "real(Suc y) = real y + 1");
apply (erule ssubst);
apply simp;
apply (subgoal_tac "real y <= real (natfloor (abs x))");
apply (erule order_trans);
apply (rule real_natfloor_le);
apply force;
apply force;
apply simp;
apply simp;
done;
also; have "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. abs (mu2 (y + 1) / real (y + 1) *
(1 / (abs ((abs x + 1) / real (y + 1) - 1) + 1))))) =
(%x. sumr 0 (natfloor (abs x) + 1) (%y. abs(mu2 (y + 1)) / (abs x + 1)))";
apply (rule ext);
apply (rule sumr_cong);
proof -;
fix x; fix y;
assume "y < natfloor (abs x) + 1";
show "abs (mu2 (y + 1) / real (y + 1) *
(1 / (abs ((abs x + 1) / real (y + 1) - 1) + 1))) =
abs (mu2 (y + 1)) / (abs x + 1)";
proof -;
have "abs ((abs x + 1) / real (y + 1) - 1) =
(abs x + 1) / real (y + (1::nat)) - 1" (is "?one = ?two");
apply (rule abs_nonneg);
apply simp;
apply (rule div_ge_1);
apply force;
apply (subgoal_tac "real(Suc y) = real y + 1");
apply (erule ssubst);
apply simp;
apply (subgoal_tac "real(natfloor(abs x)) <= abs x");
apply (rule order_trans);
prefer 2;
apply assumption;
apply (insert prems, arith);
apply (rule real_natfloor_le);
apply auto;
done;
then have "?one + 1 = (abs x + 1) / real (y + 1)" (is "?two = ?three");
by simp;
then have "1 / ?two = 1 / ?three";
by simp;
also have "... = real(y + 1) / (abs x + 1)" (is "... = ?four");
by simp;
finally have "1 / ?two = ?four";.;
then have "mu2 (y + 1) / real (y + 1) * (1 / ?two) =
mu2 (y + 1) / real (y + 1) * ?four";
by simp;
also have "...= mu2(y + 1) / (abs x + 1)";
by simp;
finally have "abs(mu2 (y + 1) / real (y + 1) * (1 / ?two)) =
abs(mu2(y + 1) / (abs x + 1))"
by force;
also have "... = abs(mu2(y+1)) / (abs(abs x + 1))";
also have "abs (abs x + 1) = abs x + 1";
apply (rule abs_nonneg);
apply arith;
done;
finally show ?thesis;.;
qed;
qed;
finally; have "?LHS =o ?RH1 +o O(%x. sumr 0 (natfloor (abs x) + 1)
(%y. abs (mu2 (y + 1)) / (abs x + 1)))";.;
also have "... <= ?RH1 +o O(%x. 1)";
apply (rule set_plus_mono);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule sumr_ge_zero_cong);
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply arith;
apply (rule allI);
apply (subgoal_tac "sumr 0 (natfloor (abs x) + 1)
(%y. abs (mu2 (y + 1)) / (abs x + 1)) <= sumr 0 (natfloor (abs x) + 1)
(%y. 1 / (abs x + 1))");
apply (erule order_trans);
apply (subst sumr_const);
apply force;
apply simp;
apply (rule real_le_mult_imp_div_pos_le);
apply arith;
apply simp;
apply (rule real_natfloor_le);
apply arith;
apply (rule sumr_le_cong);
apply (rule divide_right_mono);
apply (rule abs_mu2_leq_1);
apply arith;
done;
finally show ?thesis;.;
qed;

lemma sumr_mu_div_n_times_ln_div_nbigo:
"(%x. sumr 0 (natfloor(abs x)+1) (%n. (mu2(n+1) / real(n+1)) *
ln((abs x+1) / (real (n+1))))) =o O(%x. 1)" (is "?LHS =o ?RHS");
proof -;
note aux;
then show ?thesis;
apply (elim rev_subsetD);
apply (rule bigo_plus_absorb_lemma1);
proof -;
show "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
(sumr 0 (natfloor ((abs x + 1) / real (y + 1)))
(%n. 1 / (real n + 1)) +
gamma))) =o O(%x. 1)" (is "?LHS =o ?RHS");
proof -;
have "?LHS = (%x. sumr 0 (natfloor(abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
(sumr 0 (natfloor((abs x + 1) / real (y + 1)))
(%n. 1 / (real n + 1))))) +
(%x. sumr 0 (natfloor(abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) * gamma))"
(is "?LHS = ?term1 + ?term2");
del: One_nat_def);
also have "?term1 + ?term2 =o O(%x. 1)";
proof -;
have "?term1 = (%x.(∑y:{)0..natfloor(abs x)+1}.
∑n:{)0..(natfloor(abs x)+1) div y}.
((mu2 y) / (real (y * n)))))";
apply (rule ext);
apply (subst setsum_sumr3 [THEN sym]);
apply (rule setsum_cong2);
apply (subst setsum_sumr3);
apply (subst sumr_mult);
apply (subst natfloor_div_nat);
apply force;
apply force;
apply (subgoal_tac "natfloor (abs x + 1) = natfloor (abs x) + 1");
apply (erule ssubst);
apply (rule sumr_cong);
apply simp;
apply simp;
done;
also have "... = (%x.(∑c:{)0..natfloor (abs x) + 1}.
∑y:{y. y dvd c}. ((mu2 y) / (real (y * (c div y))))))";
apply (rule ext);
apply (rule general_inversion_nat2);
apply force;
done;
also have "... = (%x.(∑c:{)0..natfloor (abs x) + 1}.
∑y:{y. y dvd c}. ((mu2 y) / (real c))))";
apply (rule ext);
apply (rule setsum_cong2);
apply (rule setsum_cong2);
apply (subst dvd_mult_div_cancel);
apply auto;
done;
also have "... = (%x.(∑c:{)0..natfloor (abs x) + 1}.
(1 / (real c)) * (∑y:{y. y dvd c}. mu2 y)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst setsum_const_times [THEN sym]);
apply simp;
done;
also have "... = (%x.(∑c:{)0..natfloor (abs x) + 1}.
(1 / (real c)) * (if c = 1 then 1 else 0)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (unfold mu2_def);
apply (subst real_eq_of_int);
apply (subst moebius_prop_nat_general);
apply auto;
done;
also have "... = (%x. (1 / real (1::nat)))";
apply (rule ext);
apply (rule mu_aux2);
apply force;
done;
also have "... =o O(%x. 1)";
by auto;
finally have a: "?term1 =o O(%x. 1)";.;
moreover have "?term2 =o O(%x. 1)";
proof -;
have "?term2 = (%x. gamma *
sumr 0 (natfloor (abs x) + 1) (%y. mu2 (y + 1) / real (y + 1)))";
apply (rule ext);
apply (subst sumr_mult);
done;
also have "... =o O(%x. 1)";
apply (rule bigo_const_mult7);
apply (rule  bigo_compose1 [OF sumr_mu_div_n_bigo,
of "%x. natfloor(abs x)"]);
done;
finally show ?thesis;.;
qed;
ultimately have "?term1 + ?term2 =o O(%x. 1) + O(%x. 1)";
by (rule set_plus_intro);
also have "... <= O(%x. 1)"; by auto;
finally show ?thesis;.;
qed;
finally show ?thesis;.;
qed;
qed;
qed;

subsection {* Mertens theorem *}

lemma Mertens_theorem_aux:
"(%x. sumr 0 (x + 1) (%d. Lambda (d + 1) / real (d + 1))) =o
(%x. ln (real x + 1)) +o (O(%x. 1) + O(%x. psi (x + 1) / (real x + 1)))";
proof -;
have "(%x. (real (x + 1)) * (sumr 0 (x + 1) (%d.
(Lambda (d + 1)) / (real (d + 1))))) = (%x. (sumr 0 (x + 1)
(%d. (Lambda (d + 1)) * ((real (x + 1)) / (real (d + 1))))))";
apply (rule ext);
apply (subst sumr_mult);
apply (rule sumr_cong);
apply simp;
done;
also have "… =o (%x. sumr 0 (x + 1) (%d. Lambda (d + 1) *
real ((x + 1) div (d + 1)))) +o O(%x. sumr 0 (x + 1) (%d. Lambda(d + 1)))";
apply (rule bigo_sumr6);
apply (rule allI)+;
apply (rule Lambda_ge_zero);
apply (rule_tac x = 1 in exI);
apply clarsimp;
apply (subst times_divide_eq_right [THEN sym]);
apply (subst right_diff_distrib [THEN sym]);
apply (subst abs_nonneg);
apply (rule nonneg_times_nonneg);
apply (rule Lambda_ge_zero);
apply (rule nat_div_real_div1);
apply (rule real_mult_le_one_le);
apply (rule Lambda_ge_zero);
apply (rule nat_div_real_div1);
apply (rule nat_div_real_div2);
done;
also have "(%x. sumr 0 (x + 1) (%d. Lambda (d + 1))) = (%x. psi (x + 1))";
apply (rule ext);
apply (unfold psi_def);
apply (induct_tac x);
apply simp;
done;
finally; have "(%x. real (x + 1) * sumr 0 (x + 1)
(%d. Lambda (d + 1) / real (d + 1))) =o
(%x. sumr 0 (x + 1) (%d. Lambda (d + 1) * real ((x + 1) div (d + 1)))) +o
O(%x. psi (x + 1))";.;
also have "... <= ((%x. (real x + 1) * ln(real x + 1)) +o
O(%x. real x + 1)) + O(%x. psi(x + 1))";
proof (rule set_plus_mono3);
have "(%x. sumr 0 (x + 1)
(%d. Lambda (d + 1) * real ((x + 1) div (d + 1)))) =
(%x. (∑d:{)0..x+1}. Lambda d * (real((x + 1) div d))))";
apply (rule ext);
apply (subst setsum_sumr3);
apply (rule refl);
done;
also have "... = (%x. (∑d:{)0..x+1}. (∑d':{)0..((x+1) div d)}.
Lambda d)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst setsum_constant);
apply force;
done;
also have "... = (%x. (∑c:{)0..x+1}. (∑d:{d. d dvd c}.
Lambda d)))";
apply (rule ext);
apply (subst general_inversion_nat2);
apply auto;
done;
also have "... = (%x. (∑c:{)0..x+1}. ln (real c)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst ln_eq_setsum_Lambda);
apply auto;
done;
also have "... = (%x. sumr 0 (x + 1) (%n. ln(real n + 1)))";
apply (rule ext);
apply (subst setsum_sumr3);
apply (rule sumr_cong);
apply simp;
done;
also have "... =o ((%n. (real n + 1) * ln(real n + 1)) - (%n. real n))
+o O(%n. ln (real n + 1))";
by (rule identity_three);
also have "... = (%n. (real n + 1) * ln(real n + 1)) +o
(-(%n. real n) +o O(%n. ln(real n + 1)))";
also have "... <= (%n. (real n + 1) * ln(real n + 1)) +o
(-(%n. real n) +o O(%n. real n + 1))";
apply (rule set_plus_mono);
apply (rule set_plus_mono);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule ln_ge_zero);
apply force;
apply (rule allI);
apply (rule order_trans);
apply auto;
done;
also; have "... <= (%n. (real n + 1) * ln (real n + 1)) +o
O(%n. real n + 1)";
apply (rule set_plus_mono);
apply (rule bigo_plus_absorb_lemma1);
apply (rule bigo_minus);
apply (rule bigo_bounded);
apply auto;
done;
finally; show "(%x. sumr 0 (x + 1)
(%d. Lambda (d + 1) * real ((x + 1) div (d + 1)))) =o
(%n. (real n + 1) * ln (real n + 1)) +o O(%n. real n + 1)";.;
qed;
finally; have "(%x. real (x + 1) *
sumr 0 (x + 1) (%d. Lambda (d + 1) / real (d + 1))) =o
(%x. (real x + 1) * ln (real x + 1)) +o (O(%x. real x + 1) +
O(%x. psi (x + 1)))" (is "?LHS =o ?RHS");
then have "(%x. 1 / (real x + 1)) * ?LHS =o (%x. 1 / (real x + 1)) *o
?RHS";
by (rule set_times_intro2);
also have "(%x. 1 / (real x + 1)) * ?LHS =
(%x. sumr 0 (x + 1) (%d. Lambda (d + 1) / real (d + 1)))";
apply (rule ext);
apply (subgoal_tac "real x + 1 = real (Suc x)");
apply (erule ssubst);
apply simp;
apply simp;
done;
also have "(%x. 1 / (real x + 1)) *o ?RHS =
(%x. ln (real x + 1)) +o ((%x. 1 / (real x + 1)) *o O(%x. real x + 1)
+ (%x. 1 / (real x + 1)) *o O(%x. psi (x + 1)))";
also have "... <= (%x. ln (real x + 1)) +o
(O(%x. 1) + O(%x. psi (x + 1) / (real x + 1)))";
apply (rule set_plus_mono);
apply (rule set_plus_mono2);
apply (rule order_trans);
apply (rule bigo_mult2);
apply (rule order_trans);
apply (rule bigo_mult2);
done;
finally; show ?thesis;.;
qed;

lemma Mertens_theorem:
"(%x. sumr 0 (x + 1) (%d. Lambda (d + 1) / real (d + 1))) =o
(%x. ln (real x + 1)) +o O(%x. 1)";
proof -;
have "(%x. psi(x + 1)) =o O(%x. real (x + 1))";
by (rule bigo_compose1 [OF psi_bigo]);
also have "(%x. real (x + (1::nat))) = (%x. real x + 1)";
by (rule ext, simp);
finally have "(%x. psi(x + 1)) =o O(%x. real x + 1)";.;
then have "(%x. 1 / (real x + 1)) * (%x. psi(x+1)) =o
(%x. 1 / (real x + 1)) *o O(%x. real x + 1)";
by (rule set_times_intro2);
also have "(%x. 1 / (real x + 1)) * (%x. psi(x+1)) =
(%x. psi(x+1) / (real x + 1))"; by (simp add: func_times);
also have "(%x. 1 / (real x + 1)) *o O(%x. real x + 1) <=
O((%x. 1 / (real x + 1)) * (%x. real x + 1))";
by (rule bigo_mult2);
also have "((%x. 1 / (real (x::nat) + 1)) * (%x. real x + 1)) = (%x. 1)";
finally have a: "O(%x. psi(x + 1) / (real x + 1)) <= O(%x. 1)";
by (rule bigo_elt_subset);

note Mertens_theorem_aux;
also have "(%x. ln (real x + 1)) +o
(O(%x. 1) + O(%x. psi (x + 1) / (real x + 1))) <=
(%x. ln (real x + 1)) +o O(%x. 1)";
apply (rule set_plus_mono);
apply (rule bigo_plus_subset4);
apply simp;
apply (rule a);
done;
finally show ?thesis;.;
qed;

lemma Mertens_theorem_real:
"(%x. sumr 0 (natfloor (abs x) + 1) (%d. Lambda (d + 1) / real (d + 1))) =o
(%x. ln (abs x + 1)) +o O(%x. 1)" (is "?LHS =o ?RHS");
proof -;
have "?LHS =o (%x. ln(real(natfloor(abs x)) + 1)) +o O(%x. 1)";
by (rule bigo_compose2 [OF Mertens_theorem]);
also have "... <= ((%x. ln(abs x + 1)) +o O(%x. 1 / (abs x + 1))) +
O(%x. 1)";
apply (rule set_plus_mono3);
apply (rule ln_real_approx_ln_nat);
done;
also have "... <= (%x. ln(abs x + 1)) +o O(%x. 1)";
apply (rule set_plus_mono);
apply (rule bigo_plus_subset4);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply auto;
apply arith;
apply (rule real_le_mult_imp_div_pos_le);
apply arith;
apply auto;
done;
finally show ?thesis;.;
qed;

lemma Mertens_theorem_real2: "(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m) =o (%x. ln (abs x + 1)) +o O(%x. 1)"
(is "?left =o ?right");
apply (subgoal_tac "?left =
(%x. sumr 0 (natfloor (abs x) + 1) (%d. Lambda (d + 1) / real (d + 1)))");
apply (erule ssubst);
apply (rule Mertens_theorem_real);
apply (rule ext);
apply (subst setsum_sumr4);
apply (rule refl);
done;

subsection {* Sum of mu n over n times (ln n over n) squared *}

lemma aux2a: "(y::nat) <= natfloor (abs x) ==>
abs((abs(x) + 1) / real (y + 1) - 1) + 1 =
((abs(x) + 1) / real (y + 1))";
apply (subst abs_nonneg);back;back;
apply (simp del: One_nat_def);
apply (rule div_ge_1);
apply force;
apply simp;
apply (subgoal_tac "real y <= real (natfloor (abs x))");
apply (erule order_trans);
apply (rule real_natfloor_le);
apply force;
apply simp;
apply simp;
done;

lemma sumr_ln_div_bigo:
"(%n. sumr 0 (n+1) (%i. ln((real n + 1) / (real i + 1)))) =o
(%n. real n) +o O(%n. ln (real n + 1))";
proof -;
have "(%n. sumr 0 (n+1) (%i. ln((real n + 1) / (real i + 1)))) =
(%n. sumr 0 (n+1) (%i. ln (real n + 1))) -
(%n. sumr 0 (n+1) (%i. ln (real i + 1)))";
apply (subst func_diff);
apply (rule ext);
apply (subst sumr_diff);
apply (rule sumr_cong);
apply (subst ln_div);
apply auto;
done;
also have "(%n. sumr 0 (n+1) (%i. ln (real n + 1))) = (%n. (real n + 1) *
ln(real n + 1))";
apply (rule ext);
done;
finally have "(%n. sumr 0 (n+1) (%i. ln((real n + 1) / (real i + 1)))) =
(%n. (real n + 1) * ln(real n + 1)) +
-(%n. sumr 0 (n+1) (%i. ln (real i + 1)))";
also have "... =o (%n. (real n + 1) * ln(real n + 1)) +o
(-((%n. (real n + 1) * ln(real n + 1)) - (%n. real n)) +o
O(%n. ln (real n + 1)))";
apply (rule set_plus_intro2);
apply (rule bigo_minus2);
apply (rule identity_three);
done;
also; have "... = real +o O(%n. ln(real n + 1))";
finally show ?thesis;.;
qed;

lemma sumr_ln_div_bigo_real:
"(%x. sumr 0 (natfloor(abs x)+1) (%i. ln((abs x + 1) / (real i + 1)))) =o
O(%x. abs x + 1)";
proof -;
have "(%x. sumr 0 (natfloor(abs x)+1)
(%i. ln((abs x + 1) / (real i + 1)))) =
(%x. sumr 0 (natfloor(abs x)+1) (%i. ln (abs x + 1))) -
(%x. sumr 0 (natfloor(abs x)+1) (%i. ln (real i + 1)))";
apply (subst func_diff);
apply (rule ext);
apply (subst sumr_diff);
apply (rule sumr_cong);
apply (subst ln_div);
apply auto;
apply arith;
done;
also have "(%x. sumr 0 (natfloor(abs x)+1) (%i. ln (abs x + 1))) =
(%x. (real (natfloor(abs x) + 1) * ln(abs x + 1)))";
apply (rule ext);
apply (simp only: sumr_const ring_distrib);
done;
finally have "(%x. sumr 0 (natfloor(abs x)+1)
(%i. ln((abs x + 1) / (real i + 1)))) =
(%x. (real (natfloor(abs x) + 1) * ln(abs x + 1))) +
-(%x. sumr 0 (natfloor(abs x)+1) (%i. ln (real i + 1)))";
also; have "... =o (%x. real (natfloor (abs x) + 1) * ln (abs x + 1)) +o
(-(%x. (real (natfloor (abs x) + 1)) *
ln (abs x + 1)) +o O(%x. (abs x) + 1))";
apply (rule set_plus_intro2);
apply (rule bigo_minus2);
apply (rule identity_three_cor_real);
done;
also have "... = O(%x. (abs x) + 1)";
finally show ?thesis;.;
qed;

lemma aux2: "(%x. sumr 0 (natfloor(abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
(ln ((abs x + 1) / (real (y + 1))))^2))
=o (%x. sumr 0 (natfloor(abs x) + 1)
(%y. mu2 (y + 1) / (real (y + 1)) *
ln ((abs x + 1) / (real (y + 1))) *
(sumr 0 (natfloor((abs x + 1) / real (y + 1)))
(%n. 1 / (real n + 1)) +
gamma))) +o O(%x. 1)"
(is "?LHS =o ?RH1 +o O(%x. 1)");
proof -;
note bigo_sumr8 [OF better_ln_theorem2_real, of
"%x. natfloor(abs x) + 1"
"%x y. mu2(y+1) / real(y+1) * ln ((abs x + 1) / (real (y + 1)))"
"%x y. ((abs x) + 1) / (real (y+1)) - 1"];
also have "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) * ln ((abs x + 1) / real (y + 1)) *
ln (abs ((abs x + 1) / real (y + 1) - 1) + 1))) = ?LHS";
apply (rule ext);
apply (rule sumr_cong);
apply (subst aux2a);
apply force;
apply (subst realpow_two2 [THEN sym]);
apply simp;
done;
also have "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) * ln ((abs x + 1) / real (y + 1)) *
((%x. sumr 0 (natfloor (abs x) + 1) (%n. 1 / (real n + 1))) +
(%x. gamma))
((abs x + 1) / real (y + 1) - 1))) = ?RH1";
apply (rule ext);
apply (rule sumr_cong);
apply (simp only: func_plus);
apply force;
apply (subst real_nat_one);
apply (subst aux2a);
apply force;
apply (rule refl);
done;
also have "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. abs (mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / real (y + 1)) *
(1 / (abs ((abs x + 1) / real (y + 1) - 1) + 1))))) =
(%x. sumr 0 (natfloor (abs x) + 1)
(%y. abs(mu2 (y + 1)) / (abs x + 1) *
ln ((abs x + 1) / real (y + 1))))";
apply (rule ext);
apply (rule sumr_cong);
apply (subst aux2a);
apply force;
apply (simp add: abs_divide [THEN sym] abs_mult [THEN sym]);
apply (subgoal_tac "abs(ln((abs x + 1) / real (Suc y))) =
ln((abs x + 1) / real (Suc y))");
apply (subgoal_tac "abs(abs x + 1) = abs x + 1");
apply simp;
apply (rule abs_nonneg);
apply arith;
apply (rule abs_nonneg);
apply (rule ln_ge_zero);
apply (rule div_ge_1);
apply force;
apply (subgoal_tac "real(Suc y) = real y + 1");
apply (erule ssubst);
apply simp;
apply (subgoal_tac "real(natfloor(abs x)) <= abs x");
apply (rule order_trans);
prefer 2;
apply assumption;
apply arith;
apply (rule real_natfloor_le);
apply auto;
done;
also have "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. abs (mu2 (y + 1)) / (abs x + 1) *
ln ((abs x + 1) / real (y + 1)))) =
(%x. 1 / (abs x + 1)) * (%x. sumr 0 (natfloor (abs x) + 1)
(%y. abs (mu2 (y + 1)) *
ln ((abs x + 1) / real (y + 1))))";
by (simp add: func_times sumr_mult ring_eq_simps);
also have "O(...) =
(%x. 1 / (abs x + 1)) *o O(%x. sumr 0 (natfloor (abs x) + 1)
(%y. abs (mu2 (y + 1)) * ln ((abs x + 1) / real (y + 1))))";
apply (subst bigo_mult6 [THEN sym]);
apply (rule allI);
apply clarsimp;
apply arith;
apply (rule refl);
done;
finally have "?LHS =o ?RH1 +o ...";.;
also have "... <= ?RH1 +o (%x. 1 / (abs x + 1)) *o
O(%x. sumr 0 (natfloor (abs x) + 1)
(%y. ln ((abs x + 1) / real (y + 1))))";
apply (rule set_plus_mono);
apply (rule set_times_mono);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule sumr_ge_zero_cong);
apply (rule nonneg_times_nonneg);
apply force;
apply (rule ln_ge_zero);
apply (rule div_ge_1);
apply force;
apply (subgoal_tac "real (y + 1) = real y + 1");
apply (erule ssubst);
apply simp;
apply (rule nat_le_natfloor);
apply force;
apply force;
apply force;
apply (rule allI);
apply (rule sumr_le_cong);
apply (rule real_le_one_mult_le);
apply (rule ln_ge_zero);
apply (rule div_ge_1);
apply force;
apply (subgoal_tac "real (y + 1) = real y + 1");
apply (erule ssubst);
apply simp;
apply (rule nat_le_natfloor);
apply force;
apply force;
apply force;
apply force;
apply (rule abs_mu2_leq_1);
done;
also; have "... <= ?RH1 +o (%x. 1 / (abs x + 1)) *o O(%x. (abs x + 1))";
apply (rule set_plus_mono);
apply (rule set_times_mono);
apply (rule bigo_elt_subset);
apply (subgoal_tac "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. ln ((abs x + 1) / real (y + 1)))) =
(%x. sumr 0 (natfloor (abs x) + 1)
(%y. ln ((abs x + 1) / (real y + 1))))");
apply (erule ssubst);
apply (rule sumr_ln_div_bigo_real);
apply (rule ext);
apply (rule sumr_cong);
apply (subgoal_tac "real (y + 1) = real y + 1");
apply (erule subst);
apply simp;
apply simp;
done;
also have "(%x. 1 / (abs x + 1)) *o O(%x. (abs x + 1)) =
O(%x. 1::real)";
apply (subst bigo_mult6 [THEN sym]);
apply (rule allI);
apply simp;
apply arith;
apply (subgoal_tac "(%x. (abs x + 1) / (abs x + 1)) = (%x. 1)");
apply (erule ssubst);
apply (rule refl);
apply (rule ext);
apply simp;
apply arith;
done;
finally show ?thesis;.;
qed;

lemma Lambda_sum_mu_ln: "1 <= x ==>
Lambda x = -(∑d:{d. d dvd x}. mu2(d) * ln(real d))";
proof -;
assume "1 <= (x::nat)";
then have "Lambda x = (∑d:{d. d dvd x}.
∑d':{d'. d' dvd (x div d)}.
mu2(d) * Lambda((x div d) div d'))";
apply (unfold mu2_def);
apply (subst real_eq_of_int);
apply (rule mu_inversion_nat1);
apply force;
done;
also have "... = (∑d:{d. d dvd x}. mu2(d) *
(∑d': {d'. d' dvd (x div d)}.
Lambda((x div d) div d')))";
apply (rule setsum_cong2);
apply (rule setsum_const_times);
done;
also have "... = (∑d:{d. d dvd x}. mu2(d) *
(∑d': {d'. d' dvd (x div d)}.
Lambda d'))";
apply (rule setsum_cong2);
apply (subst general_inversion_nat1 [THEN sym]);
apply clarsimp;
apply (rule nat_pos_div_dvd_gr_0);
apply (insert prems, arith);
apply assumption;
apply (rule refl);
done;
also have "... = (∑d:{d. d dvd x}. mu2(d) * ln(real (x div d)))";
apply (rule setsum_cong2);
apply (subst ln_eq_setsum_Lambda);
apply clarsimp;
apply (rule nat_pos_div_dvd_gr_0);
apply (insert prems, arith);
apply assumption;
apply simp;
done;
also have "... = (∑d:{d. d dvd x}. mu2(d) * ln(real x / real d))";
apply (rule setsum_cong2);
apply (subst nat_dvd_real_div);
apply auto;
apply (rule dvd_pos_pos);
prefer 2;
apply assumption;
apply (insert prems, arith);
done;
also have "... = (∑d:{d. d dvd x}. mu2 d * ln (real x))
- (∑d:{d. d dvd x}. mu2 d * ln (real d))";
apply (subst setsum_subtractf [THEN sym]);
apply (rule finite_nat_dvd_set);
apply (insert prems, arith);
apply (rule setsum_cong2);
apply (subst ln_div);
apply force;
apply clarsimp;
apply (rule dvd_pos_pos);
prefer 2;
apply assumption;
apply (insert prems, arith);
done;
also have "(∑d:{d. d dvd x}. mu2 d * ln (real x)) =
ln (real x) * (∑d:{d. d dvd x}. mu2 d)";
apply (subst setsum_const_times [THEN sym]);
done;
also have "... = ln(real x) * (if x = 1 then 1 else 0)";
apply (unfold mu2_def);
apply (subst real_eq_of_int);
apply (subst moebius_prop_nat_general);
apply (insert prems, arith);
apply (rule refl);
done;
also; have "... = 0";
apply (case_tac "x = 1");
apply simp;
apply simp;
done;
finally show ?thesis;
by simp;
qed;

lemma sumr_mu_div_n_times_ln_squared_div_nbigo:
"(%x. sumr 0 (natfloor(abs x)+1) (%n. (mu2(n+1) / real(n+1)) *
(ln((abs x+1) / (real (n+1))))^2)) =o
(%x. 2 * ln (abs x + 1)) +o O(%x. 1)"
(is "?LHS =o ?RHS");
proof -;
note aux2;
also have "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / real (y + 1)) *
(sumr 0 (natfloor ((abs x + 1) / real (y + 1)))
(%n. 1 / (real n + 1)) +
gamma))) =
(%x. sumr 0 (natfloor (abs x) + 1)
((%y. mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / real (y + 1)) *
(sumr 0 (natfloor ((abs x + 1) / real (y + 1)))
(%n. 1 / (real n + 1)))) +
(%y. mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / real (y + 1)) * gamma)))";
apply (rule ext);
apply (rule sumr_cong);
apply (subst func_plus);
done;
also have "... =  (%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / real (y + 1)) *
(sumr 0 (natfloor ((abs x + 1) / real (y + 1)))
(%n. 1 / (real n + 1))))) +
(%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / real (y + 1)) * gamma))";
apply (subst func_plus);
apply (rule ext);
apply (rule sumr_cong);
done;
finally; have "(%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / real (y + 1)) ^ 2)) =o
((%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / real (y + 1)) *
sumr 0 (natfloor ((abs x + 1) / real (y + 1)))
(%n. 1 / (real n + 1)))) +
(%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / real (y + 1)) *
gamma))) +o
O(%x. 1)" (is "?LHS =o (?term1 + ?term2) +o O(%x. 1)");.;
also have "... = ?term1 +o (?term2 +o O(%x. 1))";
also have "... <= ?term1 +o O(%x. 1)";
apply (rule set_plus_mono);
apply (subst bigo_plus_idemp [THEN sym]);back;
apply (rule set_plus_mono3);
apply (subgoal_tac "?term2 = (%x. gamma) *
(%x. sumr 0 (natfloor (abs x) + 1)
(%y. mu2 (y + 1) / real (y + 1) *
ln ((abs x + 1) / real (y + 1))))");
apply (erule ssubst);
apply (rule rev_subsetD);
prefer 2;
apply (subgoal_tac "(%x. gamma) *o O(%x. 1) <= O(%x. 1)");
apply assumption;
apply (rule bigo_const_mult6);
apply (rule set_times_intro2);
apply (rule sumr_mu_div_n_times_ln_div_nbigo);
apply (simp only: func_times);
apply (rule ext);
apply (subst sumr_mult);
apply (rule sumr_cong);
apply simp;
done;
also have "... <= ((%x. 2 * ln (abs x + 1)) +o O(%x. 1)) + O(%x.1)";
proof (rule set_plus_mono3);
have "?term1 = (%x. (∑ y:{)0..natfloor (abs x)+1}.
(mu2 y / real y *
ln ((abs x + 1) / real y) *
sumr 0 (natfloor ((abs x + 1) / real y))
(%n. 1 / (real n + 1)))))";
apply (rule ext);
apply (rule setsum_sumr3 [THEN sym]);
done;
also have "... = (%x. (∑ y:{)0..natfloor (abs x)+1}.
∑n:{)0..natfloor ((abs x + 1) / real y)}.
(mu2 y / real y * ln ((abs x + 1) / real y) *
1 / (real n))))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst sumr_mult);
apply (subst setsum_sumr3);
apply (rule sumr_cong);
apply simp;
done;
also have "... = (%x. (∑ y:{)0..natfloor (abs x)+1}.
∑n:{)0..(natfloor (abs x)+1) div y}.
(mu2 y / real (y * n) * ln ((abs x + 1) / real y))))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst natfloor_div_nat);
apply force;
apply force;
apply force;
apply simp;
done;
also have "... = (%x. (∑c:{)0..natfloor (abs x) + 1}.
∑y:{y. y dvd c}. (mu2 y / real (y * (c div y)) *
ln ((abs x + 1) / real y))))";
apply (rule ext);
apply (rule general_inversion_nat2);
apply force;
done;
also have "... = (%x. (∑c:{)0..natfloor (abs x) + 1}.
∑y:{y. y dvd c}. (mu2 y / real c) * ln (abs x + 1) -
(mu2 y / real c) * ln (real y)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (rule setsum_cong2);
apply (subst dvd_mult_div_cancel);
apply force;
apply (subst ln_div);
apply arith;
apply clarsimp;
apply (rule dvd_pos_pos);
apply assumption+;
done;
also have "... = (%x. (∑c:{)0..natfloor (abs x) + 1}.
∑y:{y. y dvd c}. (mu2 y / real c) * ln (abs x + 1))) -
(%x. (∑c:{)0..natfloor (abs x) + 1}.
∑y:{y. y dvd c}. (mu2 y / real c) * ln (real y)))"
(is "?temp = ?term2 - ?term3");
apply (subst func_diff);
apply (rule ext);
apply (subst setsum_subtractf [THEN sym]);
apply force;
apply (rule setsum_cong2);
apply (subst setsum_subtractf [THEN sym]);
apply (rule finite_nat_dvd_set);
apply force;
apply (rule refl);
done;
also have "... = ?term2 + -(?term3)";
by (simp only: diff_minus);
also have "?term2 = (%x. (∑c:{)0..natfloor (abs x) + 1}.
(ln (abs x + 1) / real c) * (∑y:{y. y dvd c}. mu2 y)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also have "... = (%x. (∑c:{)0..natfloor (abs x) + 1}.
(ln (abs x + 1) / real c) * (if c = 1 then 1 else 0)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (unfold mu2_def);
apply (subst real_eq_of_int);
apply (subst moebius_prop_nat_general);
apply force;
apply (rule refl);
done;
also have "... = (%x. ln (abs x + 1))";
apply (rule ext);
apply (subst mu_aux2);
apply force;
apply simp;
done;
also; have "?term3 = (%x. ∑c:{)0..natfloor (abs x) + 1}.
1 / real c * (∑y:{y. y dvd c}. mu2 y * ln (real y)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst setsum_const_times [THEN sym]);
apply simp;
done;
also have "... = - (%x. ∑c:{)0..natfloor (abs x) + 1}.
Lambda c / real c)";
apply (subst func_minus);
apply (rule ext);
apply (subst setsum_negf [THEN sym]);
apply force;
apply (rule setsum_cong2);
apply (subst Lambda_sum_mu_ln);
apply force;
apply simp;
done;
also have "- (...) = (%x. ∑c:{)0..natfloor (abs x) + 1}.
Lambda c / real c)";
by simp;
also have "... = (%x. sumr 0 (natfloor (abs x) + 1)
(%d. Lambda (d + 1) / real (d + 1)))" (is "?temp = ?term4");
apply (rule ext);
apply (rule setsum_sumr3);
done;
also have "(%x. ln (abs x + 1)) + ?term4 =o
(%x. ln (abs x + 1)) +o ((%x. ln(abs x + 1)) +o O(%x. 1))";
apply (rule set_plus_intro2);
apply (rule Mertens_theorem_real);
done;
also have "... = (%x. 2 * ln (abs x + 1)) +o O(%x. 1)";
apply (simp only: set_plus_rearranges);
done;
finally show "?term1 =o ...";.;
qed;
also have "... = (%x. 2 * ln (abs x + 1)) +o (O(%x. 1) + O(%x.1))";
by (simp only: set_plus_rearranges);
also have "... = (%x. 2 * ln (abs x + 1)) +o O(%x. 1)";
by simp;
finally show ?thesis;.;
qed;

end;
```

### Variants of inversion laws

lemma mu_inversion_nat1_real:

```  [| ∀n. 0 < n --> f n = (∑d | d dvd n. g (n div d)); 0 < n |]
==> g n = (∑d | d dvd n. mu2 d * f (n div d))```

lemma mu_inversion_nat2_real:

```  [| ∀n. 0 < n --> g n = (∑d | d dvd n. mu2 d * f (n div d)); 0 < n |]
==> f n = (∑d | d dvd n. g (n div d))```

lemma mu_inversion_nat3_real:

`  0 < n ==> g n = (∑d∈{)0..n}. ∑d'∈{)0..n div d}. mu2 d * g (n div d div d'))`

lemma abs_mu2_leq_1:

`  ¦mu2 x¦ ≤ 1`

lemma mu_inversion_nat1a':

```  [| ∀n. 0 < n --> f n = (∑d | d dvd n. g d); 0 < n |]
==> g n = (∑d | d dvd n. of_int (mu (int d)) * f (n div d))```

lemma mu_inversion_nat1a'_real:

```  [| ∀n. 0 < n --> f n = (∑d | d dvd n. g d); 0 < n |]
==> g n = (∑d | d dvd n. mu2 d * f (n div d))```

lemma aux3:

`  {)0..n} = {1..n}`

lemma general_inversion_nat2_modified:

```  0 < n
==> (∑d = 1..n. setsum (f d) {1..n div d}) =
(∑c = 1..n. ∑d | d dvd c. f d (c div d))```

lemma general_inversion_nat2_cor1_modified:

```  0 < n
==> (∑d = 1..n. setsum (f d) {1..n div d}) =
(∑d' = 1..n. ∑d = 1..n div d'. f d d')```

### Sum of mu div n

lemma sumr_mu_div_n_bigo:

`  (%x. sumr 0 (x + 1) (%n. mu2 (n + 1) / real (n + 1))) ∈ O(%x. 1)`

### Sum of mu div n times ln n over n

lemma aux_nat_diff:

`  a ≤ x ==> x - a + a = x`

lemma aux:

```  (%x. sumr 0 (natfloor ¦x¦ + 1)
(%y. mu2 (y + 1) / real (y + 1) * ln ((¦x¦ + 1) / real (y + 1))))
∈ (%x. sumr 0 (natfloor ¦x¦ + 1)
(%y. mu2 (y + 1) / real (y + 1) *
(sumr 0 (natfloor ((¦x¦ + 1) / real (y + 1)))
(%n. 1 / (real n + 1)) +
gamma))) +
O(%x. 1)```

lemma sumr_mu_div_n_times_ln_div_nbigo:

```  (%x. sumr 0 (natfloor ¦x¦ + 1)
(%n. mu2 (n + 1) / real (n + 1) * ln ((¦x¦ + 1) / real (n + 1))))
∈ O(%x. 1)```

### Mertens theorem

lemma Mertens_theorem_aux:

```  (%x. sumr 0 (x + 1) (%d. Lambda (d + 1) / real (d + 1)))
∈ (%x. ln (real x + 1)) + (O(%x. 1) + O(%x. psi (x + 1) / (real x + 1)))```

lemma Mertens_theorem:

```  (%x. sumr 0 (x + 1) (%d. Lambda (d + 1) / real (d + 1)))
∈ (%x. ln (real x + 1)) + O(%x. 1)```

lemma Mertens_theorem_real:

```  (%x. sumr 0 (natfloor ¦x¦ + 1) (%d. Lambda (d + 1) / real (d + 1)))
∈ (%x. ln (¦x¦ + 1)) + O(%x. 1)```

lemma Mertens_theorem_real2:

```  (%x. ∑m = 1..natfloor ¦x¦ + 1. Lambda m / real m)
∈ (%x. ln (¦x¦ + 1)) + O(%x. 1)```

### Sum of mu n over n times (ln n over n) squared

lemma aux2a:

```  y ≤ natfloor ¦x¦
==> ¦(¦x¦ + 1) / real (y + 1) - 1¦ + 1 = (¦x¦ + 1) / real (y + 1)```

lemma sumr_ln_div_bigo:

```  (%n. sumr 0 (n + 1) (%i. ln ((real n + 1) / (real i + 1))))
∈ real + O(%n. ln (real n + 1))```

lemma sumr_ln_div_bigo_real:

```  (%x. sumr 0 (natfloor ¦x¦ + 1) (%i. ln ((¦x¦ + 1) / (real i + 1))))
∈ O(%x. ¦x¦ + 1)```

lemma aux2:

```  (%x. sumr 0 (natfloor ¦x¦ + 1)
(%y. mu2 (y + 1) / real (y + 1) * (ln ((¦x¦ + 1) / real (y + 1)))²))
∈ (%x. sumr 0 (natfloor ¦x¦ + 1)
(%y. mu2 (y + 1) / real (y + 1) * ln ((¦x¦ + 1) / real (y + 1)) *
(sumr 0 (natfloor ((¦x¦ + 1) / real (y + 1)))
(%n. 1 / (real n + 1)) +
gamma))) +
O(%x. 1)```

lemma Lambda_sum_mu_ln:

`  1 ≤ x ==> Lambda x = - (∑d | d dvd x. mu2 d * ln (real d))`

lemma sumr_mu_div_n_times_ln_squared_div_nbigo:

```  (%x. sumr 0 (natfloor ¦x¦ + 1)
(%n. mu2 (n + 1) / real (n + 1) * (ln ((¦x¦ + 1) / real (n + 1)))²))
∈ (%x. 2 * ln (¦x¦ + 1)) + O(%x. 1)```