OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperJointLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniformity of the actual state/completion joint law

  1. abbrev OAI.ContingencyTables.SmallGraphProfiles.PaperFibre line 18
  2. instance OAI.ContingencyTables.SmallGraphProfiles.paperFibreNonempty line 24
  3. abbrev OAI.ContingencyTables.SmallGraphProfiles.PaperStateJoint line 34
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.paperFibre_card_block line 36
  5. def OAI.ContingencyTables.SmallGraphProfiles.stationaryJointLaw line 46
  6. theorem OAI.ContingencyTables.SmallGraphProfiles.stationaryJointLaw_uniform line 54

    Source documentation

    The law keeps the completion multiplicity exactly: each full pair has the same probability, including pairs above defective small states.

    theorem stationaryJointLaw_uniform (r : I → ℕ) (c : J → ℕ) [Nonempty (PaperStates r c)]
    (i₀ : LargeRows r ((dimensionAllowance (I := I) (J := J))^20))
…

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

  7. theorem OAI.ContingencyTables.SmallGraphProfiles.paperStateJoint_card line 64

    Source documentation

    Cardinality of the full joint space is the small chain normalizer.

    theorem paperStateJoint_card (r : I → ℕ) (c : J → ℕ) :
    (Fintype.card (PaperStateJoint r c):ℝ)=∑ z,stateWeight r c z := by
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStateJoint, OAI.ContingencyTables.SmallGraphProfiles.stateWeight