OAI/Combinatorics/ContingencyTables/Sampling/GreedyFeasibleTable.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A dimension-recursive feasible table constructor

The constructor removes a column on each inner call and a row on each outer call. Large binary margins are never processed one unit at a time.

  1. structure OAI.ContingencyTables.GreedyFeasibleTable.RowSplit line 17
  2. def OAI.ContingencyTables.GreedyFeasibleTable.splitRow line 22
  3. lemma OAI.ContingencyTables.GreedyFeasibleTable.splitRow_columns line 29
  4. lemma OAI.ContingencyTables.GreedyFeasibleTable.splitRow_balance line 39
  5. lemma OAI.ContingencyTables.GreedyFeasibleTable.splitRow_unused line 48
  6. lemma OAI.ContingencyTables.GreedyFeasibleTable.splitRow_sum line 56
  7. lemma OAI.ContingencyTables.GreedyFeasibleTable.splitRow_remaining_sum line 62
  8. def OAI.ContingencyTables.GreedyFeasibleTable.matrix line 71
  9. theorem OAI.ContingencyTables.GreedyFeasibleTable.matrix_hasMargins line 78

    Source documentation

    The arithmetic constructor fills any equal-total natural margins.

    theorem matrix_hasMargins {m n : ℕ} (r : Fin m → ℕ) (c : Fin n → ℕ)
    (htotal : (∑ i,r i)=∑ j,c j) : HasMargins (matrix r c) r c := by
…

    Mentions: OAI.ContingencyTables.HasMargins, OAI.ContingencyTables.GreedyFeasibleTable.matrix

  10. def OAI.ContingencyTables.GreedyFeasibleTable.table line 109

    Source documentation

    A literal, dimension-recursive fallback for the sampling algorithm.

    def table {m n : ℕ} (r : Fin m → ℕ) (c : Fin n → ℕ)
    (htotal : (∑ i,r i)=∑ j,c j) : Table r c := ⟨matrix r c,matrix_hasMargins r c htotal⟩
…

    Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.GreedyFeasibleTable.matrix, OAI.ContingencyTables.GreedyFeasibleTable.matrix_hasMargins