OAI/Combinatorics/ContingencyTables/Sampling/ExactPublicCost.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.ExactPublicCost.middleOutput line 17
2. def OAI.ContingencyTables.ExactPublicCost.output line 22
3. theorem OAI.ContingencyTables.ExactPublicCost.wrap_prefix line 26
4. theorem OAI.ContingencyTables.ExactPublicCost.table_prefix line 94

   Source documentation

   Table decoding preserves the finite-prefix work bound.

   theorem table_prefix (htotal : (∑ i,r i)=∑ j,c j) (N B : ℕ)
       (hB : ∀ X : Table r c,GreedyFeasibleTable.printMatrixRealizer.cost (matrixCode X.val)≤B) :
       ∃ p,Implements ExactPhysicalProgram.program.table (ExactTablePrefix.output r c)
         (ExactPhysicalProgram.program.initial (Tape.mk₁ (TreePost.packed (ExactTablePrefix.input r c)))) p ∧
         (∀ g : Option (Table r c) → ℚ,p.mean g=(ExactTablePrefix.experiment r c N).mean g) ∧
         p.cost≤ExactPhysicalCost.budget (ExactTablePrefix.input r c) N B := by
   …

   Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.ExactTablePrefix.output, OAI.ContingencyTables.ExactTablePrefix.input, OAI.ContingencyTables.ExactTablePrefix.experiment, OAI.ContingencyTables.ExactPhysicalCost.budget

5. def OAI.ContingencyTables.ExactPublicCost.budget line 121
6. theorem OAI.ContingencyTables.ExactPublicCost.prefix_correct_cost line 125
7. lemma OAI.ContingencyTables.ExactPublicCost.quadratic_budget line 142