OAI/Combinatorics/ContingencyTables/Rooted/RootedCatalogWalk.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.RootedCatalogGrid.walkLaw_eq line 17
2. theorem OAI.ContingencyTables.RootedCatalogGrid.wordWalkLaw_eq line 52
3. theorem OAI.ContingencyTables.RootedCatalogGrid.wordWalkLaw_variation line 64

   Source documentation

   The original quantitative mixing estimate holds for the actual catalog-order word walk, with the identical number of steps.

   theorem wordWalkLaw_variation (A : Instance (Fin m) (Fin n)) (C a : ℕ) (theta : ℝ)
       (hC : 0 < C) (haH : a≤rationalHeight A C) (htheta : 0 < theta)
       (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
       (K Q : ℕ) (hK : 1≤K) (hQ : 0 < Q) (hKB : (K:ℝ)≤CompanionOracleDensity.binWidth A C)
       (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (CompanionOracleDensity.dimension A))
       (hCheeger : PublishedInputs.FiniteCheeger
         (Grid (I := Fin (CompanionOracleDensity.dimension A)) K))
   …

   Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger