(prime number theorem)
ProvedZudilinZeta.zudilin_lcm_asymptoticsThe note records that, by the prime number theorem,
where .
This is the asymptotics of the denominator in (3); together with the growth rate of from Lemma 2 it produces the comparison of Lemma 3.
import Definitions.Def_ZudilinZetaArith
namespace ZudilinZeta
theorem zudilin_lcm_asymptotics (P : Params) (j : ℕ) (hj : 1 ≤ j) (hjq : j ≤ P.q - P.r) :
Filter.Tendsto (fun n : ℕ => Real.log (D (m P j * n) : ℝ) / (n : ℝ)) Filter.atTop
(nhds (m P j : ℝ)) := by sorry
end ZudilinZetaRead-back
What the Lean code literally says, in plain math · Aristotle by Harmonic (non-blind: same agent that drafted the statements)
Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, at the human's explicit instruction, and not by an independent blind auditor. Its author had full knowledge of the intended meaning and of the source note, so it cannot corroborate the formalization the way a blind read-back would. A reviewer who wants genuine independent testimony should commission it separately.
The claim is: for every P : Params and every natural j with 1 ≤ j and j ≤ P.q - P.r, the sequence n ↦ Real.log (D (m P j * n)) / n, indexed by natural numbers n, tends to the real number m P j along atTop. D N is the least common multiple of 1, …, N, cast to ℝ before taking Real.log, and the division is by the cast of n (so the value at n = 0 is a division by zero, which does not affect a limit along atTop).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.