OAI/Combinatorics/ContingencyTables/Sampling/ExactPrintCost.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform printing cost for every feasible exact-sampling output

  1. lemma OAI.ContingencyTables.ExactPrintCost.weight_ofFn line 14
  2. def OAI.ContingencyTables.ExactPrintCost.matrixSize line 19
  3. lemma OAI.ContingencyTables.ExactPrintCost.matrix_weight line 22
  4. theorem OAI.ContingencyTables.ExactPrintCost.polynomial_print_bound line 32

    Source documentation

    One fixed polynomial bounds both printing time and printed word length uniformly over the feasible set.

    theorem polynomial_print_bound : ∃ p : Polynomial ℕ,
    ∀ (m n : ℕ) (r : Fin m → ℕ) (c : Fin n → ℕ) (X : Table r c),
      GreedyFeasibleTable.printMatrixRealizer.cost (matrixCode X.val)+
        weight (GreedyFeasibleTable.printMatrix (matrixCode X.val)) ≤ p.eval (matrixSize (n := n) r) := by
…

    Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.GreedyFeasibleTable.printMatrix, OAI.ContingencyTables.ExactPrintCost.matrixSize

  5. lemma OAI.ContingencyTables.ExactPrintCost.prefix_print_bound line 40