OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperCodeProposal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The compiled neighbor draw has the small-chain proposal law

  1. def OAI.ContingencyTables.ProfilePrograms.codeNeighborProposal line 11
  2. def OAI.ContingencyTables.ProfilePrograms.codeNeighborProposalRealizer line 14
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_codeNeighborProposal line 19
  4. def OAI.ContingencyTables.SmallGraphProfiles.stateCode line 41
  5. def OAI.ContingencyTables.SmallGraphProfiles.stateCodeData line 44
  6. def OAI.ContingencyTables.SmallGraphProfiles.decodeStateCode line 47
  7. lemma OAI.ContingencyTables.SmallGraphProfiles.decode_stateCode line 50
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.stateCode_injective line 56
  9. theorem OAI.ContingencyTables.SmallGraphProfiles.decodeStateCode_eq_some_iff line 62
  10. def OAI.ContingencyTables.SmallGraphProfiles.codeNeighborStates line 73
  11. lemma OAI.ContingencyTables.SmallGraphProfiles.codeNeighborStates_nodup line 76
  12. theorem OAI.ContingencyTables.SmallGraphProfiles.mem_codeNeighborStates line 83
  13. lemma OAI.ContingencyTables.SmallGraphProfiles.codeNeighborStates_length line 94
  14. lemma OAI.ContingencyTables.SmallGraphProfiles.codeNeighborStates_codes line 106
  15. lemma OAI.ContingencyTables.SmallGraphProfiles.codeNeighbors_decode_total line 113
  16. lemma OAI.ContingencyTables.SmallGraphProfiles.getElem_filterMap_total line 120
  17. def OAI.ContingencyTables.SmallGraphProfiles.decodedCodeProposal line 132
  18. lemma OAI.ContingencyTables.SmallGraphProfiles.decodedCodeProposal_apply line 135
  19. lemma OAI.ContingencyTables.SmallGraphProfiles.decodedCodeProposal_eq line 139
  20. theorem OAI.ContingencyTables.SmallGraphProfiles.decodedCodeProposal_law line 149

    Source documentation

    The implemented binary neighbor choice has exactly the proposal law used by the already-proved small-chain mixing estimate.

    theorem decodedCodeProposal_law (htotal : (∑ i,r i)=∑ j,c j) (x : PaperStates r c) :
    mapLaw (uniformLaw (α := Fin s → Bool)) (decodedCodeProposal r c e x)=smallProposalLaw r c x := by
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.decodedCodeProposal, OAI.ContingencyTables.SmallGraphProfiles.smallProposalLaw