HarmonicAnalysis

Harmonic majorization and quantitative asymptotic estimates.

theorem CohnElkies.tendsto_saddleSourceSecondBranchLocalTailMajorant : Filter.Tendsto (fun (ℓ : ℝ) => 2 * √(400 * Real.exp 1 * Real.pi) * Real.exp (-(ℓ ^ (1 / 6) / (400 * Real.exp 1)))) Filter.atTop (nhds 0)

The local-tail majorant for the second saddle branch vanishes asymptotically.