Theory Prime_Harmonic_Misc

  File:   Prime_Harmonic_Misc.thy
  Author: Manuel Eberl <>


section ‹Auxiliary lemmas›
theory Prime_Harmonic_Misc

lemma sum_list_nonneg: "xset xs. x  0  sum_list xs  (0 :: 'a :: ordered_ab_group_add)"
  by (induction xs) auto

lemma sum_telescope':
  assumes "m  n"
  shows   "(k = Suc m..n. f k - f (Suc k)) = f (Suc m) - (f (Suc n) :: 'a :: ab_group_add)"
  by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)

lemma dvd_prodI:
  assumes "finite A" "x  A"
  shows   "f x dvd prod f A"
proof -
  from assms have "prod f A = f x * prod f (A - {x})" 
    by (intro prod.remove) simp_all
  thus ?thesis by simp

lemma dvd_prodD: "finite A  prod f A dvd x  a  A  f a dvd x"
  by (erule dvd_trans[OF dvd_prodI])

lemma multiplicity_power_nat: 
  "prime p  n > 0  multiplicity p (n ^ k :: nat) = k * multiplicity p n"
  by (induction k) (simp_all add: prime_elem_multiplicity_mult_distrib)

lemma multiplicity_prod_prime_powers_nat':
  "finite S  pS. prime p  prime p  
     multiplicity p (S :: nat) = (if p  S then 1 else 0)"
  using multiplicity_prod_prime_powers[of S p "λ_. 1"] by simp

lemma prod_prime_subset:
  assumes "finite A" "finite B"
  assumes "x. x  A  prime (x::nat)"
  assumes "x. x  B  prime x"
  assumes "A dvd B"
  shows   "A  B"
  fix x assume x: "x  A"
  from assms(4)[of 0] have "0  B" by auto
  with assms have nonzero: "zB. z  0" by (intro ballI notI) auto

  from x assms have "1 = multiplicity x (A)"
    by (subst multiplicity_prod_prime_powers_nat') simp_all
  also from assms nonzero have "  multiplicity x (B)" by (intro dvd_imp_multiplicity_le) auto
  finally have "multiplicity x (B) > 0" by simp
  moreover from assms x have "prime x" by simp
  ultimately show "x  B" using assms(2,4)
    by (subst (asm) multiplicity_prod_prime_powers_nat') (simp_all split: if_split_asm)

lemma prod_prime_eq:
  assumes "finite A" "finite B" "x. x  A  prime (x::nat)" "x. x  B  prime x" "A = B"
  shows   "A = B"
  using assms by (intro equalityI prod_prime_subset) simp_all

lemma ln_ln_nonneg:
  assumes x: "x  (3 :: real)"
  shows   "ln (ln x)  0"
proof -
  have "exp 1  (3::real)" by (rule  exp_le)
  hence "ln (exp 1)  ln (3 :: real)" by (subst ln_le_cancel_iff) simp_all
  also from x have "  ln x" by (subst ln_le_cancel_iff) simp_all
  finally have "ln 1  ln (ln x)" using x by (subst ln_le_cancel_iff) simp_all
  thus ?thesis by simp