OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorSamplingBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.rounded_family_mass line 13

   Source documentation

   Rounding the sampled family size costs at most one extra trial.

   theorem rounded_family_mass {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) :
       (⌈10 / θ⌉₊ : ℝ) * θ ≤ 11 := by
   …

2. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.rounded_family_incidence line 20
3. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.rounded_family_size line 34

   Source documentation

   This bound is uniform over every admissible sampled family.

   theorem rounded_family_size (g e c : ℕ) (he : e ≤ g) (hfeas : e - c ≤ g / 2)
       (hDN : (g / 2).choose (e - c) ≤ g.choose e) :
       ⌈10 / ((Nat.choose (g / 2) (e - c) : ℝ) / Nat.choose g e)⌉₊ ≤ 11 * 2 ^ g := by
   …

4. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.rounded_family_depth line 54