English
A variant bound: (roughNumbersUpTo N k).card ≤ N · (N.succ.primesBelow \ k.primesBelow).sum (1/p) in Real numbers.
Русский
Вариант верхней оценки: кардинальность roughNumbersUpTo(N,k) ≤ N · ∑ 1/p по p ∈ (N+1).primesBelow \ k.primesBelow, в вещественных числах.
LaTeX
$$$\#(\mathrm{roughNumbersUpTo}(N,k)).card \le N \cdot \left( (N.succ.primesBelow \ k.primesBelow).sum(\lambda p, (1 : \mathbb{R}) / p) \right)$$$
Lean4
/-- The sum over the reciprocals of the primes diverges. -/
theorem not_summable_one_div_on_primes : ¬Summable (indicator {p | p.Prime} (fun n : ℕ ↦ (1 : ℝ) / n)) :=
by
intro h
obtain ⟨k, hk⟩ := h.nat_tsum_vanishing (Iio_mem_nhds one_half_pos : Iio (1 / 2 : ℝ) ∈ 𝓝 0)
specialize hk ({p | Nat.Prime p} ∩ {p | k ≤ p}) inter_subset_right
rw [tsum_subtype, indicator_indicator, inter_eq_left.mpr fun n hn ↦ hn.1, mem_Iio] at hk
have h' : Summable (indicator ({p | Nat.Prime p} ∩ {p | k ≤ p}) fun n ↦ (1 : ℝ) / n) :=
by
convert h.indicator {n : ℕ | k ≤ n} using 1
simp only [indicator_indicator, inter_comm]
refine ((one_half_le_sum_primes_ge_one_div k).trans_lt <| LE.le.trans_lt ?_ hk).false
convert
Summable.sum_le_tsum (primesBelow ((4 ^ (k.primesBelow.card + 1)).succ) \ primesBelow k)
(fun n _ ↦ indicator_nonneg (fun p _ ↦ by positivity) _) h' using
2 with p hp
obtain ⟨hp₁, hp₂⟩ := mem_setOf_eq ▸ Finset.mem_sdiff.mp hp
have hpp := prime_of_mem_primesBelow hp₁
refine (indicator_of_mem ?_ fun n : ℕ ↦ (1 / n : ℝ)).symm
exact ⟨hpp, by simpa [primesBelow, hpp] using hp₂⟩
