CompletionStepApproximation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Completion replacement in the actual proposal-and-translation step

def OAI.ContingencyTables.CompletionTranslation.completionDecision line 19
Source documentation
A proposal is either a hold or a target state. The sampled completion is discarded after its literal translated-nonnegativity test.
```
def completionDecision (R : X → Option I → ℕ) (P : X → Option J → ℕ)
    (x : X) (proposal : Option X) (a : Table (R x) (P x)) : X :=
…
```
Mentions: OAI.ContingencyTables.Table
def OAI.ContingencyTables.CompletionTranslation.completionStepLaw line 25

theorem OAI.ContingencyTables.CompletionTranslation.completionStep_variation line 32

Source documentation

From a common state only the completion draw changes. Mapping to the accept/reject decision and averaging over the same proposal cannot enlarge TV.

theorem completionStep_variation (R : X → Option I → ℕ) (P : X → Option J → ℕ)
    (proposal : X → RationalLaw (Option X))
    (μ ν : (x : X) → RationalLaw (Table (R x) (P x))) (η : ℚ)
    (h : ∀ x,variation (μ x) (ν x) ≤ η) (x : X) :
    variation (completionStepLaw R P proposal μ x) (completionStepLaw R P proposal ν x) ≤ η := by
…

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

theorem OAI.ContingencyTables.CompletionTranslation.completionWalk_terminal_variation line 45

Source documentation

The transition draws and the final completion all use fresh bits. The bound is uniform even though the state supplied to each draw is adaptive.

theorem completionWalk_terminal_variation (R : X → Option I → ℕ) (P : X → Option J → ℕ)
    {Y : Type*} [Fintype Y] [DecidableEq Y]
    (proposal : X → RationalLaw (Option X))
    (μ ν : (x : X) → RationalLaw (Table (R x) (P x)))
    (output : (x : X) → Table (R x) (P x) → Y) (η : ℚ)
    (h : ∀ x,variation (μ x) (ν x) ≤ η) (x : X) (n : ℕ) :
    variation
      (bindLaw (walkLaw (completionStepLaw R P proposal μ) x n) (fun z => mapLaw (μ z) (output z)))
      (bindLaw (walkLaw (completionStepLaw R P proposal ν) x n) (fun z => mapLaw (ν z) (output z))) ≤
        (n+1)*η :=
…

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