Converse knapsack bound for Landau's function

Proved

LandauCriterion.converse_primePow_prod_le

by pitimespi · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorylandau-functionriemann-hypothesis

Let $t$ be a finite set of prime powers with distinct primes: there is a function assigning to each $q \in t$ a prime $f(q)$ with $q = f(q)^k$ for some $k \ge 1$ , and $f$ is injective on $t$ . If the elements of $t$ sum to at most $n$ , then their product is at most $g(n)$ (here in the form landauLocal n, the platform's mirror of Landau's function). Together with the decomposition direction, this says $g(n)$ is exactly the knapsack optimum over prime-power families. The injectivity hypothesis is essential: without distinct primes the claim is false (for example $t = \{2, 4\}$ ).

Preamble

import Mathlib
import Definitions.Def_LandauExplore_landauLocal
import Definitions.Def_LandauFunction_landau
open Finset LandauExplore LandauFunction

Formal statement

namespace LandauCriterion
theorem converse_primePow_prod_le {n : ℕ} {t : Finset ℕ}
    (hf : ∃ f : ℕ → ℕ, (∀ q ∈ t, (f q).Prime ∧ ∃ k : ℕ, 1 ≤ k ∧ q = (f q) ^ k) ∧ Set.InjOn f t)
    (hsum : ∑ q ∈ t, q ≤ n) : ∏ q ∈ t, q ≤ landauLocal n := by sorry
end LandauCriterion

Source

Local lemma `prod_primePow_le_landauLocal` in the Landau (B) exploration (verified locally, not yet on the platform); the knapsack characterization of Landau's function, cf. Massias, Nicolas, Robin, Acta Arith. 50 (1988).

Read-back

What the Lean code literally says, in plain math · Muse Spark

For every natural number $n$ and every finite set $t$ of natural numbers, if there exists a function $f : \mathbb{N} \to \mathbb{N}$ such that (i) for every $q \in t$ , $f(q)$ is prime and there exists a natural number $k \ge 1$ , possibly depending on $q$ , with $q = f(q)^k$ , and (ii) $f$ is injective on $t$ — that is, $q_1, q_2 \in t$ and $f(q_1) = f(q_2)$ imply $q_1 = q_2$ — and if additionally $\sum_{q \in t} q \le n$ , then $\prod_{q \in t} q \le \operatorname{landauLocal}(n)$ , where $\operatorname{landauLocal}(n)$ is taken as a given quantity and is not further specified by this statement. The quantification is over all $n$ and $t$ , with no assumption that $t$ is nonempty and no lower bound on $n$ ; the function $f$ is constrained only on $t$ and may be arbitrary elsewhere, and the conclusion is a non-strict inequality, not a strict one, with no converse asserted. In the edge case $t = \varnothing$ , condition (i) and injectivity hold vacuously for any $f$ , the sum is $0$ (hence the sum hypothesis holds for every $n$ ), and the empty product is $1$ , so the statement then asserts $1 \le \operatorname{landauLocal}(n)$ ; more generally, since each $q \in t$ must equal a prime power with exponent at least $1$ , any nonempty $t$ satisfying the hypotheses has every element at least $2$ , so the hypotheses can hold with $n = 0$ or $n = 1$ only when $t$ is empty.

Human review

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

View graph