OAI/Combinatorics/ContingencyTables/Sampling/UnitOuterVector.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Computed first-success counts over the original-table box

  1. abbrev OAI.ContingencyTables.UnitCountPrograms.OuterVectorInput line 13

    Source documentation

    Walk data and margins; trial markers, denominator, and fallback matrix.

    abbrev OuterVectorInput := TrialVectorInput×((List Bool×ℕ)×MatrixCode)

    Mentions: OAI.ContingencyTables.UnitCountPrograms.TrialVectorInput

  2. def OAI.ContingencyTables.UnitCountPrograms.outerVectorInput line 15
  3. def OAI.ContingencyTables.UnitCountPrograms.outerVectorInputRealizer line 18
  4. def OAI.ContingencyTables.UnitCountPrograms.outerVectorMeasure line 25
  5. lemma OAI.ContingencyTables.UnitCountPrograms.work_outerVectorInput line 27
  6. def OAI.ContingencyTables.UnitCountPrograms.outerVector line 49
  7. def OAI.ContingencyTables.UnitCountPrograms.outerVectorRealizer line 51
  8. lemma OAI.ContingencyTables.UnitCountPrograms.work_outerVector line 55
  9. lemma OAI.ContingencyTables.SmallGraphProfiles.unit_outerVector_actual line 74