OAI/Combinatorics/ContingencyTables/Machines/FixedCardinalityLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Sequential uniform sampling of a subset of prescribed size

The head is included with probability k/n; conditional on that choice, the same rule is applied to the remaining coordinates. The exact mass is k!(n-k)!/n!, matching the factorial factor in the companion lift.

  1. def OAI.ContingencyTables.FixedCardinalityLaw.count line 21
  2. lemma OAI.ContingencyTables.FixedCardinalityLaw.count_le line 23
  3. lemma OAI.ContingencyTables.FixedCardinalityLaw.count_decompose line 28
  4. def OAI.ContingencyTables.FixedCardinalityLaw.consEquiv line 33
  5. def OAI.ContingencyTables.FixedCardinalityLaw.consLaw line 39
  6. lemma OAI.ContingencyTables.FixedCardinalityLaw.consLaw_mass line 43
  7. lemma OAI.ContingencyTables.FixedCardinalityLaw.consLaw_variation line 47
  8. def OAI.ContingencyTables.FixedCardinalityLaw.bernoulli line 54
  9. def OAI.ContingencyTables.FixedCardinalityLaw.headProbability line 59
  10. lemma OAI.ContingencyTables.FixedCardinalityLaw.headProbability_bounds line 61
  11. def OAI.ContingencyTables.FixedCardinalityLaw.headLaw line 67
  12. def OAI.ContingencyTables.FixedCardinalityLaw.remaining line 70
  13. def OAI.ContingencyTables.FixedCardinalityLaw.fixedLaw line 72
  14. def OAI.ContingencyTables.FixedCardinalityLaw.factorialMass line 76
  15. lemma OAI.ContingencyTables.FixedCardinalityLaw.factorialMass_true line 78
  16. lemma OAI.ContingencyTables.FixedCardinalityLaw.factorialMass_false line 85
  17. theorem OAI.ContingencyTables.FixedCardinalityLaw.fixedLaw_mass line 95

    Source documentation

    Each vector of the requested size has the reciprocal-binomial mass, and all other vectors have mass zero.

    theorem fixedLaw_mass (n k : ℕ) (hk : k≤n) (v : Fin n → Bool) :
    (fixedLaw n k).mass v=if count v=k then factorialMass n k else 0 := by
…

    Mentions: OAI.ContingencyTables.FixedCardinalityLaw.fixedLaw, OAI.ContingencyTables.FixedCardinalityLaw.count, OAI.ContingencyTables.FixedCardinalityLaw.factorialMass