OAI/Combinatorics/ContingencyTables/Sampling/AllSmallInitialization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reading the unique all-small completion directly from its profile

  1. def OAI.ContingencyTables.SmallGraphProfiles.allSmallFibre line 17

    Source documentation

    The output data consists only of the two stored small views. Existence of a completion supplies the erased proof that these are valid margins.

    noncomputable def allSmallFibre
    (hsmall : ∀ i j,FirstPaperPhysicalMarginal.paperSmall r c i j=true)
    (z : PaperStates r c) : PaperFibre r c z := by
…

    Mentions: OAI.ContingencyTables.FirstPaperPhysicalMarginal.paperSmall, OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.PaperFibre