OAI/Combinatorics/ContingencyTables/Transport/BoundedProfileSemantics.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The bounded binary loop preserves the physical profile walk

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.stateCode_bounded line 18
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.capViews_stateCode line 23
  3. def OAI.ContingencyTables.SmallGraphProfiles.encodedConfiguration line 44
  4. theorem OAI.ContingencyTables.SmallGraphProfiles.advanceProfile_encoded line 47
  5. theorem OAI.ContingencyTables.SmallGraphProfiles.profileWalk_ofFn line 60