OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationBudgetSampling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.prefix_floor_modulus_lower line 11
2. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.actual_modulus_floor_lower line 39
3. def OAI.LowSpaceSubsetSum.RepresentationSetup.AllocatedResourceGood line 48
4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.actual_history_resource_failure line 63

   Source documentation

   Every actual prime history has the resource tail estimate before observing its independently uniform low residues.

   theorem actual_history_resource_failure (hn : 20000 ≤ n)
       (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
       (hu : 256 ≤ inputScale R.input) (h : R.PrimeHistory) :
       finiteUniformProbability (fun r : R.Residues h.2 =>
         ¬R.AllocatedResourceGood hn hlog ⟨h, r⟩) <
         (1 / 10 : ℝ) / (inputScale R.input : ℝ) ^ 100 := by
   …

   Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.finiteUniformProbability

5. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.actual_joint_resource_failure line 79

   Source documentation

   Joint failure with any event fixed before the low residues is small. In particular this applies to the spread-test event, without conditioning on the rare surviving representation.

   theorem actual_joint_resource_failure (hn : 20000 ≤ n)
       (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
       (hu : 256 ≤ inputScale R.input) (passing : R.PrimeHistory → Prop) :
       R.trialLaw.probability (fun h => passing h.1 ∧ ¬R.AllocatedResourceGood hn hlog h) ≤
         (1 / 10 : ℝ) / (inputScale R.input : ℝ) ^ 100 := by
   …

   Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.inputScale