Unrestricted depth-three lower bound: tuple counting

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

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

def Complexity.DepthThreeLowerBound.TupleNoSingleton {Z : Type uDepth1} [DecidableEq Z] {n : ℕ} (a : Fin n → Z) : Prop

Every value occurring in the tuple occurs at least twice.

Equations

• Complexity.DepthThreeLowerBound.TupleNoSingleton a = ∀ (z : Z), {i : Fin n | a i = z}.card ≠ 1

theorem Complexity.DepthThreeLowerBound.tuple_singleton_of_not {Z : Type uDepth2} [DecidableEq Z] {n : ℕ} (a : Fin n → Z) (h : ¬TupleNoSingleton a) : ∃ (i₀ : Fin n), ∀ (i : Fin n), a i = a i₀ → i = i₀

theorem Complexity.DepthThreeLowerBound.tuple_support_card_le_half {Z : Type uDepth3} [DecidableEq Z] (h : ℕ) (a : Fin (2 * h) → Z) (hns : TupleNoSingleton a) : (Finset.image a Finset.univ).card ≤ h

theorem Complexity.DepthThreeLowerBound.tuple_factor_through {Z : Type uDepth4} [Nonempty Z] [DecidableEq Z] {n h : ℕ} (a : Fin n → Z) (hcard : (Finset.image a Finset.univ).card ≤ h) : ∃ (f : Fin h → Z) (g : Fin n → Fin h), (fun (i : Fin n) => f (g i)) = a

theorem Complexity.DepthThreeLowerBound.card_noSingleton_tuples_le {Z : Type uDepth5} [Fintype Z] [Nonempty Z] [DecidableEq Z] (h : ℕ) : {a : Fin (2 * h) → Z | TupleNoSingleton a}.card ≤ Fintype.card Z ^ h * h ^ (2 * h)