OAI/Combinatorics/ContingencyTables/Dense/DenseRationalKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Rational transition and walk laws for the actual dense bin chain

  1. def OAI.ContingencyTables.GridBoundary.rationalProposal line 18
  2. def OAI.ContingencyTables.GridBoundary.rationalMove line 20
  3. def OAI.ContingencyTables.GridBoundary.rationalTransition line 25
  4. theorem OAI.ContingencyTables.GridBoundary.rationalMove_cast line 29
  5. theorem OAI.ContingencyTables.GridBoundary.rationalTransition_cast line 39
  6. def OAI.ContingencyTables.GridBoundary.rationalTransitionLaw line 50
  7. def OAI.ContingencyTables.GridBoundary.rationalWalk line 63
  8. theorem OAI.ContingencyTables.GridBoundary.rationalWalk_cast line 68
  9. def OAI.ContingencyTables.GridBoundary.rationalWalkLaw line 80
  10. def OAI.ContingencyTables.GridBoundary.rationalStationaryLaw line 93
  11. theorem OAI.ContingencyTables.GridBoundary.rationalStationaryLaw_cast line 105
  12. theorem OAI.ContingencyTables.GridBoundary.rationalWalkLaw_variation line 116

    Source documentation

    The exact rational finite-walk law satisfies the dense sampler's mixing bound. The hypotheses are precisely the two published geometric inputs.

    theorem rationalWalkLaw_variation (R : Option I → ℕ) (P : Option J → ℕ)
    (d : ℕ) (hd : 14 ≤ d) (hR : ∀ i, d ^ 12 ≤ R i) (hP : ∀ j, d ^ 12 ≤ P j)
    (hRmax : ∀ i, R (some i) ≤ R none) (hPmax : ∀ j, P (some j) ≤ P none)
    (hdimR : Fintype.card (Option I) ≤ d) (hdimP : Fintype.card (Option J) ≤ d)
    (hfree : Fintype.card (I × J) ≤ d) (htotal : ∑ i, R i = ∑ j, P j)
    (e : I × J ≃ Fin q) (hPL : PublishedInputs.FiniteBoxPrekopaLeindler q)
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin q) (4 * d ^ 8)))
…

    Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger, OAI.ContingencyTables.GridBoundary.Grid