OAI/Combinatorics/ContingencyTables/Sampling/ExactPublicLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.ExactPublicLaw.prefixError line 21
2. lemma OAI.ContingencyTables.ExactPublicLaw.error_limit line 24
3. lemma OAI.ContingencyTables.ExactPublicLaw.event_output line 30
4. lemma OAI.ContingencyTables.ExactPublicLaw.prefix_error line 46
5. theorem OAI.ContingencyTables.ExactPublicLaw.tableMass_limit line 52
6. theorem OAI.ContingencyTables.ExactPublicLaw.tail_limit line 88
7. theorem OAI.ContingencyTables.ExactPublicLaw.haltMass_limit line 102
8. theorem OAI.ContingencyTables.ExactPublicLaw.halted_feasible line 118

   Source documentation

   Every finite halted public execution is feasible, including events of arbitrarily small positive probability.

   theorem halted_feasible (t : ℕ) (bits : Bits t)
       (hh : (MatchingFPRAS.run machine (Algorithms.encodeMargins r c) bits).state=none) :
       ∃ X : Table r c,Algorithms.OutputsTable machine (Algorithms.encodeMargins r c) bits X.val := by
   …

   Mentions: OAI.MatchingFPRAS.run, OAI.ContingencyTables.Algorithms.encodeMargins, OAI.ContingencyTables.Table, OAI.ContingencyTables.Algorithms.OutputsTable