RootedOracleMixing.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit point and total-variation mixing for the selected-root grid

lemma OAI.ContingencyTables.RootedOracleDensity.gridWeight_bounds line 18
lemma OAI.ContingencyTables.RootedOracleDensity.oracleChain_pi_lower line 51
theorem OAI.ContingencyTables.RootedOracleDensity.oracleChain_polynomial_poincare line 70

theorem OAI.ContingencyTables.RootedOracleDensity.oracleChain_point_mixing line 92

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) (R : RootedCompletion.Selection A.T) (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.RootedCompletion.Selection, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

theorem OAI.ContingencyTables.RootedOracleDensity.oracleChain_scheduled_point_mixing line 110

Source documentation

The actual dyadic Metropolis chain attains the per-draw error used in the evaluator's union bound at the explicit finite source schedule.

theorem oracleChain_scheduled_point_mixing (A : Instance I J) (R : RootedCompletion.Selection A.T) (C a theta : ℝ)
    (hC : 0 < C) (ha : 0 ≤ a) (haH : a ≤ height A C) (htheta : 0 < theta)
    (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
    (K Q : ℕ) (hK : 1 ≤ K) (hQ : 0 < Q) (hKB : (K:ℝ) ≤ binWidth A C)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…

theorem OAI.ContingencyTables.RootedOracleDensity.oracleChain_scheduled_total_variation line 122