Unrestricted depth-three lower bound: sparse streams

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

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

inductive Complexity.DepthThreeLowerBound.SparseDecisionTree (Label : Type uDepth1) : Type uDepth1

The binary decision tree recording a sparsification process.

• leaf {Label : Type uDepth1} : SparseDecisionTree Label
• node {Label : Type uDepth1} : Label → SparseDecisionTree Label → SparseDecisionTree Label → SparseDecisionTree Label

def Complexity.DepthThreeLowerBound.SparseDecisionTree.Leaf {Label : Type uDepth2} : SparseDecisionTree Label → Type

Leaves of the sparsification decision tree.

Equations

• Complexity.DepthThreeLowerBound.SparseDecisionTree.leaf.Leaf = Unit
• (Complexity.DepthThreeLowerBound.SparseDecisionTree.node a l r).Leaf = (l.Leaf ⊕ r.Leaf)

@[instance_reducible]

def Complexity.DepthThreeLowerBound.SparseDecisionTree.leafFintype {Label : Type uDepth2} (t : SparseDecisionTree Label) : Fintype t.Leaf

The finite enumeration of a sparsification tree's leaves.

Equations

• Complexity.DepthThreeLowerBound.SparseDecisionTree.leaf.leafFintype = { elems := Complexity.DepthThreeLowerBound.SparseDecisionTree.leafFintype._aux_1, complete := ⋯ }
• (Complexity.DepthThreeLowerBound.SparseDecisionTree.node a l r).leafFintype = id inferInstance

@[instance_reducible]

instance Complexity.DepthThreeLowerBound.SparseDecisionTree.instFintypeLeaf {Label : Type uDepth2} (t : SparseDecisionTree Label) : Fintype t.Leaf

Equations

• t.instFintypeLeaf = t.leafFintype

def Complexity.DepthThreeLowerBound.SparseDecisionTree.stream {Label : Type uDepth2} [DecidableEq Label] (t : SparseDecisionTree Label) : t.Leaf → Label → List Bool

The sequence of branch choices leading to a leaf.

Equations

• Complexity.DepthThreeLowerBound.SparseDecisionTree.leaf.stream x_3 x✝ = []
• (Complexity.DepthThreeLowerBound.SparseDecisionTree.node a l a_1).stream (Sum.inl p) x✝ = if x✝ = a then false :: l.stream p x✝ else l.stream p x✝
• (Complexity.DepthThreeLowerBound.SparseDecisionTree.node a a_1 r).stream (Sum.inr p) x✝ = if x✝ = a then true :: r.stream p x✝ else r.stream p x✝

def Complexity.DepthThreeLowerBound.SparseDecisionTree.streamBit {Label : Type uDepth2} [DecidableEq Label] (t : SparseDecisionTree Label) (p : t.Leaf) (i : Label) (k : ℕ) : Bool

Read a branch bit from a leaf's choice stream.

Equations

• t.streamBit p i k = (t.stream p i).getD k false

def Complexity.DepthThreeLowerBound.SparseDecisionTree.padded {Label : Type uDepth2} [DecidableEq Label] (t : SparseDecisionTree Label) (N : Label → ℕ) (p : t.Leaf) (i : Label) (k : Fin (N i)) : Bool

Pad a leaf's choice stream to the specified common length.

Equations

• t.padded N p i k = t.streamBit p i ↑k

theorem Complexity.DepthThreeLowerBound.SparseDecisionTree.streamBit_injective {Label : Type uDepth2} [DecidableEq Label] (t : SparseDecisionTree Label) : Function.Injective t.streamBit

theorem Complexity.DepthThreeLowerBound.SparseDecisionTree.padded_injective {Label : Type uDepth2} [DecidableEq Label] (t : SparseDecisionTree Label) (N : Label → ℕ) (hN : ∀ (p : t.Leaf) (i : Label), (t.stream p i).length ≤ N i) : Function.Injective (t.padded N)

theorem Complexity.DepthThreeLowerBound.SparseDecisionTree.trueCount_getD (xs : List Bool) (N : ℕ) (h : xs.length ≤ N) : (trueCount fun (j : Fin N) => xs.getD (↑j) false) = List.count true xs

theorem Complexity.DepthThreeLowerBound.SparseDecisionTree.padded_trueCount {Label : Type uDepth2} [DecidableEq Label] (t : SparseDecisionTree Label) (N : Label → ℕ) (p : t.Leaf) (i : Label) (h : (t.stream p i).length ≤ N i) : trueCount (t.padded N p i) = List.count true (t.stream p i)

theorem Complexity.DepthThreeLowerBound.SparseDecisionTree.card_le_prod_admitted {Label : Type uDepth2} [DecidableEq Label] [Fintype Label] (t : SparseDecisionTree Label) (N : Label → ℕ) (hN : ∀ (p : t.Leaf) (i : Label), (t.stream p i).length ≤ N i) (admitted : (i : Label) → Finset (Fin (N i) → Bool)) (hmem : ∀ (p : t.Leaf) (i : Label), t.padded N p i ∈ admitted i) : Fintype.card t.Leaf ≤ ∏ i : Label, (admitted i).card

theorem Complexity.DepthThreeLowerBound.SparseDecisionTree.card_le_prod_lowWeight {Label : Type uDepth2} [DecidableEq Label] [Fintype Label] (t : SparseDecisionTree Label) (N r : Label → ℕ) (hN : ∀ (p : t.Leaf) (i : Label), (t.stream p i).length ≤ N i) (hones : ∀ (p : t.Leaf) (i : Label), r i * List.count true (t.stream p i) ≤ N i) : Fintype.card t.Leaf ≤ ∏ i : Label, {w : Fin (N i) → Bool | r i * trueCount w ≤ N i}.card