Analytic Number Theory Domain Library

The ANT domain library packages specialized number-theoretic certificates on top of LeanCert's general proof templates.

Use this section when the statement is about Chebyshev functions, Abel summation, Euler/log products, Dirichlet sums, Mertens sums, or explicit-PNT transfer schemas.

Topic	Use when you need...
Chebyshev	finite-range bounds for ψ and θ
Finite ANT	step sums, Abel transforms, Euler/log products, Dirichlet truncations, and Mertens finite sums
ANT Asymptotic	Stieltjes-Abel and Dirichlet-hyperbola transforms over AsympEnv
Explicit PNT	ψ → θ and θ → π transfer schemas

For reusable proof patterns independent of ANT, see Proof Templates.