OAI/Combinatorics/LowSpaceSubsetSum/Counting/CheckListWork.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LowSpaceSubsetSum.TopCoordinates.CheckInputs line 16
2. def OAI.LowSpaceSubsetSum.TopCoordinates.checkInputSize line 18
3. def OAI.LowSpaceSubsetSum.TopCoordinates.totalScans line 21
4. theorem OAI.LowSpaceSubsetSum.TopCoordinates.mean_totalScans line 25
5. theorem OAI.LowSpaceSubsetSum.TopCoordinates.totalScans_tail line 50

   Source documentation

   The check list is fixed before the separator draws, so no independence between the individual checks is used in this tail bound.

   theorem totalScans_tail (S : RoundedParameters g) (u : ℕ)
       (hu : 256 ≤ u) (hnu : n ≤ u) (hgu : g + 1 ≤ u)
       (target : ℤ) (checks : List (CheckInputs n))
       (hleft : ∀ p ∈ checks, ∀ x ∈ p.1.toList, ∀ i,
         (SeparatorCheck.localMask i (C.encodeEntry x).mask).card = S.c i)
       (hright : ∀ p ∈ checks, ∀ x ∈ p.2.toList, ∀ i,
         (SeparatorCheck.localMask i (C.encodeEntry x).mask).card = g / 2 - S.c i)
       (T : ℝ) (hT : 0 < T) :
       finiteUniformProbability (fun draws : IndependentFamilies g S.e S.counts =>
         T < (C.totalScans (familyArrays draws) target checks : ℝ)) ≤
         ((checkInputSize checks : ℝ) * (u : ℝ) ^ 22 *
           (2 : ℝ) ^ (((4 * g : ℕ) : ℝ) * (1 - binaryEntropy (1 / 4)))) / T := by
   …

   Mentions: OAI.LowSpaceSubsetSum.TopCoordinates.CheckInputs, OAI.LowSpaceSubsetSum.SeparatorCheck.localMask, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.TopCoordinates.checkInputSize, OAI.LowSpaceSubsetSum.binaryEntropy