Unrestricted depth-three lower bound: sparse leaf count #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/SparseLeafCount.lean
Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.
theorem
Complexity.DepthThreeLowerBound.SparseDecisionTree.card_le_entropy_sum
{Label : Type uDepth1}
[DecidableEq Label]
[Fintype Label]
(t : SparseDecisionTree Label)
(N r : Label → ℕ)
(hr : ∀ (i : Label), 2 ≤ r i)
(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)
:
theorem
Complexity.DepthThreeLowerBound.SparseDecisionTree.card_le_of_entropy_budget
{Label : Type uDepth1}
[DecidableEq Label]
[Fintype Label]
(t : SparseDecisionTree Label)
(N r : Label → ℕ)
(hr : ∀ (i : Label), 2 ≤ r i)
(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)
{B : ℝ}
(hbudget : ∑ i : Label, ↑(N i) * binaryEntropy (1 / ↑(r i)) ≤ B)
: