RootedCorrectionSamples.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Confidence for the actual rational correction samples

def OAI.ContingencyTables.RootedOracleDensity.correctionMean line 20
lemma OAI.ContingencyTables.RootedOracleDensity.correctionMean_eq line 24
lemma OAI.ContingencyTables.RootedOracleDensity.correctionMean_bounds line 32
def OAI.ContingencyTables.RootedOracleDensity.correctionSample line 40
lemma OAI.ContingencyTables.RootedOracleDensity.correctionSample_mean line 46

theorem OAI.ContingencyTables.RootedOracleDensity.correctionSample_mean_bias line 58

Source documentation

Both finite sampling error and deterministic rational power error are bounded relative to the literal correction mean.

theorem correctionSample_mean_bias (A : Instance I J) (R : RootedCompletion.Selection A.T) (C a : ℕ) (theta : ℝ)
    (hC : 0 < C) (haH : a ≤ rationalHeight A C) (htheta : 0 < theta)
    (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
    (K Q h : ℕ) (hK : 1 ≤ K) (hQ : 0 < Q) (hW : 100*A.d*K ≤ A.W)
    (hB : (K:ℝ)=binWidth A C) (sigma : ℚ) (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1/2)
    (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.correctionSamples_failure line 96

Source documentation

Independent finite words give confidence for the computed correction; the displayed arithmetic tolerances are discharged by the outer schedule.

theorem correctionSamples_failure (A : Instance I J) (R : RootedCompletion.Selection A.T) (C a : ℕ) (theta delta : ℝ)
    (hC : 0 < C) (haH : a ≤ rationalHeight A C) (htheta : 0 < theta) (hdelta : 0 < delta)
    (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
    (K Q h N : ℕ) (hK : 1 ≤ K) (hQ : 0 < Q) (hW : 100*A.d*K ≤ A.W) (hN : 0 < N)
    (hB : (K:ℝ)=binWidth A C) (sigma : ℚ) (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1/2)
    (hsigmaDelta : (sigma:ℝ) ≤ delta/4)
    (hnoise : theta/(8*Q)+(A.d:ℝ)/(2:ℝ)^(4*(h+A.d)) ≤ delta/1024)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…