OAI/Combinatorics/ContingencyTables/Transport/IntegerEquivLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integer laws under bijective coordinate changes

  1. def OAI.ContingencyTables.IntegerLaw.equiv line 13

    Source documentation

    A coordinate permutation leaves the common denominator unchanged.

    def equiv (p : IntegerLaw A Q) (e : A ≃ B) : IntegerLaw B Q where
…

    Mentions: OAI.ContingencyTables.IntegerLaw

  2. lemma OAI.ContingencyTables.IntegerLaw.equiv_count line 17
  3. lemma OAI.ContingencyTables.IntegerLaw.toRational_equiv line 20
  4. def OAI.ContingencyTables.IntegerLaw.walk line 26

    Source documentation

    The integer propagation table also defines a normalized finite law.

    def walk [DecidableEq A] (K : A → IntegerLaw A Q) (x : A) (n : ℕ) :
    IntegerLaw A (Q^n) where
…

    Mentions: OAI.ContingencyTables.IntegerLaw

  5. lemma OAI.ContingencyTables.IntegerLaw.toRational_walk line 31