Prove2Me

Logarithmic spread guarantees disjoint petals

Proved
Erdos20.spread_disjoint_bound

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

combinatoricsprobabilityspread-familiessunflower

There is an absolute constant C≥4C\ge4 such that the following holds for integers n,k≥2n,k\ge2. Let F\mathcal F be a nonempty finite family of nonempty finite sets, each of size at most nn. If F\mathcal F is normalized RR-spread for R=Cklog⁡nR=Ck\log n, meaning

R∣T∣ ∣{A∈F:T⊆A}∣≤∣F∣for every finite T,R^{|T|}\,|\{A\in\mathcal F:T\subseteq A\}|\le|\mathcal F|\quad\text{for every finite }T,

then it contains a subfamily H\mathcal H with

∣H∣=k,A∩B=∅for distinct A,B∈H.|\mathcal H|=k,\qquad A\cap B=\varnothing\quad\text{for distinct }A,B\in\mathcal H.

This is the probabilistic disjoint-petals component of the logarithmic sunflower argument, formulated for bounded rank and normalized spread. Nonempty members ensure that petals chosen in different color classes are distinct. Logarithms are natural.

Source formulation. This is a bounded-rank normalized-spread adaptation, not a verbatim restatement of Bell–Chueluecha–Warnke Lemma 2, whose spread convention uses an absolute degree bound for uniform families. The stated form combines the normalized-spread refinement/iteration in Hu and Tao with the 2k2k-color expectation step in Bell–Chueluecha–Warnke. It is left as an open child of the milestone reduction.

Preamble
import Definitions.Def_SunflowerSpread
import Mathlib.Analysis.SpecialFunctions.Log.Basic
Formal statement
namespace Erdos20
theorem spread_disjoint_bound :
    ∃ C : ℝ, 4 ≤ C ∧ ∀ (n k : ℕ), 2 ≤ n → 2 ≤ k →
      ∀ {α : Type} [DecidableEq α] (F : Finset (Finset α)),
        F.Nonempty → (∀ A ∈ F, A.Nonempty ∧ A.card ≤ n) →
        IsSpread (C * k * Real.log n) F →
        ∃ H ⊆ F, H.card = k ∧
          ∀ A ∈ H, ∀ B ∈ H, A ≠ B → Disjoint A B := by
  sorry

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 (2020), Definition 1 and Propositions 5–6 (iteration), https://terrytao.wordpress.com/2020/07/20/the-sunflower-lemma-via-shannon-entropy/ ; T. Bell, S. Chueluecha, L. Warnke, Note on Sunflowers, arXiv:2009.09327v2, proof of Lemma 2 (2k-color expectation step), https://arxiv.org/html/2009.09327v2 . Bounded-rank normalized-spread adaptation explicitly described in the statement.

View graph