RootedOracleSchedule.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Explicit accuracy and sample-count parameters for the weight oracle

theorem OAI.ContingencyTables.RootedOracleDensity.scheduled_correction_failure line 22

Source documentation

The concrete correction schedule discharges both arithmetic error allowances; only the named published PL/Cheeger inputs remain.

theorem scheduled_correction_failure (A : Instance I J) (R : RootedCompletion.Selection A.T) (C a j : ℕ)
    (hC : 0 < C) (haH : a ≤ rationalHeight A C) (delta failure : ℚ)
    (hdelta : 0 < delta) (hdelta1 : delta < 1) (hfailure : 0 < failure)
    (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
    (K : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (hB : (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.scheduled_ratio_failure line 50