Upper density

Conjectura.Defs.Mathematics.Combinatorics.UpperDensity

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Order.Filter.AtTopBot.Defs
import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Data.Set.Card

/-! # Upper density -/

namespace Conjectura.Combinatorics

open Filter

/-- The **upper density** of a set of naturals is the limit superior of the proportion of
`{0, …, n-1}` it occupies. Positive upper density is the hypothesis in Szemerédi's theorem. -/
noncomputable def upperDensity (S : Set ℕ) : ℝ :=
  limsup (fun n : ℕ => ((Set.Iio n ∩ S).ncard : ℝ) / (n : ℝ)) atTop

end Conjectura.Combinatorics