OAI/Combinatorics/ContingencyTables/Transport/RationalWalkApproximation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Adaptive completion errors add once per actual transition

  1. theorem OAI.ContingencyTables.FirstSuccess.variation_bind_two line 14
  2. theorem OAI.ContingencyTables.FirstSuccess.variation_bind_uniform line 48
  3. theorem OAI.ContingencyTables.FirstSuccess.walkLaw_variation line 62

    Source documentation

    The common state may depend on earlier randomness. Only the uniform one-step bound is used; the approximating chain need not be reversible.

    theorem walkLaw_variation (K L : α → RationalLaw α) (η : ℚ)
    (hη : ∀ x,variation (K x) (L x) ≤ η) (a : α) (n : ℕ) :
    variation (walkLaw K a n) (walkLaw L a n) ≤ n*η := by
…

    Mentions: OAI.ContingencyTables.FirstSuccess.variation, OAI.ContingencyTables.FirstSuccess.walkLaw

  4. theorem OAI.ContingencyTables.FirstSuccess.walkLaw_terminal_variation line 74