Prime reciprocal sums on logarithmic intervals

This module turns the uniform error term in Mertens' second theorem into the fixed-endpoint limit

∑_{N^a < p ≤ N^b} 1 / p → log (b / a)

for 0 < a < b. Both cutoffs are real powers; the finite carrier uses the floor of the upper cutoff, and the lower endpoint remains strict.

noncomputable def MathlibNt.SieveTheory.PrimeReciprocalLogScale.rpowFloor (N : ℕ) (a : ℝ) : ℕ

The natural cutoff obtained by flooring the real power N ^ a.

Equations

• MathlibNt.SieveTheory.PrimeReciprocalLogScale.rpowFloor N a = ⌊↑N ^ a⌋₊

noncomputable def MathlibNt.SieveTheory.PrimeReciprocalLogScale.primeReciprocalLogInterval (N : ℕ) (a b : ℝ) : ℝ

The reciprocal sum over primes in the real interval N ^ a < p ≤ N ^ b.

Equations

• MathlibNt.SieveTheory.PrimeReciprocalLogScale.primeReciprocalLogInterval N a b = ∑ p ∈ Finset.range (MathlibNt.SieveTheory.PrimeReciprocalLogScale.rpowFloor N b + 1) with Nat.Prime p ∧ ↑N ^ a < ↑p ∧ ↑p ≤ ↑N ^ b, 1 / ↑p

theorem MathlibNt.SieveTheory.PrimeReciprocalLogScale.tendsto_rpowFloor_atTop {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (N : ℕ) => rpowFloor N a) Filter.atTop Filter.atTop

A positive real power, restricted to natural inputs and then floored, tends to infinity.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogScale.eventually_two_le_rpowFloor {a : ℝ} (ha : 0 < a) : ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ rpowFloor N a

In particular, the floored power is eventually in the range where the uniform Mertens estimate applies.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogScale.tendsto_rpowFloor_div_rpow {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (N : ℕ) => ↑(rpowFloor N a) / ↑N ^ a) Filter.atTop (nhds 1)

Flooring a positive real power changes it by a relative error tending to zero.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogScale.tendsto_log_rpowFloor_atTop {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (N : ℕ) => Real.log ↑(rpowFloor N a)) Filter.atTop Filter.atTop

The logarithm of a floored positive power tends to infinity.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogScale.tendsto_log_rpowFloor_sub_log_rpow {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (N : ℕ) => Real.log ↑(rpowFloor N a) - Real.log (↑N ^ a)) Filter.atTop (nhds 0)

The first logarithm is unchanged asymptotically by flooring.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogScale.tendsto_log_log_rpowFloor_sub {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (N : ℕ) => Real.log (Real.log ↑(rpowFloor N a)) - (Real.log a + Real.log (Real.log ↑N))) Filter.atTop (nhds 0)

Supporting log--log asymptotic, including the exact log (N ^ a) = a log N algebra: log log floor(N^a) = log a + log log N + o(1).

theorem MathlibNt.SieveTheory.PrimeReciprocalLogScale.primeReciprocalLogInterval_eq_sub (N : ℕ) {a b : ℝ} (hN : 1 ≤ N) (hab : a ≤ b) : primeReciprocalLogInterval N a b = MertensTheorem.primeReciprocalSum (rpowFloor N b) - MertensTheorem.primeReciprocalSum (rpowFloor N a)

The real-cutoff interval sum is exactly the difference of the two Mertens prefixes. Thus the lower endpoint is strict and the upper endpoint is non-strict, with no rounding error term.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogScale.tendsto_primeReciprocalLogInterval {a b : ℝ} (ha : 0 < a) (hab : a < b) : Filter.Tendsto (fun (N : ℕ) => primeReciprocalLogInterval N a b) Filter.atTop (nhds (Real.log (b / a)))

For fixed 0 < a < b, the reciprocal sum over the real interval N^a < p ≤ N^b tends to log (b / a).

theorem MathlibNt.SieveTheory.PrimeReciprocalLogScale.eventually_abs_primeReciprocalLogInterval_sub_lt {a b ε : ℝ} (ha : 0 < a) (hab : a < b) (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, |primeReciprocalLogInterval N a b - Real.log (b / a)| < ε

Quantitative eventual form of the fixed-cell limit. It is directly suitable for taking a maximum of the finitely many thresholds belonging to a fixed partition.

theorem MathlibNt.SieveTheory.PrimeReciprocalLogScale.exists_abs_primeReciprocalLogInterval_sub_lt {a b ε : ℝ} (ha : 0 < a) (hab : a < b) (hε : 0 < ε) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → |primeReciprocalLogInterval N a b - Real.log (b / a)| < ε

Threshold form of the quantitative fixed-cell estimate.