Dickman–de Bruijn function

DefinitionDickman–de Bruijn functions#✓fully proved

A function \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function if \(\rho(u) = 0\) for every real \(u < 0\), \(\rho\) maps \([0, \infty)\) into \([0, 1]\), \(\rho\) is continuous on \([0, \infty)\), \(\rho(u) = 1\) for every \(u \in [0, 1]\), and for every real \(u > 1\) the function \(\rho\) is differentiable at \(u\) with \(u \rho'(u) + \rho(u - 1) = 0\).

These conditions describe the Dickman–de Bruijn function, extended by zero to negative inputs. Continuity is asserted only on the original nonnegative domain, since the total zero extension is discontinuous at zero.

def IsDickmanDeBruijn (ρ : ℝ → ℝ) : Prop :=
  (∀ u, u < 0 → ρ u = 0) ∧
    Set.MapsTo ρ (Set.Ici (0 : ℝ)) (Set.Icc (0 : ℝ) 1) ∧
    ContinuousOn ρ (Set.Ici (0 : ℝ)) ∧
    (∀ u ∈ Set.Icc (0 : ℝ) 1, ρ u = 1) ∧
    ∀ u, 1 < u → DifferentiableAt ℝ ρ u ∧ u * deriv ρ u + ρ (u - 1) = 0

Used by 12

Used byContinuity of the Dickman–de Bruijn function on the nonnegative reals · Delay differential equation of the Dickman–de Bruijn function · Differentiability of the Dickman–de Bruijn function above one · The Dickman–de Bruijn function equals one on the unit interval · Normalization of the Dickman–de Bruijn function, inequality form · The Dickman–de Bruijn function vanishes on the negative reals · Existence and uniqueness of the Dickman–de Bruijn function · Upper bound one for the Dickman–de Bruijn function on the nonnegative reals · Range of the Dickman–de Bruijn function on the nonnegative reals · Pointwise range bound for the Dickman–de Bruijn function · Nonnegativity of the Dickman–de Bruijn function · Explicit lower bound for the Dickman function

LemmaThe Dickman–de Bruijn function vanishes on the negative reals#✓fully proved

If \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function, then \(\rho(u) = 0\) for every real \(u < 0\).

lemma IsDickmanDeBruijn.eq_zero_of_neg {ρ : ℝ → ℝ}
    (h : IsDickmanDeBruijn ρ) {u : ℝ} (hu : u < 0) : ρ u = 0

Uses 1

Statement usesDickman–de Bruijn functions

LemmaRange of the Dickman–de Bruijn function on the nonnegative reals#✓fully proved

If \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function, then \(0 \le \rho(u) \le 1\) for every real \(u \ge 0\).

lemma IsDickmanDeBruijn.mapsTo_Ici_Icc {ρ : ℝ → ℝ}
    (h : IsDickmanDeBruijn ρ) :
    Set.MapsTo ρ (Set.Ici (0 : ℝ)) (Set.Icc (0 : ℝ) 1)

Uses 1 · Used by 3

Statement usesDickman–de Bruijn functions

Used byUpper bound one for the Dickman–de Bruijn function on the nonnegative reals · Pointwise range bound for the Dickman–de Bruijn function · Nonnegativity of the Dickman–de Bruijn function

LemmaContinuity of the Dickman–de Bruijn function on the nonnegative reals#✓fully proved

If \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function, then \(\rho\) is continuous on \([0, \infty)\).

lemma IsDickmanDeBruijn.continuousOn_Ici {ρ : ℝ → ℝ}
    (h : IsDickmanDeBruijn ρ) : ContinuousOn ρ (Set.Ici (0 : ℝ))

Uses 1

Statement usesDickman–de Bruijn functions

LemmaThe Dickman–de Bruijn function equals one on the unit interval#✓fully proved

If \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function, then \(\rho(u) = 1\) for every \(u \in [0, 1]\).

lemma IsDickmanDeBruijn.eq_one_of_mem_Icc {ρ : ℝ → ℝ}
    (h : IsDickmanDeBruijn ρ) {u : ℝ} (hu : u ∈ Set.Icc (0 : ℝ) 1) : ρ u = 1

Uses 1 · Used by 1

Statement usesDickman–de Bruijn functions

Used byNormalization of the Dickman–de Bruijn function, inequality form

LemmaNormalization of the Dickman–de Bruijn function, inequality form#✓fully proved

If \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function and \(u\) is a real number with \(0 \le u\) and \(u \le 1\), then \(\rho(u) = 1\).

lemma IsDickmanDeBruijn.eq_one_of_nonneg_of_le_one {ρ : ℝ → ℝ}
    (h : IsDickmanDeBruijn ρ) {u : ℝ} (h0 : 0 ≤ u) (h1 : u ≤ 1) : ρ u = 1

Uses 2

Statement usesDickman–de Bruijn functions

Proof usesThe Dickman–de Bruijn function equals one on the unit interval

LemmaDifferentiability of the Dickman–de Bruijn function above one#✓fully proved

If \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function, then \(\rho\) is differentiable at every real \(u > 1\).

lemma IsDickmanDeBruijn.differentiableAt_of_one_lt {ρ : ℝ → ℝ}
    (h : IsDickmanDeBruijn ρ) {u : ℝ} (hu : 1 < u) : DifferentiableAt ℝ ρ u

Uses 1

Statement usesDickman–de Bruijn functions

LemmaDelay differential equation of the Dickman–de Bruijn function#✓fully proved

If \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function, then \(u \rho'(u) + \rho(u - 1) = 0\) for every real \(u > 1\).

lemma IsDickmanDeBruijn.delay_eq {ρ : ℝ → ℝ}
    (h : IsDickmanDeBruijn ρ) {u : ℝ} (hu : 1 < u) :
    u * deriv ρ u + ρ (u - 1) = 0

Uses 1

Statement usesDickman–de Bruijn functions

LemmaNonnegativity of the Dickman–de Bruijn function#✓fully proved

If \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function, then \(\rho(u) \ge 0\) for every real \(u \ge 0\).

lemma IsDickmanDeBruijn.nonneg_of_nonneg {ρ : ℝ → ℝ}
    (h : IsDickmanDeBruijn ρ) {u : ℝ} (hu : 0 ≤ u) : 0 ≤ ρ u

Uses 2

Statement usesDickman–de Bruijn functions

Proof usesRange of the Dickman–de Bruijn function on the nonnegative reals

LemmaUpper bound one for the Dickman–de Bruijn function on the nonnegative reals#✓fully proved

If \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function, then \(\rho(u) \le 1\) for every real \(u \ge 0\).

lemma IsDickmanDeBruijn.le_one_of_nonneg {ρ : ℝ → ℝ}
    (h : IsDickmanDeBruijn ρ) {u : ℝ} (hu : 0 ≤ u) : ρ u ≤ 1

Uses 2

Statement usesDickman–de Bruijn functions

Proof usesRange of the Dickman–de Bruijn function on the nonnegative reals

LemmaPointwise range bound for the Dickman–de Bruijn function#✓fully proved

If \(\rho : \mathbb{R} \to \mathbb{R}\) is a Dickman–de Bruijn function and \(u \ge 0\) is real, then \(\rho(u) \in [0, 1]\).

lemma IsDickmanDeBruijn.mem_Icc_of_nonneg {ρ : ℝ → ℝ}
    (h : IsDickmanDeBruijn ρ) {u : ℝ} (hu : 0 ≤ u) : ρ u ∈ Set.Icc (0 : ℝ) 1

Uses 2

Statement usesDickman–de Bruijn functions

Proof usesRange of the Dickman–de Bruijn function on the nonnegative reals

TheoremExistence and uniqueness of the Dickman–de Bruijn function#✓fully proved

There is exactly one function \(\rho : \mathbb{R} \to \mathbb{R}\) that is a Dickman–de Bruijn function, that is, such that \(\rho(u) = 0\) for \(u < 0\), \(0 \le \rho(u) \le 1\) for \(u \ge 0\), \(\rho\) is continuous on \([0, \infty)\), \(\rho(u) = 1\) for \(0 \le u \le 1\), and for every \(u > 1\) the function \(\rho\) is differentiable at \(u\) with \(u \rho'(u) + \rho(u - 1) = 0\).

theorem existsUnique_isDickmanDeBruijn :
    ∃! ρ : ℝ → ℝ, IsDickmanDeBruijn ρ

Sources

• O. Gorodetsky, Rigidity of Averages over the Two Largest Prime Factors, which characterizes the unique continuous function on the nonnegative reals and specifies its zero extension to negative inputs; Lean packages those clauses in Real.IsDickmanDeBruijn.

Uses 1

Statement usesDickman–de Bruijn functions

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.