Quadratic exponential decay dominates every fixed denominator

Proved

Apery.tendsto_pow_mul_exp_neg_sq_of_pos

by tomasz · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

formalizationirrationalitynumber-theoryzeta5-mo271

For every real $c>0$ and every positive natural number $b$ ,

\lim_{n\to\infty}b^{37n}e^{-cn^2}=0.

This supplies the decay hypothesis of the polynomial irrationality criterion for any strictly positive quadratic decay rate, including the rate provided by the repository's modified normalization.

Preamble

import Mathlib

open Polynomial Filter Topology MeasureTheory

Formal statement

namespace Apery

theorem tendsto_pow_mul_exp_neg_sq_of_pos {c : ℝ} (hc : 0 < c) (b : ℕ) (hb : 0 < b) :
    Tendsto (fun n : ℕ => (b : ℝ) ^ (37 * n) * Real.exp (-c * (n : ℝ) ^ 2)) atTop (𝓝 0) := by sorry

end Apery

Source

https://github.com/mo271/Zeta5/blob/7fe736760f4b96bfdb4334b68e3b3124ecbe10b0/Apery/Criterion.lean#L98-L119

Read-back

What the Lean code literally says, in plain math · GPT-6 (Codex independent auditor)

For every real number $c$ satisfying $c>0$ and every natural number $b$ satisfying $b>0$ , the real sequence $b^{37n}\exp(-cn^2)$ , with $b$ and $n$ embedded in $\mathbb R$ , tends to $0$ as the natural number $n$ tends to infinity. The allowed bases include $b=1$ and exclude $b=0$ ; the sequence is defined at $n=0$ , where its value is $1$ .

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by tomasz · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph