OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperRationalMixing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Mixing in total variation for the actual rational small-walk law

  1. def OAI.ContingencyTables.SmallGraphProfiles.smallStationaryRat line 15
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.smallStationaryRat_cast line 24
  3. def OAI.ContingencyTables.SmallGraphProfiles.smallStationaryLaw line 33
  4. theorem OAI.ContingencyTables.SmallGraphProfiles.smallWalkLaw_variation line 48

    Source documentation

    This is the rational finite-walk distribution, rather than a bound only on real observables of an abstract chain.

    theorem smallWalkLaw_variation (r : I → ℕ) (c : J → ℕ) [Nonempty (PaperStates r c)]
    (i₀ : LargeRows r ((dimensionAllowance (I := I) (J := J))^20))
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.LargeRows