Theory Prime_Harmonic_Misc

(*
  File:   Prime_Harmonic_Misc.thy
  Author: Manuel Eberl <manuel@pruvisto.org>

*)

section ‹Auxiliary lemmas›
theory Prime_Harmonic_Misc
imports
  Complex_Main
  "HOL-Number_Theory.Number_Theory" 
begin

lemma sum_list_nonneg: "∀x∈set 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
qed

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 ⟹ ∀p∈S. 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"
proof
  fix x assume x: "x ∈ A"
  from assms(4)[of 0] have "0 ∉ B" by auto
  with assms have nonzero: "∀z∈B. 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)
qed

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
qed

end