Unrestricted depth-three lower bound: sunflower

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/Sunflower.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

def Complexity.DepthThreeLowerBound.Sunflower {α : Type uDepth1} [DecidableEq α] (family : Finset (Finset α)) (core : Finset α) : Prop

A finite family whose pairwise intersections are its common core.

Equations

• Complexity.DepthThreeLowerBound.Sunflower family core = ∀ A ∈ family, ∀ B ∈ family, A ≠ B → A ∩ B = core

theorem Complexity.DepthThreeLowerBound.Sunflower.mono {α : Type uDepth1} [DecidableEq α] {family : Finset (Finset α)} {core : Finset α} (h : Sunflower family core) {sub : Finset (Finset α)} (hsub : sub ⊆ family) : Sunflower sub core

theorem Complexity.DepthThreeLowerBound.Sunflower.core_subset {α : Type uDepth1} [DecidableEq α] {family : Finset (Finset α)} {core A : Finset α} (h : Sunflower family core) (hcard : 2 ≤ family.card) (hA : A ∈ family) : core ⊆ A

theorem Complexity.DepthThreeLowerBound.Sunflower.core_card_lt {α : Type uDepth1} [DecidableEq α] {family : Finset (Finset α)} {core : Finset α} {i : ℕ} (h : Sunflower family core) (hcard : 2 ≤ family.card) (uniform : ∀ A ∈ family, A.card = i) : core.card < i

theorem Complexity.DepthThreeLowerBound.Sunflower.petal_card {α : Type uDepth1} [DecidableEq α] {family : Finset (Finset α)} {core A : Finset α} {i : ℕ} (h : Sunflower family core) (hcard : 2 ≤ family.card) (uniform : ∀ A ∈ family, A.card = i) (hA : A ∈ family) : (A \ core).card = i - core.card

theorem Complexity.DepthThreeLowerBound.Sunflower.petal_nonempty {α : Type uDepth1} [DecidableEq α] {family : Finset (Finset α)} {core A : Finset α} {i : ℕ} (h : Sunflower family core) (hcard : 2 ≤ family.card) (uniform : ∀ A ∈ family, A.card = i) (hA : A ∈ family) : (A \ core).Nonempty

theorem Complexity.DepthThreeLowerBound.Sunflower.petal_card_lt {α : Type uDepth1} [DecidableEq α] {family : Finset (Finset α)} {core A : Finset α} {i : ℕ} (h : Sunflower family core) (hcard : 2 ≤ family.card) (uniform : ∀ A ∈ family, A.card = i) (hc : core.Nonempty) (hA : A ∈ family) : (A \ core).card < i

theorem Complexity.DepthThreeLowerBound.Sunflower.petals_disjoint {α : Type uDepth1} [DecidableEq α] {family : Finset (Finset α)} {core A B : Finset α} (h : Sunflower family core) (hA : A ∈ family) (hB : B ∈ family) (hne : A ≠ B) : Disjoint (A \ core) (B \ core)

theorem Complexity.DepthThreeLowerBound.Sunflower.petal_injective {α : Type uDepth1} [DecidableEq α] {family : Finset (Finset α)} {core : Finset α} (h : Sunflower family core) (hcard : 2 ≤ family.card) : Set.InjOn (fun (A : Finset α) => A \ core) ↑family

theorem Complexity.DepthThreeLowerBound.Sunflower.card_petals {α : Type uDepth1} [DecidableEq α] {family : Finset (Finset α)} {core : Finset α} (h : Sunflower family core) (hcard : 2 ≤ family.card) : (Finset.image (fun (A : Finset α) => A \ core) family).card = family.card

def Complexity.DepthThreeLowerBound.eraseContaining {α : Type uDepth1} [DecidableEq α] (family : Finset (Finset α)) (x : α) : Finset (Finset α)

Remove a selected element from the sets that contain it.

Equations

• Complexity.DepthThreeLowerBound.eraseContaining family x = Finset.image (fun (A : Finset α) => A.erase x) ({A ∈ family | x ∈ A})

theorem Complexity.DepthThreeLowerBound.finite_uniform_sunflower {α : Type uDepth1} [DecidableEq α] (family : Finset (Finset α)) (s r : ℕ) (hr : 2 ≤ r) (uniform : ∀ A ∈ family, A.card = s) (large : s.factorial * (r - 1) ^ s < family.card) : ∃ sub ⊆ family, sub.card = r ∧ ∃ (core : Finset α), Sunflower sub core

theorem Complexity.DepthThreeLowerBound.no_nonempty_core_sunflower_occurrence_le {α : Type uDepth1} [DecidableEq α] (family : Finset (Finset α)) (i r : ℕ) (hr : 2 ≤ r) (uniform : ∀ A ∈ family, A.card = i + 1) (hno : ∀ sub ⊆ family, sub.card = r → ∀ (core : Finset α), core.Nonempty → ¬Sunflower sub core) (x : α) : {A ∈ family | x ∈ A}.card ≤ i.factorial * (r - 1) ^ i