OAI/Combinatorics/ContingencyTables/Transport/SuccessfulJointBijection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The literal successful balanced pairs are exactly the original tables

  1. abbrev OAI.ContingencyTables.SmallGraphProfiles.PaperJoint line 16
  2. def OAI.ContingencyTables.SmallGraphProfiles.jointTable line 20
  3. abbrev OAI.ContingencyTables.SmallGraphProfiles.SuccessfulJoint line 25
  4. def OAI.ContingencyTables.SmallGraphProfiles.originalSuccessfulJoint line 29
  5. def OAI.ContingencyTables.SmallGraphProfiles.unpadSuccessfulJoint line 38
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.unpadSuccessfulJoint_val line 54
  7. def OAI.ContingencyTables.SmallGraphProfiles.successfulJointEquiv line 60

    Source documentation

    Each success produces exactly one original table, and every original table has exactly one successful state/completion preimage.

    noncomputable def successfulJointEquiv (r : I → ℕ) (c : J → ℕ) :
    Table r c ≃ SuccessfulJoint r c where
…

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