OAI/Combinatorics/ContingencyTables/Sampling/OriginalOuterVector.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.ProfilePrograms.OuterVectorInput line 13

    Source documentation

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

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

    Mentions: OAI.ContingencyTables.ProfilePrograms.TrialVectorInput

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