OAI/Combinatorics/ContingencyTables/Transport/FiniteMetropolis.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FirstSuccess.finiteAcceptStep line 17
2. def OAI.ContingencyTables.FirstSuccess.finiteAcceptLaw line 23
3. theorem OAI.ContingencyTables.FirstSuccess.finiteAcceptStep_eq_iff line 28
4. theorem OAI.ContingencyTables.FirstSuccess.finiteAcceptLaw_off_diagonal line 41

   Source documentation

   The off-diagonal mass is the exact product of the proposal-code and acceptance-coin frequencies. Both experiments use bounded finite samples.

   theorem finiteAcceptLaw_off_diagonal (a b : α) (proposal : β → Option α)
       (accept : α → γ → Prop) (hab : a ≠ b) :
       (finiteAcceptLaw a proposal accept).mass b =
         ((Finset.univ.filter (fun z => proposal z = some b)).card / (Fintype.card β : ℚ)) *
         ((Finset.univ.filter (accept b)).card / (Fintype.card γ : ℚ)) := by
   …

   Mentions: OAI.ContingencyTables.FirstSuccess.finiteAcceptLaw

5. theorem OAI.ContingencyTables.FirstSuccess.RationalLaw.eq_of_off_diagonal line 68

   Source documentation

   Two finite probability laws agreeing off a fixed state agree there as well. This recovers the rejection/stay probability from normalization.

   theorem RationalLaw.eq_of_off_diagonal (p q : RationalLaw α) (a : α)
       (h : ∀ b, b ≠ a → p.mass b = q.mass b) : p = q := by
   …