Improved bounds for the sunflower lemma | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: R. Alweiss, S. Lovett, K. Wu, and J. Zhang, `Improved bounds for the sunflower lemma`, Annals of Math, 194 (3) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2021-194-3-ImprovedBoundsSunflowerLemma.lean

Informal solution: Unavailable.

/-- The absolute constant `C` in Theorem 1.4. Although not explicitly stated in the paper,
the constant `C` doesn't depend on `r`. -/
noncomputable def declaration uses `sorry`C : ℝ := sorry

/--
Statement of Theorem 1.4 (Main theorem, sunflowers):

Let `r ≥ 3`. For some constant `C`, any `w`-set system `F` of size
`|F| ≥ (C * r ^ 3 * log w * log log w) ^ w` contains an `r`-sunflower.

Note: We require `w ≥ 2`, as the paper assumes `log log w > 0`.
-/
theorem declaration uses `sorry`theorem_1_4 (r : ℕ) (hr : r ≥ 3) (X : Type*) [Finite X] (ℱ : Set (Set X)) (w : ℕ)
      (hw : w ≥ 2) (hℱ₁ : ℱ.IsSystem w) (hℱ₂ : ℱ.ncard ≥ lowerBound r C w) :
      ∃ S ⊆ ℱ, S.IsSunflower r := byr:ℕhr:r ≥ 3X:Type u_1inst✝:Finite Xℱ:Set (Set X)w:ℕhw:w ≥ 2hℱ₁:Set.IsSystem w ℱhℱ₂:↑ℱ.ncard ≥ lowerBound r C w⊢ ∃ S ⊆ ℱ, Set.IsSunflower r S
  sorryAll goals completed! 🐙