1. FormalConjecturesForMathlib
  2. Data
  3. Set
  4. Density
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import Mathlib.Analysis.SpecialFunctions.Log.Basic public import FormalConjecturesForMathlib.Algebra.Order.Group.Pointwise.Interval public import FormalConjecturesForMathlib.Data.Set.Interval public import FormalConjecturesForMathlib.Order.Interval.Finset.Basic public import FormalConjecturesForMathlib.Order.Interval.Finset.Nat public import Batteries.Util.ProofWanted public import Mathlib.Tactic@[expose] public sectionopen Filteropen scoped Topologynamespace Set

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

@[inline] noncomputable abbrev partialDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := Set.univ) (b : β) : ℝ := ((S ∩ A) ∩ Iio b).ncard / (A ∩ Iio b).ncardtheorem partialDensity_le_one {β : Type*} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := Set.univ) (b : β) : S.partialDensity A b ≤ 1 := β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set βb:β⊢ S.partialDensity A b ≤ 1 β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set βb:β⊢ ↑(S ∩ A ∩ Iio b).ncard ≤ ↑(A ∩ Iio b).ncard All goals completed! 🐙

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 → ∞.

noncomputable def upperDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := Set.univ) : ℝ := atTop.limsup fun (b : β) ↦ S.partialDensity A b

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 → ∞.

noncomputable def lowerDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := Set.univ) : ℝ := atTop.liminf fun (b : β) ↦ S.partialDensity A btheorem lowerDensity_le_one {β : Type*} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := Set.univ) : S.lowerDensity A ≤ 1 := β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set β⊢ S.lowerDensity A ≤ 1 β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set βh:atTop = ⊥⊢ S.lowerDensity A ≤ 1β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set βh:¬atTop = ⊥⊢ S.lowerDensity A ≤ 1 β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set βh:atTop = ⊥⊢ S.lowerDensity A ≤ 1 All goals completed! 🐙 β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set βh:¬atTop = ⊥⊢ S.lowerDensity A ≤ 1 β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set βh:¬atTop = ⊥this:atTop.NeBot⊢ S.lowerDensity A ≤ 1 β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set βh:¬atTop = ⊥this:atTop.NeBotx:ℝhx:x ∈ {a | ∀ᶠ (n : ℝ) in map (fun b ↦ S.partialDensity A b) atTop, a ≤ n}⊢ x ≤ 1 All goals completed! 🐙β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set β⊢ 0 ≤ sSup {a | ∀ᶠ (n : β) in atTop, a ≤ S.partialDensity A n} exact (em _).elim (le_csSup · <| .of_forall fun _ ↦ β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βS:Set βA:Set β⊢ 0 ≤ S.lowerDensity A All goals completed! 🐙) (Real.sSup_of_not_bddAbove · |>.ge)

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 ℕ).

def HasDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (α : ℝ) (A : Set β := Set.univ) : Prop := Tendsto (fun (b : β) => S.partialDensity A b) atTop (𝓝 α)

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).

def HasPosDensity {β : Type*} [Preorder β] [LocallyFiniteOrderBot β] (S : Set β) (A : Set β := Set.univ) : Prop := ∃ α > 0, S.HasDensity α A

The two-sided partial natural density of a set of integers, counted inside the interval [-N, N].

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

A set of integers has two-sided natural density α.

def HasIntDensity (S : Set ℤ) (α : ℝ) : Prop := Tendsto (fun N : ℕ => S.intPartialDensity N) atTop (𝓝 α)@[simp] theorem intPartialDensity_empty (N : ℕ) : intPartialDensity (∅ : Set ℤ) N = 0 := N:ℕ⊢ ∅.intPartialDensity N = 0 All goals completed! 🐙namespace HasIntDensity@[simp] theorem empty : HasIntDensity (∅ : Set ℤ) 0 := ⊢ ∅.HasIntDensity 0 All goals completed! 🐙end HasIntDensitynamespace HasDensity

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

