English
The set of k-rough numbers up to N equals the biUnion over primes p in ((N+1).primesBelow \ k.primesBelow) of the sets {m ∈ {1,...,N} | p ∣ m}.
Русский
Множество k-шероховатых чисел до N равно биобъединению по простым p ∈ ((N+1).primesBelow \ k.primesBelow) множеств {m ≤ N | p ∣ m}.
LaTeX
$$$\mathrm{roughNumbersUpTo}(N,k) = ((N+1).primesBelow \ k.primesBelow).biUnion\, (\lambda p, \{ m \in \mathrm{Finset.range}(N+1) \mid m \neq 0 \land p \mid m \})$$$
Lean4
/-- The sum over primes `k ≤ p ≤ 4^(π(k-1)+1)` over `1/p` (as a real number) is at least `1/2`. -/
theorem one_half_le_sum_primes_ge_one_div (k : ℕ) :
1 / 2 ≤ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, (1 / p : ℝ) :=
by
set m : ℕ := 2 ^ k.primesBelow.card
set N₀ : ℕ := 2 * m ^ 2 with hN₀
let S : ℝ := ((2 * N₀).succ.primesBelow \ k.primesBelow).sum (fun p ↦ (1 / p : ℝ))
suffices 1 / 2 ≤ S by
convert this using 5
rw [show 4 = 2 ^ 2 by simp, pow_right_comm]
ring
suffices 2 * N₀ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S by
rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add', cast_mul, cast_mul, cast_pow,
cast_two, show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
mul_le_mul_iff_right₀ <| by positivity] at this
calc
(2 * N₀ : ℝ)
_ = ((2 * N₀).smoothNumbersUpTo k).card + ((2 * N₀).roughNumbersUpTo k).card := by
exact_mod_cast ((2 * N₀).smoothNumbersUpTo_card_add_roughNumbersUpTo_card k).symm
_ ≤ m * (2 * N₀).sqrt + ((2 * N₀).roughNumbersUpTo k).card := by
exact_mod_cast Nat.add_le_add_right ((2 * N₀).smoothNumbersUpTo_card_le k) _
_ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S := add_le_add_left ?_ _
exact_mod_cast roughNumbersUpTo_card_le' (2 * N₀) k
