Ported for Lean Pool from PrimeNumberTheoremAnd commit 0c7abf7be7765dc5ffd21afc1c37b018199ec3c9, via wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022 (both Apache-2.0). The port adds the MooreBound namespace and updates Mathlib APIs and proof style. Wiener and Consequences retain the PNT and prime-interval dependency closure; unrelated later developments and LeanArchitect annotations are omitted.

theorem MooreBound.Real.tendsto_pow_log_div_pow_atTop (a b : ℝ) (ha : 0 < a) : Filter.Tendsto (fun (x : ℝ) => Real.log x ^ b / x ^ a) Filter.atTop (nhds 0)

log^b x / x^a goes to zero at infinity if a is positive.