Three-term asymptotic expansion of $\ln g(n)$ (Massias–Nicolas–Robin 1988)

Proved

LandauFunction.landau_log_asymptotic_expansion

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptoticslandau-function

As $n\to\infty$ ,

\ln g(n)=\sqrt{n\ln n}\left(1+\frac{\ln\ln n-1}{2\ln n}-\frac{(\ln\ln n)^2-6\ln\ln n+9}{8(\ln n)^2}+O\!\left(\left(\frac{\ln\ln n}{\ln n}\right)^{3}\right)\right).

This refines Landau's theorem $\ln g(n)\sim\sqrt{n\ln n}$ by two further terms.

Formalization Note The statement is that the difference between $\ln g(n)$ and the explicit main term is $O\bigl(\sqrt{n\ln n}\,(\ln\ln n/\ln n)^3\bigr)$ along $n\to\infty$ in $\mathbb N$ .

Preamble

import Mathlib
import Definitions.Def_LandauFunction_landau

Formal statement

namespace LandauFunction
theorem landau_log_asymptotic_expansion :
    (fun n : ℕ => Real.log (landau n) - Real.sqrt (n * Real.log n) *
        (1 + (Real.log (Real.log n) - 1) / (2 * Real.log n)
          - (Real.log (Real.log n) ^ 2 - 6 * Real.log (Real.log n) + 9) / (8 * Real.log n ^ 2)))
      =O[Filter.atTop]
      (fun n : ℕ => Real.sqrt (n * Real.log n) * (Real.log (Real.log n) / Real.log n) ^ 3) := by
  sorry
end LandauFunction

Source

Massias, Nicolas, Robin, Acta Arith. 50 (1988) 221–242; as quoted in Wikipedia, "Landau's function", revision oldid=1303222269 (https://en.wikipedia.org/w/index.php?title=Landau%27s_function&oldid=1303222269), display after "More precisely", ref. [3].

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source material and of the intended meaning. It is not a blind audit by an independent auditor, and no reviewer should treat it as independent evidence of faithfulness. It was produced at the explicit request of the proposal owner.

Write $L=\ln n$ and $LL=\ln\ln n$ (real natural logarithms; the library sets $\ln 0=0$ and $\ln x=\ln|x|$ , and $x/0=0$ , but these conventions only matter for $n\le 2$ , which is irrelevant to an eventual statement). Let $g(n)$ be the maximal order of a permutation of an $n$ -element set (definition landau). The statement asserts that, as $n\to\infty$ through the natural numbers,

\ln g(n)-\sqrt{nL}\left(1+\frac{LL-1}{2L}-\frac{LL^2-6\,LL+9}{8L^2}\right)=O\!\left(\sqrt{nL}\left(\frac{LL}{L}\right)^{3}\right),

i.e. there are constants $C$ and $N$ such that for all $n\ge N$ the absolute value of the left-hand side is at most $C$ times the absolute value of $\sqrt{nL}\,(LL/L)^3$ . No hypotheses are imposed.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by pitimespi · Nov 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Three-term asymptotic expansion of ln⁡g(n)\ln g(n)lng(n) (Massias–Nicolas–Robin 1988)

Three-term asymptotic expansion of $\ln g(n)$ (Massias–Nicolas–Robin 1988)