OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperSuccessEvent.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The actual joint-law success event counts every original table once

  1. def OAI.ContingencyTables.SmallGraphProfiles.stateJointProjection line 27

    Source documentation

    Forget the redundant small-profile coordinate while retaining both full margin views. This projection is injective on all actual joint pairs.

    def stateJointProjection (a : PaperStateJoint r c) := a.2.val

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStateJoint

  2. lemma OAI.ContingencyTables.SmallGraphProfiles.stateJointProjection_injective line 29
  3. def OAI.ContingencyTables.SmallGraphProfiles.paperJointState line 34
  4. def OAI.ContingencyTables.SmallGraphProfiles.paperJointEmbedding line 42
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.paperJointEmbedding_injective line 45
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.paperJointEmbedding_balanced line 51
  7. def OAI.ContingencyTables.SmallGraphProfiles.balancedJointFromState line 55
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.balancedJointFromState_projection line 60
  9. lemma OAI.ContingencyTables.SmallGraphProfiles.embedding_fromState line 66
  10. lemma OAI.ContingencyTables.SmallGraphProfiles.fromState_embedding line 72
  11. def OAI.ContingencyTables.SmallGraphProfiles.StateJointSuccess line 78

    Source documentation

    The success test reads precisely balance and the lower padding bound.

    def StateJointSuccess (a : PaperStateJoint r c) : Prop :=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStateJoint

  12. abbrev OAI.ContingencyTables.SmallGraphProfiles.SuccessfulStateJoint line 82
  13. def OAI.ContingencyTables.SmallGraphProfiles.successStateEquiv line 84
  14. def OAI.ContingencyTables.SmallGraphProfiles.originalStateSuccessEquiv line 96

    Source documentation

    Every accepted actual state/completion pair unpads to one original table, and every original table has one such pair.

    def originalStateSuccessEquiv : Table r c ≃ SuccessfulStateJoint r c :=
…

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