Finite average bounds and extraction of multiple witnesses

Stream: new members

[Bob Jefferson]

I'm looking for a new, finite, self-contained project. I’m considering a small Lean 4 project formalising a very common finite combinatorial pattern:

from a lower bound on the average (or sum) of a finite {0,1}-valued predicate, extract explicit structural consequences (multiple “hits”, bounded gaps, witnesses, etc.).

Before starting, I wanted to check whether the following are already in mathlib (or close variants exist):

• Finite average → ≥ k hits: for a finite nonempty set A and {0,1}-valued f,
  (∑ f) / |A| ≥ k / |A| ⇒ f = 1 at ≥ k distinct elements.

• Sum → hits: ∑ f ≥ k ⇒ existence of k distinct indices with f = 1.

• Two hits in [0,B] ⇒ bounded gap: if h₁,h₂ ∈ [0,B], then |h₁ − h₂| ≤ B (and predicate-parametric versions).

Based on recent experience, my impression is that pieces exist (pigeonhole/cardinality lemmas), but not as a small reusable toolkit for “finite density → structure” arguments.

Any pointers to existing lemmas, preferred formulations, or advice on whether packaging this would be useful would be much appreciated.