OAI/Combinatorics/ContingencyTables/Sampling/GreedyPublicMachine.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.GreedyFeasibleTable.encodeNat_nonzero line 12
2. lemma OAI.ContingencyTables.GreedyFeasibleTable.encodeNat_alphabet line 18
3. lemma OAI.ContingencyTables.GreedyFeasibleTable.publicGreedy_alphabet line 24
4. lemma OAI.ContingencyTables.GreedyFeasibleTable.encodeMargins_nonzero line 31
5. theorem OAI.ContingencyTables.GreedyFeasibleTable.publicGreedy_machine line 40

   Source documentation

   A single finite transition table performs the feasible initialization from the public margin encoding, with polynomial cost in its bit length.

   theorem publicGreedy_machine :
       ∃ (A : RandomMachine) (p : Polynomial ℕ),
         ∀ (m n : ℕ) (r : Fin m → ℕ) (c : Fin n → ℕ),
         (∑ i,r i)=∑ j,c j → ∀ t,
         p.eval (Algorithms.encodeMargins r c).length ≤ t → ∀ bits : Fin t → Bool,
         ∃ X : Table r c,Algorithms.OutputsTable A (Algorithms.encodeMargins r c) bits X.val := by
   …

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

6. theorem OAI.ContingencyTables.GreedyFeasibleTable.publicGreedy_sampling_machine line 55

   Source documentation

   The same initializer accepts the precision parameter on sampling inputs.

   theorem publicGreedy_sampling_machine :
       ∃ (A : RandomMachine) (p : Polynomial ℕ),
         ∀ (m n : ℕ) (r : Fin m → ℕ) (c : Fin n → ℕ),
         (∑ i,r i)=∑ j,c j → ∀ k t,
         p.eval (Algorithms.encodeSamplingInput r c k).length ≤ t → ∀ bits : Fin t → Bool,
         ∃ X : Table r c,Algorithms.OutputsTable A (Algorithms.encodeSamplingInput r c k) bits X.val := by
   …

   Mentions: OAI.ContingencyTables.Algorithms.encodeSamplingInput, OAI.ContingencyTables.Table, OAI.ContingencyTables.Algorithms.OutputsTable