OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorWorkBound.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Expected scans of the actual checker at the manuscript's exponent

  1. structure OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters line 15

    Source documentation

    Numerical consequences of the prescribed rounded sample sizes.

    structure RoundedParameters (g : ℕ) where
…
  2. def OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.counts line 32
  3. def OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.leftCharge line 35
  4. def OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.rightCharge line 39
  5. def OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.chargeBound line 43
  6. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.count_half line 46
  7. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.counts_depth line 54
  8. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.left_charge_nonneg line 58
  9. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.right_charge_nonneg line 62
  10. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.left_charge_le line 66
  11. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.right_charge_le line 77
  12. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.map_sum_le line 89
  13. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.total_charge_le line 97
  14. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.mean_scans_polynomial line 110