OAI/Combinatorics/ContingencyTables/Transport/InitialFactorialLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Independent initial cell choices give the literal companion law

The finite rational law is the product of the uniform-size subset laws. Encoding a choice as its paired transversal yields exactly the initial law of the companion's factorial lift, with its actual free-completion normalizer cancelled.

  1. def OAI.ContingencyTables.InitialFactorialLaw.choiceLaw line 23
  2. theorem OAI.ContingencyTables.InitialFactorialLaw.choiceLaw_mass_cast line 30
  3. def OAI.ContingencyTables.InitialFactorialLaw.plainLaw line 40
  4. theorem OAI.ContingencyTables.InitialFactorialLaw.plainLaw_mass_cast line 43
  5. theorem OAI.ContingencyTables.InitialFactorialLaw.plainLaw_lift line 49
  6. def OAI.ContingencyTables.InitialFactorialLaw.companionLaw line 62
  7. theorem OAI.ContingencyTables.InitialFactorialLaw.companionLaw_mass line 68

    Source documentation

    No abstract initialization hypothesis: the rational product law is the actual phase-zero law of the given bounded-table instance.

    theorem companionLaw_mass (A : Instance I J)
    (S : {S : Set (Labels A×Bool) // PlainState pairs S}) :
    ((companionLaw A).mass S:ℝ)=CompanionWarmStart.law A 0 S.val := by
…

    Mentions: OAI.ContingencyTables.InitialFactorialLaw.companionLaw, OAI.ContingencyTables.CompanionWarmStart.law