OAI/Combinatorics/ContingencyTables/Sampling/GreedyRowMachine.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A binary list program for one row of the greedy initializer

  1. abbrev OAI.ContingencyTables.GreedyFeasibleTable.RowAccumulator line 11
  2. def OAI.ContingencyTables.GreedyFeasibleTable.rowCell line 15

    Source documentation

    A row pass keeps its residual margin and builds both output lists in reverse order, using only binary minimum, subtraction and list cons.

    def rowCell (z : ℕ × RowAccumulator) : RowAccumulator :=
…

    Mentions: OAI.ContingencyTables.GreedyFeasibleTable.RowAccumulator

  3. def OAI.ContingencyTables.GreedyFeasibleTable.rowCellRealizer line 19
  4. def OAI.ContingencyTables.GreedyFeasibleTable.listSplitRow line 32

    Source documentation

    The list version of the already proved dimension-recursive row split.

    def listSplitRow : ℕ → List ℕ → RowAccumulator
  | a,[] => (a,([],[]))
  | a,c::cs =>
    let q := min a c
…

    Mentions: OAI.ContingencyTables.GreedyFeasibleTable.RowAccumulator

  5. lemma OAI.ContingencyTables.GreedyFeasibleTable.fold_rowCell line 39
  6. def OAI.ContingencyTables.GreedyFeasibleTable.rowSplitRealizer line 52
  7. lemma OAI.ContingencyTables.GreedyFeasibleTable.listSplitRow_balance line 65
  8. lemma OAI.ContingencyTables.GreedyFeasibleTable.listSplitRow_lengths line 75