Liu's prime-pair sum to integral transfer #
This module combines the refining logarithmic-grid limit with the finite prime
limit for one fixed grid. The grid is chosen before the finite-N threshold,
preserving the quantifier order in Liu's source transfer.
Liu's finite reciprocal-log prime-pair sum is eventually bounded by the source integral, with an arbitrary positive additive error.
Inspect dependencies
MathlibNt.SieveTheory.LiuWeight.liuSourcePrimeSumToIntegralTransfer · compiled type and proof/definition references.
theorem
MathlibNt.SieveTheory.LiuWeight.eventually_liuSourceReciprocalLogBound :
∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → LiuSourceReciprocalLogBound N
Liu's exact source reciprocal-log estimate holds for all sufficiently large
N, unconditionally.
Inspect dependencies
MathlibNt.SieveTheory.LiuWeight.eventually_liuSourceReciprocalLogBound · compiled type and proof/definition references.