Unrestricted depth-three lower bound: sparse finite family

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

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

noncomputable def Complexity.DepthThreeLowerBound.sparseMinimalFamily {α : Type uDepth1} (A : Finset (Finset α)) : Finset (Finset α)

The finite family of minimal sparse CNFs used as tests.

Equations

• Complexity.DepthThreeLowerBound.sparseMinimalFamily A = {C ∈ A | ∀ D ∈ A, D ⊆ C → C ⊆ D}

theorem Complexity.DepthThreeLowerBound.mem_sparseMinimalFamily {α : Type uDepth1} {A : Finset (Finset α)} {C : Finset α} : C ∈ sparseMinimalFamily A ↔ C ∈ A ∧ ∀ D ∈ A, D ⊆ C → C ⊆ D

theorem Complexity.DepthThreeLowerBound.sparseMinimalFamily_subset {α : Type uDepth1} (A : Finset (Finset α)) : sparseMinimalFamily A ⊆ A

theorem Complexity.DepthThreeLowerBound.sparseMinimalFamily_antichain {α : Type uDepth1} (A : Finset (Finset α)) (C : Finset α) : C ∈ sparseMinimalFamily A → ∀ D ∈ sparseMinimalFamily A, C ⊆ D → C = D

theorem Complexity.DepthThreeLowerBound.exists_mem_sparseMinimalFamily_subset {α : Type uDepth1} {A : Finset (Finset α)} {C : Finset α} (hC : C ∈ A) : ∃ D ∈ sparseMinimalFamily A, D ⊆ C

theorem Complexity.DepthThreeLowerBound.forall_sparseMinimalFamily_iff {α : Type uDepth1} (A : Finset (Finset α)) (P : Finset α → Prop) (hP : ∀ {C D : Finset α}, C ⊆ D → P C → P D) : (∀ C ∈ sparseMinimalFamily A, P C) ↔ ∀ C ∈ A, P C

theorem Complexity.DepthThreeLowerBound.sparseMinimalFamily_empty {α : Type uDepth1} : sparseMinimalFamily ∅ = ∅