OAI/Computability/DepthThree/SparsePrefix.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DepthThreeLowerBound.SparseNumerics line 18
  2. theorem OAI.DepthThreeLowerBound.sparse_occurrence_le_of_no_sunflower line 26
  3. structure OAI.DepthThreeLowerBound.SparseStep line 57
  4. def OAI.DepthThreeLowerBound.SparseStep.batch line 67
  5. theorem OAI.DepthThreeLowerBound.SparseStep.target_active line 71
  6. theorem OAI.DepthThreeLowerBound.SparseStep.target_added line 77
  7. theorem OAI.DepthThreeLowerBound.SparseStep.valid line 83
  8. theorem OAI.DepthThreeLowerBound.SparseStep.fresh_added line 88
  9. theorem OAI.DepthThreeLowerBound.SparseStep.batch_size_count line 96
  10. theorem OAI.DepthThreeLowerBound.SparseStep.removed_eq_empty_of_le line 112
  11. theorem OAI.DepthThreeLowerBound.SparseStep.update_balance line 125
  12. inductive OAI.DepthThreeLowerBound.SparsePath line 135
  13. def OAI.DepthThreeLowerBound.SparsePath.length line 144
  14. def OAI.DepthThreeLowerBound.SparsePath.insertions line 148
  15. def OAI.DepthThreeLowerBound.SparsePath.processed line 154
  16. def OAI.DepthThreeLowerBound.SparsePath.petalSteps line 158
  17. theorem OAI.DepthThreeLowerBound.SparsePath.valid line 163
  18. theorem OAI.DepthThreeLowerBound.SparsePath.insertions_nil line 169
  19. theorem OAI.DepthThreeLowerBound.SparsePath.insertions_snoc line 172
  20. theorem OAI.DepthThreeLowerBound.SparsePath.insertions_sum_snoc line 177
  21. theorem OAI.DepthThreeLowerBound.SparsePath.added_occurrence_bound line 186
  22. theorem OAI.DepthThreeLowerBound.SparsePath.online_insertion_bound line 221
  23. theorem OAI.DepthThreeLowerBound.SparsePath.insertion_recurrence line 250
  24. theorem OAI.DepthThreeLowerBound.SparsePath.length_le_insertions line 262
  25. theorem OAI.DepthThreeLowerBound.SparsePath.processed_le_insertions line 275
  26. theorem OAI.DepthThreeLowerBound.SparsePath.petalSteps_mul_le_insertions line 290
  27. theorem OAI.DepthThreeLowerBound.sparse_insertion_budget_of_recurrence line 309
  28. theorem OAI.DepthThreeLowerBound.SparsePath.insertion_budget line 339
  29. theorem OAI.DepthThreeLowerBound.SparsePath.insertion_sum_budget line 346
  30. theorem OAI.DepthThreeLowerBound.SparsePath.length_budget line 360
  31. theorem OAI.DepthThreeLowerBound.SparsePath.processed_budget line 367
  32. theorem OAI.DepthThreeLowerBound.SparsePath.petalSteps_budget line 374