OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorExpectedWork.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.table_full_count line 18
2. abbrev OAI.LowSpaceSubsetSum.SeparatorExpectation.IndependentFamilies line 28
3. def OAI.LowSpaceSubsetSum.SeparatorExpectation.familyArrays line 31
4. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.left_multiplicity line 35
5. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.right_multiplicity line 50
6. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_left_multiplicity line 68
7. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_right_multiplicity line 90
8. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_mono line 110
9. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_mul_left line 116
10. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_list_sum line 120
11. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.coefficient_families line 126
12. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.mean_scans_le line 135

    Source documentation

    Exact finite expected charges bound the actual traversal, with every input occurrence counted separately even when its key is duplicated.

    theorem mean_scans_le (n : ℕ) (e ν : Fin 4 → ℕ) (heg : ∀ i, e i ≤ g)
        (target : ℤ) (xs ys : List (SeparatorCheck.Record g))
        (hce : ∀ x ∈ xs, ∀ i, (SeparatorCheck.localMask i x.mask).card ≤ e i) :
        mean (fun draws : IndependentFamilies g e ν =>
          ((SeparatorCheck.run n (familyArrays draws) target xs ys).scans : ℝ)) ≤
          ((6 * n + 8 + 2 * ∑ i : Fin 4, Nat.clog 2 (ν i) : ℕ) : ℝ) *
            ((xs.map (fun x => ∏ i : Fin 4, (1 + (ν i : ℝ) *
              ((Nat.choose (g - (SeparatorCheck.localMask i x.mask).card)
                (e i - (SeparatorCheck.localMask i x.mask).card) : ℝ) / Nat.choose g (e i))))).sum +
             (ys.map (fun y => ∏ i : Fin 4, (1 + (ν i : ℝ) *
              ((Nat.choose (g - (SeparatorCheck.localMask i y.mask).card) (e i) : ℝ) /
                Nat.choose g (e i))))).sum) := by
    …

    Mentions: OAI.LowSpaceSubsetSum.SeparatorCheck.Record, OAI.LowSpaceSubsetSum.SeparatorCheck.localMask, OAI.LowSpaceSubsetSum.SeparatorExpectation.IndependentFamilies, OAI.LowSpaceSubsetSum.SeparatorCheck.run, OAI.LowSpaceSubsetSum.SeparatorExpectation.familyArrays