Skip to content

Natural and logarithmic density

12 fully proved

Densities

AbbreviationPartial density#✓fully proved

Let \(\beta\) be a preorder in which every set \(\{x \in \beta \mid x \le b\}\) is finite, let \(S, A \subseteq \beta\) and \(b \in \beta\), and write \(A_{\lt b} = \{x \in A \mid x < b\}\). The partial density of \(S\) relative to \(A\) at \(b\) is the proportion \(\lvert S \cap A_{\lt b} \rvert / \lvert A_{\lt b} \rvert\) of elements of \(A_{\lt b}\) that lie in \(S\), taken to be \(0\) when \(A_{\lt b}\) is empty. By default \(A = \beta\).

@[inline]
noncomputable abbrev partialDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot β]
    (S : Set β) (A : Set β := Set.univ) (b : β) : ℝ :=
  ((S ∩ A) ∩ Iio b).ncard / (A ∩ Iio b).ncard
Sources
  • inspired by https://github.com/b-mehta/unit-fractions
Used by 7
Used byDensity of a set · Natural density of the even numbers · Finite sets have natural density zero · Sets of nonzero natural density are infinite · Lower density · The whole order has density one · Upper density

DefinitionUpper density#✓fully proved

Let \(\beta\) be a preorder in which every set \(\{x \in \beta \mid x \le b\}\) is finite, and let \(S, A \subseteq \beta\). The upper density of \(S\) relative to \(A\) is the limit superior, as \(b \to \infty\) in \(\beta\), of the partial densities of \(S\) relative to \(A\) at \(b\). By default \(A = \beta\).

noncomputable def upperDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot β]
    (S : Set β) (A : Set β := Set.univ) : ℝ :=
  atTop.limsup fun (b : β) ↦ S.partialDensity A b
Uses 1 · Used by 3
Statement usesPartial density
Used byErdős Problem 109 (the Erdős sumset conjecture) · Erdős Problem 656 (shifted restricted sumsets in dense sets) · Erdős Problem 741, upper-density question

DefinitionLower density#✓fully proved

Let \(\beta\) be a preorder in which every set \(\{x \in \beta \mid x \le b\}\) is finite, and let \(S, A \subseteq \beta\). The lower density of \(S\) relative to \(A\) is the limit inferior, as \(b \to \infty\) in \(\beta\), of the partial densities of \(S\) relative to \(A\) at \(b\). By default \(A = \beta\).

noncomputable def lowerDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot β]
    (S : Set β) (A : Set β := Set.univ) : ℝ :=
  atTop.liminf fun (b : β) ↦ S.partialDensity A b
Uses 1 · Used by 3
Statement usesPartial density
Used byErdős Problem 851 · Erdős Problem 822 · Sign densities of the ψ-analog of the 5-core partition function

DefinitionDensity of a set#✓fully proved

Let \(\beta\) be a preorder in which every set \(\{x \in \beta \mid x \le b\}\) is finite, let \(S, A \subseteq \beta\) and \(\alpha \in \mathbb{R}\), and write \(\beta_{\lt b} = \{x \in \beta \mid x < b\}\). The set \(S\) has density \(\alpha\) relative to \(A\) if the partial density \(\lvert S \cap A \cap \beta_{\lt b} \rvert / \lvert A \cap \beta_{\lt b} \rvert\), taken to be \(0\) when the denominator is \(0\), tends to \(\alpha\) as \(b \to \infty\) in \(\beta\).

By default \(A = \beta\); for \(\beta = \mathbb{N}\) this is the natural density of \(S\).

def HasDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot β]
    (S : Set β) (α : ℝ) (A : Set β := Set.univ) : Prop :=
  Tendsto (fun (b : β) => S.partialDensity A b) atTop (𝓝 α)
Uses 1 · Used by 34
Statement usesPartial density
Used byLorentz's theorem on additive complements (Erdős Problem 31) · Zero density of A005717 modulo a prime · Zero density of A005773 modulo a prime · Density of each nonzero residue among generalized Motzkin numbers modulo \(p\) · Zero density formula for generalized Motzkin numbers modulo a prime · Generalized Motzkin numbers vanish modulo a prime with density one · Zero density of Motzkin numbers modulo a prime · Zero density of Riordan numbers modulo a prime · Zero density of shifted combinations of central trinomial coefficients · Density one for zeros of shifted combinations of central trinomial coefficients · Natural density of the even numbers · Finite sets have natural density zero · Positive density · Sets of nonzero natural density are infinite · The whole order has density one · Erdős Problem 845 · A fixed positive integer divides the divisor sum of almost every natural number · The \(k\)-th prime-factor density · Density-one zeros of constant terms modulo \(p^a\) · Density-one zeros of constant terms modulo \(p\) · Linear recurrence of combinations of constant terms modulo \(p\) · Linear recurrence of combinations of constant terms modulo \(p^a\) · Linear recurrence of constant terms modulo \(p\) · Linear recurrence of constant terms modulo \(p^a\) · Zeckendorf variation densities exist, with finite moments and mean zero · Fibonacci shifts have the same Zeckendorf variation densities as shift one · Distribution of the Zeckendorf digit-sum variation for shift one · Geometric negative tail of the Zeckendorf variation densities · Strong pseudoprime bases almost always form a subgroup · The subgroup criteria for strong pseudoprime bases hold almost always · Binomial coefficients dividing the middle binomial coefficient · Valuations of the middle binomial coefficient on a set of density one · Products of consecutive integers dividing the middle binomial coefficient · Short runs of consecutive integers have small valuations almost always

