Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Upper density

upperDensitydef

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

Used by

From Mathlib

import Conjectura.Defs.Mathematics.Combinatorics.UpperDensity · maintainer — open · raw source

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

Full credits