@[reducible, inline]

noncomputable abbrev Set.partialDensity {β : Type u_1} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := univ) (b : β) : ℝ

Given a set S and an element b in an order β, where all intervals bounded above are finite, we define the partial density of S (relative to a set A) to be the proportion of elements in {x ∈ A | x < b} that lie in S ∩ A.

This definition was inspired from https://github.com/b-mehta/unit-fractions

Equations

• S.partialDensity A b = ↑((S ∩ A).interIio b).ncard / ↑(A.interIio b).ncard

theorem Set.partialDensity_le_one {β : Type u_1} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := univ) (b : β) : S.partialDensity A b ≤ 1

noncomputable def Set.upperDensity {β : Type u_1} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := univ) : ℝ

Given a set S in an order β, where all intervals bounded above are finite, we define the upper density of S (relative to a set A) to be the limsup of the partial densities of S (relative to A) for b → ∞.

Equations

• S.upperDensity A = Filter.limsup (fun (b : β) => S.partialDensity A b) Filter.atTop

noncomputable def Set.lowerDensity {β : Type u_1} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := univ) : ℝ

Given a set S in an order β, where all intervals bounded above are finite, we define the lower density of S (relative to a set A) to be the liminf of the partial densities of S (relative to A) for b → ∞.

Equations

• S.lowerDensity A = Filter.liminf (fun (b : β) => S.partialDensity A b) Filter.atTop

theorem Set.lowerDensity_le_one {β : Type u_1} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := univ) : S.lowerDensity A ≤ 1

theorem Set.lowerDensity_nonneg {β : Type u_1} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := univ) : 0 ≤ S.lowerDensity A

def Set.HasDensity {β : Type u_1} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (α : ℝ) (A : Set β := univ) : Prop

A set S in an order β where all intervals bounded above are finite is said to have density α : ℝ (relative to a set A) if the proportion of x ∈ S such that x < n in A tends to α as n → ∞.

When β = ℕ this by default defines the natural density of a set (i.e., relative to all of ℕ).

Equations

• S.HasDensity α A = Filter.Tendsto (fun (b : β) => S.partialDensity A b) Filter.atTop (nhds α)

def Set.HasPosDensity {β : Type u_1} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := univ) : Prop

A set S in an order β where all intervals bounded above are finite is said to have positive density (relative to a set A) if there exists a positive α : ℝ such that S has density α (relative to a set A).

Equations

• S.HasPosDensity A = ∃ α > 0, S.HasDensity α A

@[simp]

theorem Set.HasDensity.univ {β : Type u_1} [PartialOrder β] [LocallyFiniteOrder β] [OrderBot β] [Nontrivial β] : Set.univ.HasDensity 1

In a non-trivial partial order with a least element, the set of all elements has density one.

theorem Set.HasDensity.univ_nat_hasDensity_one : Set.univ.HasDensity 1

@[simp]

theorem Set.HasDensity.empty {β : Type u_1} [Preorder β] [LocallyFiniteOrderBot β] (A : Set β := Set.univ) : ∅.HasDensity 0 A

theorem Set.HasDensity.mono {β : Type u_1} [PartialOrder β] [LocallyFiniteOrder β] [OrderBot β] {S T : Set β} {αS αT : ℝ} [Filter.atTop.NeBot] (h : S ⊆ T) (hS : S.HasDensity αS) (hT : T.HasDensity αT) : αS ≤ αT

theorem Set.HasDensity.nonneg {β : Type u_1} [Preorder β] [LocallyFiniteOrderBot β] [Filter.atTop.NeBot] {S : Set β} {α : ℝ} (h : S.HasDensity α) : 0 ≤ α

theorem Nat.hasDensity_even : {n : ℕ | Even n}.HasDensity (1 / 2)

The natural density of the set of even numbers is 1 / 2.

theorem Nat.hasDensity_zero_of_finite {S : Set ℕ} (h : S.Finite) : S.HasDensity 0

A finite set has natural density zero.

theorem Nat.infinite_of_hasDensity_pos {S : Set ℕ} {α : ℝ} (h : S.HasDensity α) (hα : 0 < α) : S.Infinite

A set of positive natural density is infinite.