OAI/Combinatorics/ContingencyTables/Sampling/GreedyPublicProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Parsing the public margins and printing the greedy matrix

All operations are existing binary list programs. The bounded take and drop operations also terminate polynomially on malformed headers.

  1. def OAI.ContingencyTables.GreedyFeasibleTable.marginLists line 19

    Source documentation

    The first two natural numbers give the lengths of the two margins.

    def marginLists (ns : List ℕ) : List ℕ × List ℕ :=
…
  2. def OAI.ContingencyTables.GreedyFeasibleTable.marginListsRealizer line 25
  3. lemma OAI.ContingencyTables.GreedyFeasibleTable.polynomial_marginLists line 32
  4. def OAI.ContingencyTables.GreedyFeasibleTable.printMatrix line 45
  5. def OAI.ContingencyTables.GreedyFeasibleTable.printMatrixRealizer line 48
  6. lemma OAI.ContingencyTables.GreedyFeasibleTable.polynomial_printMatrix line 51
  7. def OAI.ContingencyTables.GreedyFeasibleTable.publicGreedy line 54
  8. def OAI.ContingencyTables.GreedyFeasibleTable.publicGreedyRealizer line 58
  9. theorem OAI.ContingencyTables.GreedyFeasibleTable.polynomial_publicGreedy line 64

    Source documentation

    One fixed program parses dimensions, computes all greedy cells and prints the public binary matrix representation in polynomial bit time.

    theorem polynomial_publicGreedy : PolynomialTime publicGreedyRealizer :=
…

    Mentions: OAI.ContingencyTables.GreedyFeasibleTable.publicGreedyRealizer

  10. lemma OAI.ContingencyTables.GreedyFeasibleTable.natWords_fold line 69
  11. lemma OAI.ContingencyTables.GreedyFeasibleTable.parse_natWords line 76
  12. lemma OAI.ContingencyTables.GreedyFeasibleTable.encodeMargins_natWords line 79
  13. lemma OAI.ContingencyTables.GreedyFeasibleTable.marginLists_spec line 85
  14. lemma OAI.ContingencyTables.GreedyFeasibleTable.printMatrix_ofFn line 92
  15. theorem OAI.ContingencyTables.GreedyFeasibleTable.publicGreedy_spec line 99

    Source documentation

    The actual parser/program/printer computes the mathematically proved initializer on the exact public input encoding.

    theorem publicGreedy_spec {m n : ℕ} (r : Fin m → ℕ) (c : Fin n → ℕ) :
    publicGreedy (Algorithms.encodeMargins r c)=Algorithms.encodeMatrix (matrix r c) := by
…

    Mentions: OAI.ContingencyTables.GreedyFeasibleTable.publicGreedy, OAI.ContingencyTables.Algorithms.encodeMargins, OAI.ContingencyTables.Algorithms.encodeMatrix, OAI.ContingencyTables.GreedyFeasibleTable.matrix

  16. lemma OAI.ContingencyTables.GreedyFeasibleTable.publicGreedy_suffix line 111

    Source documentation

    Extra encoded parameters after the margins do not change initialization.

    lemma publicGreedy_suffix {m n : ℕ} (r : Fin m → ℕ) (c : Fin n → ℕ) (ns : List ℕ) :
    publicGreedy (Algorithms.encodeMargins r c++ns.flatMap encodeNat)=
      Algorithms.encodeMatrix (matrix r c) := by
…

    Mentions: OAI.ContingencyTables.GreedyFeasibleTable.publicGreedy, OAI.ContingencyTables.Algorithms.encodeMargins, OAI.ContingencyTables.Algorithms.encodeMatrix, OAI.ContingencyTables.GreedyFeasibleTable.matrix

  17. lemma OAI.ContingencyTables.GreedyFeasibleTable.publicGreedy_sampling line 124