OAI/Combinatorics/ContingencyTables/Transport/FiniteMetropolisTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FiniteObservableTransport.proposedMove line 15
2. theorem OAI.ContingencyTables.FiniteObservableTransport.proposedMove_sameLaw line 22

   Source documentation

   The proposed state and fresh acceptance experiment can both be replaced by experiments with the same observable law.

   theorem proposedMove_sameLaw (start : X) (pick : P → Option X) (pick' : Q → Option X)
       (accept : X → U → Bool) (accept' : X → V → Bool)
       (hp : SameLaw pick pick') (ha : ∀ next,SameLaw (accept next) (accept' next)) :
       SameLaw (fun z : P × U => proposedMove start (pick z.1) accept z.2)
         (fun z : Q × V => proposedMove start (pick' z.1) accept' z.2) := by
   …

   Mentions: OAI.ContingencyTables.FiniteObservableTransport.SameLaw, OAI.ContingencyTables.FiniteObservableTransport.proposedMove

3. theorem OAI.ContingencyTables.FiniteObservableTransport.holding_sameLaw line 35

   Source documentation

   An independent holding flag is preserved by the replacement.

   theorem holding_sameLaw {A B : Type*} [Fintype A] [Fintype B]
       (start : X) (f : A → X) (g : B → X) (h : SameLaw f g) :
       SameLaw (fun z : (Fin 1 → Bool) × A => if z.1 0 then start else f z.2)
         (fun z : (Fin 1 → Bool) × B => if z.1 0 then start else g z.2) := by
   …

   Mentions: OAI.ContingencyTables.FiniteObservableTransport.SameLaw