CompletionProposalLaw.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The literal proposal, completion draw and acceptance test

def OAI.ContingencyTables.CompletionTranslation.proposalLaw line 18
Source documentation
Each feasible neighbor is assigned its prescribed dyadic mass; the remaining proposal words hold at the present state.
```
def proposalLaw (w : X → ℚ) (hw : ∀ y,0 ≤ w y) (htotal : ∑ y,w y ≤ 1) :
    RationalLaw (Option X) where
…
```
lemma OAI.ContingencyTables.CompletionTranslation.completionDecision_eq line 30
Source documentation
Only a proposal of y can reach y from a distinct current state x.
```
lemma completionDecision_eq (R : X → Option I → ℕ) (P : X → Option J → ℕ)
    (x y : X) (hne : x≠y) (q : Option X) (a : Table (R x) (P x)) :
    completionDecision R P x q a=y ↔
      q=some y ∧ ∀ i j,0 ≤ (a.val i j:ℤ)+between (R x) (R y) (P x) (P y) i j := by
…
```
Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.CompletionTranslation.completionDecision, OAI.ContingencyTables.CompletionTranslation.between
lemma OAI.ContingencyTables.CompletionTranslation.completionStepLaw_mass_ne line 44

lemma OAI.ContingencyTables.CompletionTranslation.uniformAcceptedMass line 69

Source documentation

The normalized completion indicator is exactly the acceptance count used in the reversible small kernel.

lemma uniformAcceptedMass (R : X → Option I → ℕ) (P : X → Option J → ℕ)
    (x y : X) [Nonempty (Table (R x) (P x))] :
    (∑ a : Table (R x) (P x),
      if ∀ i j,0 ≤ (a.val i j:ℤ)+between (R x) (R y) (P x) (P y) i j
      then (uniformLaw (α := Table (R x) (P x))).mass a else 0)=
…

Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.CompletionTranslation.between