OAI/Combinatorics/ContingencyTables/Dense/DenseCompletionProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Signed dependent entries from binary margin and matrix lists

  1. abbrev OAI.ContingencyTables.DensePrograms.CompletionData line 12
  2. abbrev OAI.ContingencyTables.DensePrograms.CompletionCell line 13
  3. def OAI.ContingencyTables.DensePrograms.completionParts line 16

    Source documentation

    Index zero denotes the distinguished dependent row or column.

    def completionParts (z : CompletionCell) : ℕ×ℕ :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.CompletionCell

  4. def OAI.ContingencyTables.DensePrograms.completionPartsRealizer line 25
  5. theorem OAI.ContingencyTables.DensePrograms.polynomial_completionParts line 48
  6. def OAI.ContingencyTables.DensePrograms.marginCode line 82
  7. def OAI.ContingencyTables.DensePrograms.optionIndex line 85
  8. lemma OAI.ContingencyTables.DensePrograms.marginCode_getD line 89
  9. theorem OAI.ContingencyTables.DensePrograms.completionParts_code line 97
  10. theorem OAI.ContingencyTables.DensePrograms.completionParts_signed line 123

    Source documentation

    The difference of the computed pair is the exact signed completion entry.

    theorem completionParts_signed {m n : ℕ} (R : Option (Fin m) → ℕ)
    (P : Option (Fin n) → ℕ) (z : Fin m → Fin n → ℕ)
    (i : Option (Fin m)) (j : Option (Fin n)) :
    let p := completionParts
…

    Mentions: OAI.ContingencyTables.DensePrograms.completionParts