CompanionEstimatorAmplification.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic confidence amplification of the actual weight estimator

def OAI.ContingencyTables.CompanionOracleDensity.medianEstimatorBits line 20
Source documentation
Each complete estimator uses constant confidence; the requested failure probability changes only the number of independent medians.
```
def medianEstimatorBits (A : Instance I J) (C K j : ℕ) (epsilon delta : ℚ) : ℕ :=
…
```
def OAI.ContingencyTables.CompanionOracleDensity.medianEstimate line 23
theorem OAI.ContingencyTables.CompanionOracleDensity.medianEstimate_success line 32
theorem OAI.ContingencyTables.CompanionOracleDensity.medianEstimate_range line 84
Source documentation
Amplification also preserves the proved range on every word, including statistically unsuccessful words.
```
theorem medianEstimate_range (A : Instance I J) (C : ℕ) (hC : 0 < C) (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) (j : ℕ) (hj : j ≤ rationalHeight A C)
    (epsilon delta : ℚ) (he0 : 0 < epsilon) (he1 : epsilon < 1)
    (v : Grid (I := Fin (dimension A)) K)
…
```
Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.CompanionOracleDensity.dimension
lemma OAI.ContingencyTables.CompanionOracleDensity.medianEstimatorBits_eq line 112
Source documentation
The exact bit budget grows linearly with the binary confidence parameter, rather than with its reciprocal.
```
lemma medianEstimatorBits_eq (A : Instance I J) (C K j : ℕ) (epsilon delta : ℚ) :
    medianEstimatorBits A C K j epsilon delta =
      64*(delta.den.bits.length+1) *
        estimatorWordBits A C K j (innerTolerance (epsilon/2) j) 1 := rfl
…
```
Mentions: OAI.ContingencyTables.CompanionOracleDensity.medianEstimatorBits, OAI.ContingencyTables.CompanionOracleDensity.estimatorWordBits, OAI.ContingencyTables.CompanionOracleDensity.innerTolerance