Normalized spread for indexed finite families

Definition

SunflowerIndexedSpread

by lunjia · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsspread-familiessunflower

For a finite set of labels $I$ and an indexed family $(A_i)_{i\in I}$ of finite subsets of a ground type, normalized $R$ -spread means

R^{|T|}\,|\{i\in I:T\subseteq A_i\}|\le |I|\qquad\text{for every finite }T.

Labels are counted separately, even when their members coincide. Empty members are permitted. This convention supports iterated refinement, where residual sets may become equal while their original labels remain distinct. The predicate itself imposes no sign assumption on $R$ or nonemptiness assumption on $I$ ; theorems state the conditions they require.

Definition code

import Mathlib.Data.Fintype.Card
import Mathlib.Data.Finset.Card
import Mathlib.Data.Real.Basic

set_option autoImplicit false

namespace Erdos20

/-- Spread for a uniformly sampled indexed family. Repeated members retain
their labels, so every cardinality here counts multiplicity. -/
def IndexedSpread {α ι : Type*} [DecidableEq α] [Fintype ι]
    (R : ℝ) (A : ι → Finset α) : Prop :=
  ∀ T : Finset α,
    R ^ T.card * ((Finset.univ.filter (fun i => T ⊆ A i)).card : ℝ) ≤
      Fintype.card ι

end Erdos20

Source

L. Hu, Entropy Estimation via Two Chains (19 May 2021), Definition 1 and Lemma 2, https://theorydish.blog/2021/05/19/entropy-estimation-via-two-chains-streamlining-the-proof-of-the-sunflower-lemma/ ; T. Tao, The sunflower lemma via Shannon entropy (20 July 2020), Definition 1 and refinement argument, https://terrytao.wordpress.com/2020/07/20/the-sunflower-lemma-via-shannon-entropy/ . This is an indexed, normalized-spread Bernoulli adaptation of those arguments, not a verbatim restatement of the fixed-cardinality sampling lemma.

View graph