OAI/Computability/DepthThree/SparseStreams.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DepthThreeLowerBound.SparseDecisionTree line 16
  2. def OAI.DepthThreeLowerBound.SparseDecisionTree.Leaf line 25
  3. def OAI.DepthThreeLowerBound.SparseDecisionTree.leafFintype line 30
  4. instance OAI.DepthThreeLowerBound.SparseDecisionTree.(instance at line 38) line 38
  5. def OAI.DepthThreeLowerBound.SparseDecisionTree.stream line 40
  6. def OAI.DepthThreeLowerBound.SparseDecisionTree.streamBit line 48
  7. def OAI.DepthThreeLowerBound.SparseDecisionTree.padded line 52
  8. theorem OAI.DepthThreeLowerBound.SparseDecisionTree.streamBit_injective line 56
  9. theorem OAI.DepthThreeLowerBound.SparseDecisionTree.padded_injective line 100
  10. theorem OAI.DepthThreeLowerBound.SparseDecisionTree.sum_getD_false line 113
  11. theorem OAI.DepthThreeLowerBound.SparseDecisionTree.trueCount_getD line 128
  12. theorem OAI.DepthThreeLowerBound.SparseDecisionTree.padded_trueCount line 135
  13. theorem OAI.DepthThreeLowerBound.SparseDecisionTree.card_le_prod_admitted line 141
  14. theorem OAI.DepthThreeLowerBound.SparseDecisionTree.card_le_prod_lowWeight line 158