OAI/Combinatorics/ContingencyTables/Transport/TranslatedCompletionCounts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Symmetric accepted counts for the literal completion adjustment

  1. def OAI.ContingencyTables.CompletionTranslation.blockCount line 13
  2. def OAI.ContingencyTables.CompletionTranslation.acceptedCount line 16
  3. lemma OAI.ContingencyTables.CompletionTranslation.blockCount_pos line 19
  4. lemma OAI.ContingencyTables.CompletionTranslation.acceptedCount_le line 23
  5. theorem OAI.ContingencyTables.CompletionTranslation.acceptedCount_symmetric line 29

    Source documentation

    Reversibility uses the cardinality of actual accepted translations, not a Metropolis weight-ratio oracle.

    theorem acceptedCount_symmetric (R : X → Option I → ℕ) (P : X → Option J → ℕ)
    (htotal : ∀ x,(∑ i,R x i)=∑ j,P x j) (x y : X) :
    acceptedCount R P x y=acceptedCount R P y x := by
…

    Mentions: OAI.ContingencyTables.CompletionTranslation.acceptedCount