OAI/Combinatorics/ContingencyTables/Machines/FixedCardinalityMixture.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The uniform-size mixture realizes the initial factorial weights

A size is drawn uniformly from 0,...,n, followed by the sequential fixed-cardinality draw. Its subset mass is the literal local factorial weight divided by n+1. The bounded Boolean implementation uses a fresh word for the size and for each inclusion decision.

  1. def OAI.ContingencyTables.FixedCardinalityMixture.sizeMixture line 21
  2. theorem OAI.ContingencyTables.FixedCardinalityMixture.sizeMixture_mass line 24
  3. def OAI.ContingencyTables.FixedCardinalityMixture.subsetEquiv line 36
  4. lemma OAI.ContingencyTables.FixedCardinalityMixture.count_subset_inverse line 44
  5. def OAI.ContingencyTables.FixedCardinalityMixture.localLaw line 51
  6. theorem OAI.ContingencyTables.FixedCardinalityMixture.localLaw_mass line 54
  7. theorem OAI.ContingencyTables.FixedCardinalityMixture.localLaw_mass_cast line 59
  8. def OAI.ContingencyTables.FixedCardinalityMixture.roundedSizeMixture line 64
  9. lemma OAI.ContingencyTables.FixedCardinalityMixture.uniformInt_eq line 68
  10. theorem OAI.ContingencyTables.FixedCardinalityMixture.roundedSizeMixture_error line 74
  11. def OAI.ContingencyTables.FixedCardinalityMixture.drawBits line 88
  12. def OAI.ContingencyTables.FixedCardinalityMixture.vectorDraw line 90
  13. theorem OAI.ContingencyTables.FixedCardinalityMixture.vectorDraw_law line 94
  14. def OAI.ContingencyTables.FixedCardinalityMixture.subsetDraw line 114
  15. theorem OAI.ContingencyTables.FixedCardinalityMixture.subsetDraw_error line 117