OAI/Combinatorics/ContingencyTables/Transport/IntegerLawEmbedding.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Propagating a finite law inside a larger executable state box

  1. lemma OAI.ContingencyTables.IntegerLaw.push_count_injective line 14
  2. theorem OAI.ContingencyTables.IntegerLaw.walk_push_count line 21

    Source documentation

    A transition matrix may contain unused box states. Starting in the embedded state set gives exactly the pushed-forward original walk.

    theorem walk_push_count (K : A → IntegerLaw A Q) (L : B → IntegerLaw B Q)
    (f : A → B) (hf : ∀ x,L (f x)=(K x).push f) (start : A) (N : ℕ) (b : B) :
    (walk L (f start) N).count b=((walk K start N).push f).count b := by
…

    Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.IntegerLaw.push, OAI.ContingencyTables.IntegerLaw.walk