OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionSamplerCoupling.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.CompressionData.sampler line 16

   Source documentation

   Compression draws one permutation and one prime. Its residue counter is enumerated deterministically by compressionTrial.

   def sampler (_D : CompressionData n) (hn : 168000000 ≤ n) :
       SamplerCoupling (CompressionSetup.TrialHistory n) :=
   …

   Mentions: OAI.LowSpaceSubsetSum.CompressionData, OAI.LowSpaceSubsetSum.SamplerCoupling, OAI.LowSpaceSubsetSum.CompressionSetup.TrialHistory

2. theorem OAI.LowSpaceSubsetSum.CompressionData.sampler_uniform line 21
3. theorem OAI.LowSpaceSubsetSum.CompressionData.sampler_failure line 27
4. theorem OAI.LowSpaceSubsetSum.CompressionData.prime_tail line 38
5. theorem OAI.LowSpaceSubsetSum.CompressionData.sampler_failure_pow line 50
6. theorem OAI.LowSpaceSubsetSum.CompressionData.sampler_event line 81

   Source documentation

   Every ideal compression event loses at most the unconditional exhaustion probability. No event is conditioned on successful sampling.

   theorem sampler_event (hn : 168000000 ≤ n)
       (P : CompressionSetup.TrialHistory n → Prop) :
       (D.trialLaw hn).probability P - 1 / (2 : ℝ) ^ n ≤
         (D.sampler hn).boundedLaw.probability (fun o => ∃ h, o = some h ∧ P h) := by
   …

   Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.TrialHistory