Theory MuSum

(*  Title:      MuSum.thy
    Author:     Jeremy Avigad
*)

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))";
    by (rule bigo_add_commute_imp);
  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;
    by (simp add: func_times);
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))";
        by (simp add: abs_divide);
      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 (subst natfloor_add [THEN sym]);
    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");
          by (simp add: sumr_add func_plus ring_eq_simps
            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 add: ring_eq_simps);
            apply (subst natfloor_add [THEN sym]);
            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);
              apply (simp add: ring_eq_simps);
              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 add: Lambda_zero);
    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;
      apply (simp add: real_eq_of_nat mult_ac);
      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)))";
      by (simp add: diff_minus set_plus_rearranges add_ac);
    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 (subst add_commute);
      apply (rule order_trans);
      apply (rule ln_add_one_self_le_self);
      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");
    by (simp add: set_plus_rearranges);
  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 (simp add: func_times);
    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)))";
    by (simp add: set_times_plus_distribs func_times);
  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 (simp add: func_times);
    apply (rule order_trans);
    apply (rule bigo_mult2);
    apply (simp add: func_times);
    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)";
    by (simp add: func_times);
  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 bigo_add_commute_imp);
    apply (rule ln_real_approx_ln_nat);
    done;
  also have "... <= (%x. ln(abs x + 1)) +o O(%x. 1)";
    apply (simp add: set_plus_rearranges add_ac);
    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);
    apply (simp add: sumr_const ring_distrib);
    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)))"; 
    by (simp add: diff_minus);
  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))";
    by (simp add: set_plus_rearranges add_ac); 
  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)))"; 
    by (simp add: diff_minus);
  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)";
    by (simp add: set_plus_rearranges add_ac);
  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 (subst natfloor_add [THEN sym]);
    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 (simp add: abs_mult abs_divide);
    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 (simp add: func_times);
    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);
    apply (simp add: ring_eq_simps);
    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]);
    apply (simp add: mult_ac);
    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);
     apply (simp add: ring_distrib);
     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 (subst sumr_add);
    apply (rule sumr_cong);
    apply (simp add: func_plus);
    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))";
    by (simp only: set_plus_rearranges add_ac);
  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 (subst natfloor_add [THEN sym]);
       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+;
       apply (simp add: right_diff_distrib);
       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);
       apply (simp add: func_plus);
       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;