Energy estimate and logarithmic asymptotic (§5.3 of the proof notes).

The result is stated in exponential form, |Q_n(C_r)| ≤ exp((−6 + ε) n²): a logarithmic form would, with Lean's convention Real.log 0 = 0, silently assert that Q_n(C_r) ≠ 0, which the energy method does not give. energy_bound_of_inputs_log gives the logarithmic form wherever the value is nonzero.

Module map (Zeta32/Analytic/Energy/): Pointwise, Stirling, LogNorm, Scaling — (5′), (6′); PoissonKernel, Component, Poisson, CIntegrals, Regularity, Potential — (8′), (11′), (15′) and the identification with rhoA, Wt, ellA, massA of FstarDefs; ZeroMass, CircleTools, Discrete — (12), (13′); Assembly — (14′) and the constant.

theorem Zeta32.Analytic.energy_bound_of_inputs (r : ℚ) : (∀ (n : ℕ), HeineBound r n) → FstarInput → ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |(Polynomial.aeval (Cr r)) (Qtilde r n)| ≤ Real.exp ((-6 + ε) * ↑n ^ 2)

theorem Zeta32.Analytic.energy_bound_of_inputs_log (r : ℚ) : (∀ (n : ℕ), HeineBound r n) → FstarInput → ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, (Polynomial.aeval (Cr r)) (Qtilde r n) ≠ 0 → Real.log |(Polynomial.aeval (Cr r)) (Qtilde r n)| ≤ (-6 + ε) * ↑n ^ 2