# Theory Prime_Harmonic_Misc

(* File: Prime_Harmonic_Misc.thy Author: Manuel Eberl <eberlm@in.tum.de> *) 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

# Theory Squarefree_Nat

(* File: Squarefree_Nat.thy Author: Manuel Eberl <eberlm@in.tum.de> The unique decomposition of a natural number into a squarefree part and a square. *) section ‹Squarefree decomposition of natural numbers› theory Squarefree_Nat imports Main "HOL-Number_Theory.Number_Theory" Prime_Harmonic_Misc begin text ‹ The squarefree part of a natural number is the set of all prime factors that appear with odd multiplicity. The square part, correspondingly, is what remains after dividing by the squarefree part. › definition squarefree_part :: "nat ⇒ nat set" where "squarefree_part n = {p∈prime_factors n. odd (multiplicity p n)}" definition square_part :: "nat ⇒ nat" where "square_part n = (if n = 0 then 0 else (∏p∈prime_factors n. p ^ (multiplicity p n div 2)))" lemma squarefree_part_0 [simp]: "squarefree_part 0 = {}" by (simp add: squarefree_part_def) lemma square_part_0 [simp]: "square_part 0 = 0" by (simp add: square_part_def) lemma squarefree_decompose: "∏(squarefree_part n) * square_part n ^ 2 = n" proof (cases "n = 0") case False define A s where "A = squarefree_part n" and "s = square_part n" have "(∏A) = (∏p∈A. p ^ (multiplicity p n mod 2))" by (intro prod.cong) (auto simp: A_def squarefree_part_def elim!: oddE) also have "… = (∏p∈prime_factors n. p ^ (multiplicity p n mod 2))" by (intro prod.mono_neutral_left) (auto simp: A_def squarefree_part_def) also from False have "… * s^2 = n" by (simp add: s_def square_part_def prod.distrib [symmetric] power_add [symmetric] power_mult [symmetric] prime_factorization_nat [symmetric] algebra_simps prod_power_distrib) finally show "∏A * s^2 = n" . qed simp lemma squarefree_part_pos [simp]: "∏(squarefree_part n) > 0" using prime_gt_0_nat unfolding squarefree_part_def by auto lemma squarefree_part_ge_Suc_0 [simp]: "∏(squarefree_part n) ≥ Suc 0" using squarefree_part_pos[of n] by presburger lemma squarefree_part_subset [intro]: "squarefree_part n ⊆ prime_factors n" unfolding squarefree_part_def by auto lemma squarefree_part_finite [simp]: "finite (squarefree_part n)" by (rule finite_subset[OF squarefree_part_subset]) simp lemma squarefree_part_dvd [simp]: "∏(squarefree_part n) dvd n" by (subst (2) squarefree_decompose [of n, symmetric]) simp lemma squarefree_part_dvd' [simp]: "p ∈ squarefree_part n ⟹ p dvd n" by (rule dvd_prodD[OF _ squarefree_part_dvd]) simp_all lemma square_part_dvd [simp]: "square_part n ^ 2 dvd n" by (subst (2) squarefree_decompose [of n, symmetric]) simp lemma square_part_dvd' [simp]: "square_part n dvd n" by (subst (2) squarefree_decompose [of n, symmetric]) simp lemma squarefree_part_le: "p ∈ squarefree_part n ⟹ p ≤ n" by (cases "n = 0") (simp_all add: dvd_imp_le) lemma square_part_le: "square_part n ≤ n" by (cases "n = 0") (simp_all add: dvd_imp_le) lemma square_part_le_sqrt: "square_part n ≤ nat ⌊sqrt (real n)⌋" proof - have "1 * square_part n ^ 2 ≤ ∏(squarefree_part n) * square_part n ^ 2" by (intro mult_right_mono) simp_all also have "… = n" by (rule squarefree_decompose) finally have "real (square_part n ^ 2) ≤ real n" by (subst of_nat_le_iff) simp hence "sqrt (real (square_part n ^ 2)) ≤ sqrt (real n)" by (subst real_sqrt_le_iff) simp_all also have "sqrt (real (square_part n ^ 2)) = real (square_part n)" by simp finally show ?thesis by linarith qed lemma square_part_pos [simp]: "n > 0 ⟹ square_part n > 0" unfolding square_part_def using prime_gt_0_nat by auto lemma square_part_ge_Suc_0 [simp]: "n > 0 ⟹ square_part n ≥ Suc 0" using square_part_pos[of n] by presburger lemma zero_not_in_squarefree_part [simp]: "0 ∉ squarefree_part n" unfolding squarefree_part_def by auto lemma multiplicity_squarefree_part: "prime p ⟹ multiplicity p (∏(squarefree_part n)) = (if p ∈ squarefree_part n then 1 else 0)" using squarefree_part_subset[of n] by (intro multiplicity_prod_prime_powers_nat') auto text ‹ The squarefree part really is square, its only square divisor is 1. › lemma square_dvd_squarefree_part_iff: "x^2 dvd ∏(squarefree_part n) ⟷ x = 1" proof (rule iffI, rule multiplicity_eq_nat) assume dvd: "x^2 dvd ∏(squarefree_part n)" hence "x ≠ 0" using squarefree_part_subset[of n] prime_gt_0_nat by (intro notI) auto thus x: "x > 0" by simp fix p :: nat assume p: "prime p" from p x have "2 * multiplicity p x = multiplicity p (x^2)" by (simp add: multiplicity_power_nat) also from dvd have "… ≤ multiplicity p (∏(squarefree_part n))" by (intro dvd_imp_multiplicity_le) simp_all also have "… ≤ 1" using multiplicity_squarefree_part[of p n] p by simp finally show "multiplicity p x = multiplicity p 1" by simp qed simp_all lemma squarefree_decomposition_unique1: assumes "squarefree_part m = squarefree_part n" assumes "square_part m = square_part n" shows "m = n" by (subst (1 2) squarefree_decompose [symmetric]) (simp add: assms) lemma squarefree_decomposition_unique2: assumes n: "n > 0" assumes decomp: "n = (∏A2 * s2^2)" assumes prime: "⋀x. x ∈ A2 ⟹ prime x" assumes fin: "finite A2" assumes s2_nonneg: "s2 ≥ 0" shows "A2 = squarefree_part n" and "s2 = square_part n" proof - define A1 s1 where "A1 = squarefree_part n" and "s1 = square_part n" have "finite A1" unfolding A1_def by simp note fin = ‹finite A1› ‹finite A2› have "A1 ⊆ prime_factors n" unfolding A1_def using squarefree_part_subset . note subset = this prime have "∏A1 > 0" "∏A2 > 0" using subset(1) prime_gt_0_nat by (auto intro!: prod_pos dest: prime) from n have "s1 > 0" unfolding s1_def by simp from assms have "s2 ≠ 0" by (intro notI) simp hence "s2 > 0" by simp note pos = ‹∏A1 > 0› ‹∏A2 > 0› ‹s1 > 0› ‹s2 > 0› have eq': "multiplicity p s1 = multiplicity p s2" "multiplicity p (∏A1) = multiplicity p (∏A2)" if p: "prime p" for p proof - define m where "m = multiplicity p" from decomp have "m (∏A1 * s1^2) = m (∏A2 * s2^2)" unfolding A1_def s1_def by (simp add: A1_def s1_def squarefree_decompose) with p pos have eq: "m (∏A1) + 2 * m s1 = m (∏A2) + 2 * m s2" by (simp add: m_def prime_elem_multiplicity_mult_distrib multiplicity_power_nat) moreover from fin subset p have "m (∏A1) ≤ 1" "m (∏A2) ≤ 1" unfolding m_def by ((subst multiplicity_prod_prime_powers_nat', auto)[])+ ultimately show "m s1 = m s2" by linarith with eq show "m (∏A1) = m (∏A2)" by simp qed show "s2 = square_part n" by (rule multiplicity_eq_nat) (insert pos eq'(1), auto simp: s1_def) have "∏A2 = ∏(squarefree_part n)" by (rule multiplicity_eq_nat) (insert pos eq'(2), auto simp: A1_def) with fin subset show "A2 = squarefree_part n" unfolding A1_def by (intro prod_prime_eq) auto qed lemma squarefree_decomposition_unique2': assumes decomp: "(∏A1 * s1^2) = (∏A2 * s2^2 :: nat)" assumes fin: "finite A1" "finite A2" assumes subset: "⋀x. x ∈ A1 ⟹ prime x" "⋀x. x ∈ A2 ⟹ prime x" assumes pos: "s1 > 0" "s2 > 0" defines "n ≡ ∏A1 * s1^2" shows "A1 = A2" "s1 = s2" proof - from pos have n: "n > 0" using prime_gt_0_nat by (auto simp: n_def intro!: prod_pos dest: subset) have "A1 = squarefree_part n" "s1 = square_part n" by ((rule squarefree_decomposition_unique2[of n A1 s1], insert assms n, simp_all)[])+ moreover have "A2 = squarefree_part n" "s2 = square_part n" by ((rule squarefree_decomposition_unique2[of n A2 s2], insert assms n, simp_all)[])+ ultimately show "A1 = A2" "s1 = s2" by simp_all qed text ‹ The following is a nice and simple lower bound on the number of prime numbers less than a given number due to Erd\H{o}s. In particular, it implies that there are infinitely many primes. › lemma primes_lower_bound: fixes n :: nat assumes "n > 0" defines "π ≡ λn. card {p. prime p ∧ p ≤ n}" shows "real (π n) ≥ ln (real n) / ln 4" proof - have "real n = real (card {1..n})" by simp also have "{1..n} = (λ(A, b). ∏A * b^2) ` (λn. (squarefree_part n, square_part n)) ` {1..n}" unfolding image_comp o_def squarefree_decompose case_prod_unfold fst_conv snd_conv by simp also have "card … ≤ card ((λn. (squarefree_part n, square_part n)) ` {1..n})" by (rule card_image_le) simp_all also have "… ≤ card (squarefree_part ` {1..n} × square_part ` {1..n})" by (rule card_mono) auto also have "real … = real (card (squarefree_part ` {1..n})) * real (card (square_part ` {1..n}))" by simp also have "… ≤ 2 ^ π n * sqrt (real n)" proof (rule mult_mono) have "card (squarefree_part ` {1..n}) ≤ card (Pow {p. prime p ∧ p ≤ n})" using squarefree_part_subset squarefree_part_le by (intro card_mono) force+ also have "real … = 2 ^ π n" by (simp add: π_def card_Pow) finally show "real (card (squarefree_part ` {1..n})) ≤ 2 ^ π n" by - simp_all next have "square_part k ≤ nat ⌊sqrt n⌋" if "k ≤ n" for k by (rule order.trans[OF square_part_le_sqrt]) (insert that, auto intro!: nat_mono floor_mono) hence "card (square_part ` {1..n}) ≤ card {1..nat ⌊sqrt n⌋}" by (intro card_mono) (auto intro: order.trans[OF square_part_le_sqrt]) also have "… = nat ⌊sqrt n⌋" by simp also have "real … ≤ sqrt n" by simp finally show "real (card (square_part ` {1..n})) ≤ sqrt (real n)" by - simp_all qed simp_all finally have "real n ≤ 2 ^ π n * sqrt (real n)" by - simp_all with ‹n > 0› have "ln (real n) ≤ ln (2 ^ π n * sqrt (real n))" by (subst ln_le_cancel_iff) simp_all moreover have "ln (4 :: real) = real 2 * ln 2" by (subst ln_realpow [symmetric]) simp_all ultimately show ?thesis using ‹n > 0› by (simp add: ln_mult ln_realpow[of _ "π n"] ln_sqrt field_simps) qed end

# Theory Prime_Harmonic

(* File: Prime_Harmonic.thy Author: Manuel Eberl <eberlm@in.tum.de> A lower bound for the partial sums of the prime harmonic series, and a proof of its divergence. (#81 on the list of 100 mathematical theorems) *) section ‹The Prime Harmonic Series› theory Prime_Harmonic imports "HOL-Analysis.Analysis" "HOL-Number_Theory.Number_Theory" Prime_Harmonic_Misc Squarefree_Nat begin subsection ‹Auxiliary equalities and inequalities› text ‹ First of all, we prove the following result about rearranging a product over a set into a sum over all subsets of that set. › lemma prime_harmonic_aux1: fixes A :: "'a :: field set" shows "finite A ⟹ (∏x∈A. 1 + 1 / x) = (∑x∈Pow A. 1 / ∏x)" proof (induction rule: finite_induct) fix a :: 'a and A :: "'a set" assume a: "a ∉ A" and fin: "finite A" assume IH: "(∏x∈A. 1 + 1 / x) = (∑x∈Pow A. 1 / ∏x)" from a and fin have "(∏x∈insert a A. 1 + 1 / x) = (1 + 1 / a) * (∏x∈A. 1 + 1 / x)" by simp also from fin have "… = (∑x∈Pow A. 1 / ∏x) + (∑x∈Pow A. 1 / (a * ∏x))" by (subst IH) (auto simp add: algebra_simps sum_divide_distrib) also from fin a have "(∑x∈Pow A. 1 / (a * ∏x)) = (∑x∈Pow A. 1 / ∏(insert a x))" by (intro sum.cong refl, subst prod.insert) (auto dest: finite_subset) also from a have "… = (∑x∈insert a ` Pow A. 1 / ∏x)" by (subst sum.reindex) (auto simp: inj_on_def) also from fin a have "(∑x∈Pow A. 1 / ∏x) + … = (∑x∈Pow A ∪ insert a ` Pow A. 1 / ∏x)" by (intro sum.union_disjoint [symmetric]) (simp, simp, blast) also have "Pow A ∪ insert a ` Pow A = Pow (insert a A)" by (simp only: Pow_insert) finally show " (∏x∈insert a A. 1 + 1 / x) = (∑x∈Pow (insert a A). 1 / ∏x)" . qed simp text ‹ Next, we prove a simple and reasonably accurate upper bound for the sum of the squares of any subset of the natural numbers, derived by simple telescoping. Our upper bound is approximately 1.67; the exact value is $\frac{\pi^2}{6} \approx 1.64$. (cf. Basel problem) › lemma prime_harmonic_aux2: assumes "finite (A :: nat set)" shows "(∑k∈A. 1 / (real k ^ 2)) ≤ 5/3" proof - define n where "n = max 2 (Max A)" have n: "n ≥ Max A" "n ≥ 2" by (auto simp: n_def) with assms have "A ⊆ {0..n}" by (auto intro: order.trans[OF Max_ge]) hence "(∑k∈A. 1 / (real k ^ 2)) ≤ (∑k=0..n. 1 / (real k ^ 2))" by (intro sum_mono2) auto also from n have "… = 1 + (∑k=Suc 1..n. 1 / (real k ^ 2))" by (simp add: sum.atLeast_Suc_atMost) also have "(∑k=Suc 1..n. 1 / (real k ^ 2)) ≤ (∑k=Suc 1..n. 1 / (real k ^ 2 - 1/4))" unfolding power2_eq_square by (intro sum_mono divide_left_mono mult_pos_pos) (linarith, simp_all add: field_simps less_1_mult) also have "… = (∑k=Suc 1..n. 1 / (real k - 1/2) - 1 / (real (Suc k) - 1/2))" by (intro sum.cong refl) (simp_all add: field_simps power2_eq_square) also from n have "… = 2 / 3 - 1 / (1 / 2 + real n)" by (subst sum_telescope') simp_all also have "1 + … ≤ 5/3" by simp finally show ?thesis by - simp qed subsection ‹Estimating the partial sums of the Prime Harmonic Series› text ‹ We are now ready to show our main result: the value of the partial prime harmonic sum over all primes no greater than $n$ is bounded from below by the $n$-th harmonic number $H_n$ minus some constant. In our case, this constant will be $\frac{5}{3}$. As mentioned before, using a proof of the Basel problem can improve this to $\frac{\pi^2}{6}$, but the improvement is very small and the proof of the Basel problem is a very complex one. The exact asymptotic behaviour of the partial sums is actually $\ln (\ln n) + M$, where $M$ is the Meissel--Mertens constant (approximately 0.261). › theorem prime_harmonic_lower: assumes n: "n ≥ 2" shows "(∑p←primes_upto n. 1 / real p) ≥ ln (harm n) - ln (5/3)" proof - ― ‹the set of primes that we will allow in the squarefree part› define P where "P n = set (primes_upto n)" for n { fix n :: nat have "finite (P n)" by (simp add: P_def) } note [simp] = this ― ‹The function that combines the squarefree part and the square part› define f where "f = (λ(R, s :: nat). ∏R * s^2)" ― ‹@{term f} is injective if the squarefree part contains only primes and the square part is positive.› have inj: "inj_on f (Pow (P n)×{1..n})" proof (rule inj_onI, clarify, rule conjI) fix A1 A2 :: "nat set" and s1 s2 :: nat assume A: "A1 ⊆ P n" "A2 ⊆ P n" "s1 ∈ {1..n}" "s2 ∈ {1..n}" "f (A1, s1) = f (A2, s2)" have fin: "finite A1" "finite A2" by (rule A(1,2)[THEN finite_subset], simp)+ show "A1 = A2" "s1 = s2" by ((rule squarefree_decomposition_unique2'[of A1 s1 A2 s2], insert A fin, auto simp: f_def P_def set_primes_upto)[])+ qed ― ‹@{term f} hits every number between @{term "1::nat"} and @{term "n"}. It also hits a lot of other numbers, but we do not care about those, since we only need a lower bound.› have surj: "{1..n} ⊆ f ` (Pow (P n)×{1..n})" proof fix x assume x: "x ∈ {1..n}" have "x = f (squarefree_part x, square_part x)" by (simp add: f_def squarefree_decompose) moreover have "squarefree_part x ∈ Pow (P n)" using squarefree_part_subset[of x] x by (auto simp: P_def set_primes_upto intro: order.trans[OF squarefree_part_le[of _ x]]) moreover have "square_part x ∈ {1..n}" using x by (auto simp: Suc_le_eq intro: order.trans[OF square_part_le[of x]]) ultimately show "x ∈ f ` (Pow (P n)×{1..n})" by simp qed ― ‹We now show the main result by rearranging the sum over all primes to a product over all all squarefree parts times a sum over all square parts, and then applying some simple-minded approximation› have "harm n = (∑n=1..n. 1 / real n)" by (simp add: harm_def field_simps) also from surj have "… ≤ (∑n∈f ` (Pow (P n)×{1..n}). 1 / real n)" by (intro sum_mono2 finite_imageI finite_cartesian_product) simp_all also from inj have "… = (∑x∈Pow (P n)×{1..n}. 1 / real (f x))" by (subst sum.reindex) simp_all also have "… = (∑A∈Pow (P n). 1 / real (∏A)) * (∑k=1..n. 1 / (real k)^2)" unfolding f_def by (subst sum_product, subst sum.cartesian_product) (simp add: case_prod_beta) also have "… ≤ (∑A∈Pow (P n). 1 / real (∏A)) * (5/3)" by (intro mult_left_mono prime_harmonic_aux2 sum_nonneg) (auto simp: P_def intro!: prod_nonneg) also have "(∑A∈Pow (P n). 1 / real (∏A)) = (∑A∈((`) real) ` Pow (P n). 1 / ∏A)" by (subst sum.reindex) (auto simp: inj_on_def inj_image_eq_iff prod.reindex) also have "((`) real) ` Pow (P n) = Pow (real ` P n)" by (intro image_Pow_surj refl) also have "(∑A∈Pow (real ` P n). 1 / ∏A) = (∏x∈real ` P n. 1 + 1 / x)" by (intro prime_harmonic_aux1 [symmetric] finite_imageI) simp_all also have "… = (∏i∈P n. 1 + 1 / real i)" by (subst prod.reindex) (auto simp: inj_on_def) also have "… ≤ (∏i∈P n. exp (1 / real i))" by (intro prod_mono) auto also have "… = exp (∑i∈P n. 1 / real i)" by (simp add: exp_sum) finally have "ln (harm n) ≤ ln (… * (5/3))" using n by (subst ln_le_cancel_iff) simp_all hence "ln (harm n) - ln (5/3) ≤ (∑i∈P n. 1 / real i)" by (subst (asm) ln_mult) (simp_all add: algebra_simps) thus ?thesis unfolding P_def by (subst (asm) sum.distinct_set_conv_list) simp_all qed text ‹ We can use the inequality $\ln (n + 1) \le H_n$ to estimate the asymptotic growth of the partial prime harmonic series. Note that $H_n \sim \ln n + \gamma$ where $\gamma$ is the Euler--Mascheroni constant (approximately 0.577), so we lose some accuracy here. › corollary prime_harmonic_lower': assumes n: "n ≥ 2" shows "(∑p←primes_upto n. 1 / real p) ≥ ln (ln (n + 1)) - ln (5/3)" proof - from assms ln_le_harm[of n] have "ln (ln (real n + 1)) ≤ ln (harm n)" by simp also from assms have "… - ln (5/3) ≤ (∑p←primes_upto n. 1 / real p)" by (rule prime_harmonic_lower) finally show ?thesis by - simp qed (* TODO: Not needed in Isabelle 2016 *) lemma Bseq_eventually_mono: assumes "eventually (λn. norm (f n) ≤ norm (g n)) sequentially" "Bseq g" shows "Bseq f" proof - from assms(1) obtain N where N: "⋀n. n ≥ N ⟹ norm (f n) ≤ norm (g n)" by (auto simp: eventually_at_top_linorder) from assms(2) obtain K where K: "⋀n. norm (g n) ≤ K" by (blast elim!: BseqE) { fix n :: nat have "norm (f n) ≤ max K (Max {norm (f n) |n. n < N})" apply (cases "n < N") apply (rule max.coboundedI2, rule Max.coboundedI, auto) [] apply (rule max.coboundedI1, force intro: order.trans[OF N K]) done } thus ?thesis by (blast intro: BseqI') qed lemma Bseq_add: assumes "Bseq (f :: nat ⇒ 'a :: real_normed_vector)" shows "Bseq (λx. f x + c)" proof - from assms obtain K where K: "⋀x. norm (f x) ≤ K" unfolding Bseq_def by blast { fix x :: nat have "norm (f x + c) ≤ norm (f x) + norm c" by (rule norm_triangle_ineq) also have "norm (f x) ≤ K" by (rule K) finally have "norm (f x + c) ≤ K + norm c" by simp } thus ?thesis by (rule BseqI') qed lemma convergent_imp_Bseq: "convergent f ⟹ Bseq f" by (simp add: Cauchy_Bseq convergent_Cauchy) (* END TODO *) text ‹ We now use our last estimate to show that the prime harmonic series diverges. This is obvious, since it is bounded from below by $\ln (\ln (n + 1))$ minus some constant, which obviously tends to infinite. Directly using the divergence of the harmonic series would also be possible and shorten this proof a bit.. › corollary prime_harmonic_series_unbounded: "¬Bseq (λn. ∑p←primes_upto n. 1 / p)" (is "¬Bseq ?f") proof assume "Bseq ?f" hence "Bseq (λn. ?f n + ln (5/3))" by (rule Bseq_add) have "Bseq (λn. ln (ln (n + 1)))" proof (rule Bseq_eventually_mono) from eventually_ge_at_top[of "2::nat"] show "eventually (λn. norm (ln (ln (n + 1))) ≤ norm (?f n + ln (5/3))) sequentially" proof eventually_elim fix n :: nat assume n: "n ≥ 2" hence "norm (ln (ln (real n + 1))) = ln (ln (real n + 1))" using ln_ln_nonneg[of "real n + 1"] by simp also have "… ≤ ?f n + ln (5/3)" using prime_harmonic_lower'[OF n] by (simp add: algebra_simps) also have "?f n + ln (5/3) ≥ 0" by (intro add_nonneg_nonneg sum_list_nonneg) simp_all hence "?f n + ln (5/3) = norm (?f n + ln (5/3))" by simp finally show "norm (ln (ln (n + 1))) ≤ norm (?f n + ln (5/3))" by (simp add: add_ac) qed qed fact then obtain k where k: "k > 0" "⋀n. norm (ln (ln (real (n::nat) + 1))) ≤ k" by (auto elim!: BseqE simp: add_ac) define N where "N = nat ⌈exp (exp k)⌉" have N_pos: "N > 0" unfolding N_def by simp have "real N + 1 > exp (exp k)" unfolding N_def by linarith hence "ln (real N + 1) > ln (exp (exp k))" by (subst ln_less_cancel_iff) simp_all with N_pos have "ln (ln (real N + 1)) > ln (exp k)" by (subst ln_less_cancel_iff) simp_all hence "k < ln (ln (real N + 1))" by simp also have "… ≤ norm (ln (ln (real N + 1)))" by simp finally show False using k(2)[of N] by simp qed corollary prime_harmonic_series_diverges: "¬convergent (λn. ∑p←primes_upto n. 1 / p)" using prime_harmonic_series_unbounded convergent_imp_Bseq by blast end