Positivity of the finite Dickman function on the required range

Proved

Erdos390.Full.DickmanBasic.rho_pos_on_zero_five

by doctosil · Sep 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theoryerdos-390erdos390-source-construction

Let $\rho_0(x)=1$ for every real $x$ , and define recursively

\rho_{n+1}(x)=\begin{cases}1&x\le1,\\1-\int_1^x\frac{\rho_n(t-1)}{\max(t,1)}\,dt&x>1.\end{cases}

For the fifth approximant $\rho=\rho_5$ , every real $x\in[0,5]$ satisfies

\rho(x)>0.

This gives positivity on the entire finite range used by the Poisson–Dickman construction, in particular the nonzero normalization at $x=9/2$ .

Preamble

import Definitions.Def_erdos390_dickman_step_function

Formal statement

theorem Erdos390.Full.DickmanBasic.rho_pos_on_zero_five :
    ∀ {x : ℝ} (hx0 : 0 ≤ x) (hx5 : x ≤ 5), 0 < Erdos390.Full.DickmanBasic.rho x := by sorry

Source