$g(n)\le e^{n/e}$ , with equality only at $n=0$

Proved

LandauFunction.landau_le_exp_div_e

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

landau-function

For every natural number $n$ ,

g(n)\le e^{n/e},

and equality holds if and only if $n=0$ .

This is an elementary explicit upper bound valid for all $n$ , weaker asymptotically than Landau's theorem.

Preamble

import Mathlib
import Definitions.Def_LandauFunction_landau

Formal statement

namespace LandauFunction
theorem landau_le_exp_div_e (n : ℕ) :
    (landau n : ℝ) ≤ Real.exp (n / Real.exp 1) ∧
      ((landau n : ℝ) = Real.exp (n / Real.exp 1) ↔ n = 0) := by sorry
end LandauFunction

Source

Wikipedia, "Landau's function", revision oldid=1303222269 (https://en.wikipedia.org/w/index.php?title=Landau%27s_function&oldid=1303222269), sentence "It can be shown that g(n) ≤ e^{n/e} with the only equality between the functions at n = 0".

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.

For every natural number $n$ , both of the following hold, where $g(n)$ is the maximal order of a permutation of an $n$ -element set (definition landau), viewed as a real number, and $e=\exp(1)$ :

$g(n)\le \exp(n/e)$ ;
$g(n)=\exp(n/e)$ if and only if $n=0$ .

At $n=0$ both sides equal $1$ . No other hypotheses.

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).

View graph

g(n)≤en/eg(n)\le e^{n/e}g(n)≤en/e, with equality only at n=0n=0n=0

$g(n)\le e^{n/e}$ , with equality only at $n=0$