OAI/Combinatorics/ContingencyTables/Transport/FiniteDependentLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact joint laws with a finite state-dependent completion space

  1. def OAI.ContingencyTables.FirstSuccess.dependentJointLaw line 14
  2. instance OAI.ContingencyTables.FirstSuccess.dependentJointNonempty line 24
  3. theorem OAI.ContingencyTables.FirstSuccess.dependentJointLaw_uniform line 29

    Source documentation

    A state chosen in proportion to its completion count, followed by a uniform completion, gives exactly the uniform law on all joint pairs.

    theorem dependentJointLaw_uniform (p : RationalLaw X)
    (hp : ∀ x,p.mass x=(Fintype.card (Y x):ℚ)/(∑ z : X,(Fintype.card (Y z):ℚ))) :
    dependentJointLaw p (fun x => uniformLaw (α := Y x))=
…

    Mentions: OAI.ContingencyTables.FirstSuccess.dependentJointLaw, OAI.ContingencyTables.FirstSuccess.uniformLaw