OAI/Computability/DepthThree/SparsePartition.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.DepthThreeLowerBound.sparse_entropy_sum_budgetline 18 - structure
OAI.DepthThreeLowerBound.SparsePartitionline 46 - theorem
OAI.DepthThreeLowerBound.exists_sparse_partition_constantline 59