OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperIdealKernel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Separate identification of the ideal small-state completion experiment

  1. def OAI.ContingencyTables.SmallGraphProfiles.idealReferenceLaw line 25

    Source documentation

    The ideal reference draw is transported from the nonempty physical completion fibre, so no additional existence assumption is needed.

    def idealReferenceLaw (z : PaperStates r c) : RationalLaw (Table (R z) (P z)) :=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.Table

  2. lemma OAI.ContingencyTables.SmallGraphProfiles.idealReferenceLaw_uniform line 28
  3. theorem OAI.ContingencyTables.SmallGraphProfiles.smallIdealStep_eq line 39