A density version of a theorem of Banach

David A. Ross

Code by ChatGPT, mostly.

def count_le (I : ℕ → Prop) [DecidablePred I] (n : ℕ) : ℕ

Equations

• count_le I n = (Finset.filter (fun (k : ℕ) => I k) (Finset.range (n + 1))).card

noncomputable def density_seq (I : ℕ → Prop) [DecidablePred I] (n : ℕ) : ℝ

Equations

• density_seq I n = ↑(count_le I n) / (↑n + 1)

noncomputable def upper_density (I : ℕ → Prop) [DecidablePred I] : ℝ

Equations

• upper_density I = Filter.limsup (density_seq I) Filter.atTop