OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleMixing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.CompanionOracleDensity.oracle_grid_card line 16
2. lemma OAI.ContingencyTables.CompanionOracleDensity.gridWeight_bounds line 23
3. lemma OAI.ContingencyTables.CompanionOracleDensity.oracleChain_pi_lower line 56
4. def OAI.ContingencyTables.CompanionOracleDensity.mixingConstant line 75
5. lemma OAI.ContingencyTables.CompanionOracleDensity.mixingConstant_ge_one line 77
6. lemma OAI.ContingencyTables.CompanionOracleDensity.cutConstant_lower line 88
7. theorem OAI.ContingencyTables.CompanionOracleDensity.oracleChain_polynomial_poincare line 99
8. theorem OAI.ContingencyTables.CompanionOracleDensity.oracleChain_point_mixing line 121

   Source documentation

   Pointwise relative mixing for the implemented dyadic-proposal Metropolis chain; this also bounds total variation.

   theorem oracleChain_point_mixing (A : Instance I J) (C a : ℝ) (hC : 0 < C)
       (ha : 0 ≤ a) (haH : a ≤ height A C) (z : View A → ℕ)
       (hz : BalancedBox.InBox (bounds A) z) {K : ℕ} (hK : 1 ≤ K)
       (hKB : (K:ℝ) ≤ binWidth A C)
       (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
       (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
   …

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