# Theory Prime_Harmonic_Misc

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