natural density

Stream: Is there code for X?

[Chen Ling]

Do we have definition of natural density or asymptotic density? Seems like it's not difficult, and might be related to some number theory problems. Maybe something like, prime numbers have zero density (well, it's quite trivial though).

For example:

import Mathlib

/- define auxilary density function -/
noncomputable def dens_aux (f : ℕ → ℕ) (n : ℕ) : ℝ :=
  (Set.ncard {f i | i ∈ Finset.Icc 1 n}) / n

/- define upper asymptotics density  -/
noncomputable def u_d (f : ℕ → ℕ) : ℝ :=
  Filter.limsup (dens_aux f) Filter.atTop

/- define lower asymptotics density -/
noncomputable def l_d (f : ℕ → ℕ) : ℝ :=
  Filter.liminf (dens_aux f) Filter.atTop

/- prime numbers have zero upper density  -/
theorem prime_zero_density :
  u_d (Nat.nth Nat.Prime) = 0 := by
  sorry

[Chen Ling]

sorry, a mistake. the density function should be defined as

import Mathlib

/- define auxilary density function -/
noncomputable def dens_aux (f : ℕ → ℕ) (n : ℕ) : ℝ :=
  (Set.ncard { r | r ∈ Finset.Icc 1 n ∧ ∃ i, r = f i}) / n

[Yaël Dillies]

No, we do not have it explicitly. There are many different ways to formalise it, and @Bhavik Mehta and I have been gathering thoughts over the past two years on how to formalise it best. Most recently, I have been looking into means and Foelner sequences and I believe they could make a good formalism here.

[Bhavik Mehta]

There is a formalisation of some of these in the formal conjectures project, and those originated from my earlier work on unit fractions. I think the ones in that project are reasonably good. Note we do have the schnirelmann density.