OAI/Combinatorics/ContingencyTables/Sampling/GreedyTableMachine.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A fixed binary list program constructing the greedy table

  1. abbrev OAI.ContingencyTables.GreedyFeasibleTable.TableAccumulator line 10
  2. def OAI.ContingencyTables.GreedyFeasibleTable.tableRow line 12
  3. def OAI.ContingencyTables.GreedyFeasibleTable.tableRowRealizer line 16
  4. def OAI.ContingencyTables.GreedyFeasibleTable.listMatrix line 23
  5. lemma OAI.ContingencyTables.GreedyFeasibleTable.fold_tableRow line 29
  6. def OAI.ContingencyTables.GreedyFeasibleTable.tableRealizer line 43

    Source documentation

    Every loop is over an input row or column; binary margins are never counted down one unit at a time.

    def tableRealizer : Realizer (fun z : List ℕ × List ℕ => listMatrix z.1 z.2) := by
…

    Mentions: OAI.ContingencyTables.GreedyFeasibleTable.listMatrix

  7. lemma OAI.ContingencyTables.GreedyFeasibleTable.listSplitRow_ofFn line 52
  8. theorem OAI.ContingencyTables.GreedyFeasibleTable.listMatrix_ofFn line 63

    Source documentation

    The compiled list program computes the same feasible matrix used by the probability analysis.

    theorem listMatrix_ofFn {m n : ℕ} (rs : Fin m → ℕ) (cs : Fin n → ℕ) :
    listMatrix (List.ofFn rs) (List.ofFn cs)=
      List.ofFn (fun i => List.ofFn (matrix rs cs i)) := by
…

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