OAI/Combinatorics/ContingencyTables/Transport/IntegerPropagation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integer propagation tabulates adaptive finite laws without random tapes

  1. def OAI.ContingencyTables.IntegerPropagation.numerators line 15
  2. lemma OAI.ContingencyTables.IntegerPropagation.numerators_total line 19
  3. lemma OAI.ContingencyTables.IntegerPropagation.numerator_le line 29
  4. def OAI.ContingencyTables.IntegerPropagation.kernel line 35

    Source documentation

    One row of a dyadic transition table, viewed as an exact rational law.

    def kernel (hQ : 0<Q) (hrow : ∀ x,∑ y,B x y=Q) (x : A) : RationalLaw A where
…
  5. theorem OAI.ContingencyTables.IntegerPropagation.numerators_walkLaw line 44

    Source documentation

    Matrix/vector propagation accounts for all adaptive paths with one integer per state; its denominator exponent grows only with the steps.

    theorem numerators_walkLaw (hQ : 0<Q) (hrow : ∀ x,∑ y,B x y=Q)
    (start : A) (n : ℕ) (y : A) :
    (numerators B start n y:ℚ)/(Q:ℚ)^n=(walkLaw (kernel B Q hQ hrow) start n).mass y := by
…

    Mentions: OAI.ContingencyTables.IntegerPropagation.numerators, OAI.ContingencyTables.IntegerPropagation.kernel