@[simp] theorem univ {β : Type*} [PartialOrder β] [LocallyFiniteOrder β] [OrderBot β] [Nontrivial β] : (@Set.univ β).HasDensity 1 := β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βinst✝:Nontrivial β⊢ Set.univ.HasDensity 1 β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βinst✝:Nontrivial βh:atTop = ⊥⊢ Set.univ.HasDensity 1β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βinst✝:Nontrivial βh:¬atTop = ⊥⊢ Set.univ.HasDensity 1 β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βinst✝:Nontrivial βh:atTop = ⊥⊢ Set.univ.HasDensity 1 All goals completed! 🐙 β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βinst✝:Nontrivial βh:¬atTop = ⊥⊢ Set.univ.HasDensity 1 β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βinst✝:Nontrivial βh:¬atTop = ⊥⊢ Tendsto (fun b ↦ ↑(Iio b).ncard / ↑(Iio b).ncard) atTop (𝓝 1) β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βinst✝:Nontrivial βh:¬atTop = ⊥b:βhb:∀ n ≥ b, (Iio n).ncard ≠ 0⊢ Tendsto (fun b ↦ ↑(Iio b).ncard / ↑(Iio b).ncard) atTop (𝓝 1) β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βinst✝:Nontrivial βh:¬atTop = ⊥b:βhb:∀ n ≥ b, (Iio n).ncard ≠ 0⊢ (fun x ↦ 1) =ᶠ[atTop] fun b ↦ ↑(Iio b).ncard / ↑(Iio b).ncard All goals completed! 🐙theorem univ_nat_hasDensity_one : (@Set.univ ℕ).HasDensity 1 := univ@[simp] theorem empty {β : Type*} [Preorder β] [LocallyFiniteOrderBot β] (A : Set β := Set.univ) : Set.HasDensity (∅ : Set β) 0 A := β:Type u_1inst✝¹:Preorder βinst✝:LocallyFiniteOrderBot βA:Set β⊢ ∅.HasDensity 0 A All goals completed! 🐙β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βS:Set βT:Set βαS:ℝαT:ℝinst✝:atTop.NeBoth:S ⊆ ThS:Tendsto (fun b ↦ S.partialDensity Set.univ b) atTop (𝓝 αS)hT:Tendsto (fun b ↦ T.partialDensity Set.univ b) atTop (𝓝 αT)⊢ αS ≤ αT β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βS:Set βT:Set βαS:ℝαT:ℝinst✝:atTop.NeBoth:S ⊆ ThS:Tendsto (fun b ↦ S.partialDensity Set.univ b) atTop (𝓝 αS)hT:Tendsto (fun b ↦ T.partialDensity Set.univ b) atTop (𝓝 αT)⊢ (fun b ↦ S.partialDensity Set.univ b) ≤ᶠ[atTop] fun b ↦ T.partialDensity Set.univ b filter_upwards [eventually_ge_atTop ⊥] with b β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βS:Set βT:Set βαS:ℝαT:ℝinst✝:atTop.NeBoth:S ⊆ ThS:Tendsto (fun b ↦ S.partialDensity Set.univ b) atTop (𝓝 αS)hT:Tendsto (fun b ↦ T.partialDensity Set.univ b) atTop (𝓝 αT)b:βhb:⊥ ≤ b⊢ S.partialDensity Set.univ b ≤ T.partialDensity Set.univ b β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βS:Set βT:Set βαS:ℝαT:ℝinst✝:atTop.NeBoth:S ⊆ ThS:Tendsto (fun b ↦ S.partialDensity Set.univ b) atTop (𝓝 αS)hT:Tendsto (fun b ↦ T.partialDensity Set.univ b) atTop (𝓝 αT)b:βhb:⊥ ≤ b⊢ ↑(S ∩ Set.univ ∩ Iio b).ncard ≤ ↑(T ∩ Set.univ ∩ Iio b).ncardβ:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βS:Set βT:Set βαS:ℝαT:ℝinst✝:atTop.NeBoth:S ⊆ ThS:Tendsto (fun b ↦ S.partialDensity Set.univ b) atTop (𝓝 αS)hT:Tendsto (fun b ↦ T.partialDensity Set.univ b) atTop (𝓝 αT)b:βhb:⊥ ≤ b⊢ 0 ≤ ↑(Set.univ ∩ Iio b).ncard grw [β:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βS:Set βT:Set βαS:ℝαT:ℝinst✝:atTop.NeBoth:S ⊆ ThS:Tendsto (fun b ↦ S.partialDensity Set.univ b) atTop (𝓝 αS)hT:Tendsto (fun b ↦ T.partialDensity Set.univ b) atTop (𝓝 αT)b:βhb:⊥ ≤ b⊢ ↑(T ∩ Set.univ ∩ Iio b).ncard ≤ ↑(T ∩ Set.univ ∩ Iio b).ncardβ:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βS:Set βT:Set βαS:ℝαT:ℝinst✝:atTop.NeBoth:S ⊆ ThS:Tendsto (fun b ↦ S.partialDensity Set.univ b) atTop (𝓝 αS)hT:Tendsto (fun b ↦ T.partialDensity Set.univ b) atTop (𝓝 αT)b:βhb:⊥ ≤ b⊢ 0 ≤ ↑(Set.univ ∩ Iio b).ncardβ:Type u_1inst✝³:PartialOrder βinst✝²:LocallyFiniteOrder βinst✝¹:OrderBot βS:Set βT:Set βαS:ℝαT:ℝinst✝:atTop.NeBoth:S ⊆ ThS:Tendsto (fun b ↦ S.partialDensity Set.univ b) atTop (𝓝 αS)hT:Tendsto (fun b ↦ T.partialDensity Set.univ b) atTop (𝓝 αT)b:βhb:⊥ ≤ b⊢ 0 ≤ ↑(Set.univ ∩ Iio b).ncard All goals completed! 🐙theorem nonneg {β : Type*} [Preorder β] [LocallyFiniteOrderBot β] [(atTop : Filter β).NeBot] {S : Set β} {α : ℝ} (h : S.HasDensity α) : 0 ≤ α := le_of_tendsto_of_tendsto' empty h fun b => β:Type u_1inst✝²:Preorder βinst✝¹:LocallyFiniteOrderBot βinst✝:atTop.NeBotS:Set βα:ℝh:S.HasDensity αb:β⊢ ∅.partialDensity Set.univ b ≤ S.partialDensity Set.univ b All goals completed! 🐙end Set.HasDensitynamespace Natopen Set

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

h:Tendsto (fun k ↦ 1 + 1 / ↑k) atTop (𝓝 1)⊢ Tendsto (fun n ↦ (↑n + 1) / ↑n * 2⁻¹) atTop (𝓝 2⁻¹) simpa using Tendsto.mul_const _ <| Tendsto.congr' (eventually_atTop.2 ⟨1, fun k hk => h:Tendsto (fun k ↦ 1 + 1 / ↑k) atTop (𝓝 1)k:ℕhk:1 ≤ k⊢ 1 + 1 / ↑k = (↑k + 1) / ↑k All goals completed! 🐙⟩) h

A finite set has natural density zero.

S:Set ℕh:S.Finitethis:∀ (n : ℕ), ↑(S ∩ Iio n).ncard / ↑n ≤ ↑S.ncard / ↑n⊢ Tendsto (fun b ↦ ↑(S ∩ Iio b).ncard / ↑b) atTop (𝓝 0) All goals completed! 🐙

A set of positive natural density is infinite.

theorem infinite_of_hasDensity_pos {S : Set ℕ} {α : ℝ} (h : S.HasDensity α) (hα : α ≠ 0) : S.Infinite := mt hasDensity_zero_of_finite fun h' => hα (tendsto_nhds_unique h h')end Nat

Logarithmic Density

section LogarithmicDensityopen Finset Real

A set A of natural numbers has logarithmic density d if the sequence $(1 / \log n) \cdot \sum_{k \in A, k \le n} (1/k)$ converges to d. Logarithmic density is a weaker notion than natural density: if a set has natural density d, then it also has logarithmic density d (see Set.HasDensity.hasLogDensity), 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)

If a set has natural density d, then it also has logarithmic density d.

proof_wanted Set.HasDensity.hasLogDensity {A : Set ℕ} {d : ℝ} (h : A.HasDensity d) : A.HasLogDensity dend LogarithmicDensity