OAI/Combinatorics/ContingencyTables/Sampling/ExactPhysicalProgram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.ExactPhysicalProgram.ofOnline line 13
2. def OAI.ContingencyTables.ExactPhysicalProgram.program line 23
3. def OAI.ContingencyTables.ExactPhysicalProgram.output line 27
4. lemma OAI.ContingencyTables.ExactPhysicalProgram.output_some line 30
5. lemma OAI.ContingencyTables.ExactPhysicalProgram.output_none_live line 37
6. theorem OAI.ContingencyTables.ExactPhysicalProgram.prefix_correct line 43

   Source documentation

   Every finite exact-sampling prefix runs on one fixed finite physical transition table, including its live failure endpoint.

   theorem prefix_correct (as : List Symbol) (N : ℕ) :
       ∃ q,Implements program.table (output as)
         (program.initial (Tape.mk₁ (packed as))) q ∧
         ∀ g : Option MatrixCode → ℚ,
           q.mean g=(ExactCoreProgram.prefixExperiment (ProfilePrograms.exactParsedMargins as) N).mean g := by
   …

   Mentions: OAI.ContingencyTables.ExactPhysicalProgram.output, OAI.ContingencyTables.ExactCoreProgram.prefixExperiment, OAI.ContingencyTables.ProfilePrograms.exactParsedMargins