DefinitionPositive density#✓fully proved

Let \(\beta\) be a preorder in which every set \(\{x \in \beta \mid x \le b\}\) is finite, and let \(S, A \subseteq \beta\). The set \(S\) has positive density relative to \(A\) if there is a real number \(\alpha > 0\) such that \(S\) has density \(\alpha\) relative to \(A\). By default \(A = \beta\).

def HasPosDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot β]
    (S : Set β) (A : Set β := Set.univ) : Prop :=
  ∃ α > 0, S.HasDensity α A
Uses 1
Statement usesDensity of a set

DefinitionTwo-sided partial density#✓fully proved

For a set \(S\) of integers and a natural number \(N\), the two-sided partial natural density of \(S\) at \(N\) is \(\lvert S \cap [-N, N] \rvert / (2N + 1)\), where \([-N, N]\) is the set of integers \(m\) with \(-N \le m \le N\).

noncomputable def intPartialDensity (S : Set ℤ) (N : ℕ) : ℝ :=
  open scoped Classical in
  (((Finset.Icc (-(N : ℤ)) (N : ℤ)).filter (fun m => m ∈ S)).card : ℝ) /
    (2 * (N : ℝ) + 1)
Used by 1
Used byTwo-sided natural density

DefinitionTwo-sided natural density#✓fully proved

A set \(S\) of integers has two-sided natural density \(\alpha \in \mathbb{R}\) if \(\lvert S \cap [-N, N] \rvert / (2N + 1)\) tends to \(\alpha\) as the natural number \(N\) tends to infinity, where \([-N, N]\) is the set of integers \(m\) with \(-N \le m \le N\).

def HasIntDensity (S : Set ℤ) (α : ℝ) : Prop :=
  Tendsto (fun N : ℕ => S.intPartialDensity N) atTop (𝓝 α)
Uses 1
Statement usesTwo-sided partial density

Has Density

TheoremThe whole order has density one#✓fully proved

Let \(\beta\) be a partial order with a least element and at least two elements, in which every closed interval \([a, b]\) is finite. Then the set of all elements of \(\beta\) has density \(1\) (relative to all of \(\beta\)).

@[simp]
theorem univ {β : Type*} [PartialOrder β] [LocallyFiniteOrder β] [OrderBot β] [Nontrivial β] :
    (@Set.univ β).HasDensity 1
Uses 2
Statement usesDensity of a set
Proof usesPartial density

Basic properties of natural density

TheoremNatural density of the even numbers#✓fully proved

The set of even natural numbers has natural density \(1/2\).

theorem hasDensity_even : {n : ℕ | Even n}.HasDensity (1 / 2)
Uses 2
Statement usesDensity of a set
Proof usesPartial density

TheoremFinite sets have natural density zero#✓fully proved

Every finite set of natural numbers has natural density \(0\).

theorem hasDensity_zero_of_finite {S : Set ℕ} (h : S.Finite) : S.HasDensity 0
Uses 2 · Used by 1
Statement usesDensity of a set
Proof usesPartial density
Used bySets of nonzero natural density are infinite

TheoremSets of nonzero natural density are infinite#✓fully proved

If a set \(S\) of natural numbers has natural density \(\alpha\) with \(\alpha \neq 0\), then \(S\) is infinite.

theorem infinite_of_hasDensity_pos {S : Set ℕ} {α : ℝ} (h : S.HasDensity α) (hα : α ≠ 0) :
    S.Infinite
Uses 3
Statement usesDensity of a set
Proof usesFinite sets have natural density zero · Partial density

Has Density

DefinitionLogarithmic density#✓fully proved

A set \(A\) of natural numbers has logarithmic density \(d \in \mathbb{R}\) if \(\frac{1}{\log n} \sum_{k \in A,\, k \le n} \frac{1}{k}\) tends to \(d\) as \(n \to \infty\), where \(\log\) is the natural logarithm, the term \(1/k\) for \(k = 0\) is taken to be \(0\), and the whole expression is taken to be \(0\) when \(\log n = 0\).

Logarithmic density is a weaker notion than natural density: if a set has natural density \(d\), then it also has logarithmic density \(d\), but the converse is false.

def Set.HasLogDensity (A : Set ℕ) (d : ℝ) : Prop :=
  open scoped Classical in
  Tendsto (fun n : ℕ => (∑ k ≤ n with k ∈ A, (k : ℝ)⁻¹ / .log n : ℝ)) atTop (𝓝 d)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.