CompanionOracleBudget.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The explicit finite mixing schedule of the companion evaluator

lemma OAI.ContingencyTables.CompanionOracleDensity.oracle_min_mass_exponential line 16
def OAI.ContingencyTables.CompanionOracleDensity.oracleTime line 40
Source documentation
The source uses a linear reciprocal-error allowance inside the mixing time, avoiding any unimplemented logarithm computation.
```
def oracleTime (A : Instance I J) (C : ℝ) (K Q : ℕ) (theta : ℝ) : ℕ :=
…
```
lemma OAI.ContingencyTables.CompanionOracleDensity.oracle_time_error line 43
theorem OAI.ContingencyTables.CompanionOracleDensity.oracleChain_scheduled_point_mixing line 77
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) (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))
…
```
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
theorem OAI.ContingencyTables.CompanionOracleDensity.oracleChain_scheduled_total_variation line 89