OAI/Combinatorics/ContingencyTables/Sampling/GreedyRowComplexity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Polynomial binary cost of a greedy row pass

  1. lemma OAI.ContingencyTables.GreedyFeasibleTable.polynomial_cellMinimum line 11
  2. lemma OAI.ContingencyTables.GreedyFeasibleTable.polynomial_rowCell line 15
  3. lemma OAI.ContingencyTables.GreedyFeasibleTable.listSplitRow_bounds line 37

    Source documentation

    No entry produced by a row pass exceeds its original column bound; the binary list sizes therefore grow by only a constant factor.

    lemma listSplitRow_bounds (a : ℕ) (cs : List ℕ) :
    (listSplitRow a cs).1≤a ∧
    weight (listSplitRow a cs).2.1≤4*weight cs ∧
    weight (listSplitRow a cs).2.2≤4*weight cs := by
…

    Mentions: OAI.ContingencyTables.GreedyFeasibleTable.listSplitRow

  4. lemma OAI.ContingencyTables.GreedyFeasibleTable.polynomial_rowFold line 50
  5. theorem OAI.ContingencyTables.GreedyFeasibleTable.polynomial_rowSplit line 64