CompanionCorrectionSamples.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Confidence for the actual rational correction samples

def OAI.ContingencyTables.CompanionOracleDensity.correctionMean line 19
lemma OAI.ContingencyTables.CompanionOracleDensity.correctionMean_eq line 23
lemma OAI.ContingencyTables.CompanionOracleDensity.correctionMean_bounds line 31
def OAI.ContingencyTables.CompanionOracleDensity.correctionSample line 39
lemma OAI.ContingencyTables.CompanionOracleDensity.correctionSample_mean line 45
theorem OAI.ContingencyTables.CompanionOracleDensity.correctionSample_mean_bias line 57
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) (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.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

theorem OAI.ContingencyTables.CompanionOracleDensity.correctionSamples_failure line 95

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) (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))
…

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