OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleSchedule.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Explicit accuracy and sample-count parameters for the weight oracle

  1. def OAI.ContingencyTables.CompanionOracleDensity.offsetAccuracy line 18
  2. def OAI.ContingencyTables.CompanionOracleDensity.correctionTheta line 20
  3. def OAI.ContingencyTables.CompanionOracleDensity.roundingTolerance line 22
  4. def OAI.ContingencyTables.CompanionOracleDensity.sampleCount line 24
  5. lemma OAI.ContingencyTables.CompanionOracleDensity.le_two_pow line 26
  6. lemma OAI.ContingencyTables.CompanionOracleDensity.offsetAccuracy_positive line 34
  7. lemma OAI.ContingencyTables.CompanionOracleDensity.offsetAccuracy_error line 41
  8. lemma OAI.ContingencyTables.CompanionOracleDensity.correction_noise_budget line 55
  9. lemma OAI.ContingencyTables.CompanionOracleDensity.sampleCount_positive line 63
  10. lemma OAI.ContingencyTables.CompanionOracleDensity.sampleCount_budget line 71

    Source documentation

    Every one of the j ratio averages and the final correction average has failure at most this common share.

    lemma sampleCount_budget (j : ℕ) (delta failure : ℚ) (hdelta : 0 < delta)
    (hfailure : 0 < failure) :
    16384/((sampleCount j delta failure:ℝ)*(delta:ℝ)^2) ≤ (failure:ℝ)/(4*((j:ℝ)+1)) := by
…

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.sampleCount

  11. theorem OAI.ContingencyTables.CompanionOracleDensity.scheduled_correction_failure line 89

    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) (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.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

  12. theorem OAI.ContingencyTables.CompanionOracleDensity.scheduled_ratio_failure line 117