CompanionEstimatorWords.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A single Boolean word for the literal companion weight estimator

def OAI.ContingencyTables.CompanionOracleDensity.estimatorWordBits line 20
Source documentation
The complete input length, with one independent walk for each ratio sample and one walk plus integer-bin draw for each correction sample.
```
def estimatorWordBits (A : Instance I J) (C K j : ℕ) (delta failure : ℚ) : ℕ :=
…
```
lemma OAI.ContingencyTables.CompanionOracleDensity.estimatorWordBits_eq line 26
def OAI.ContingencyTables.CompanionOracleDensity.ratioBlockWordEquiv line 34
def OAI.ContingencyTables.CompanionOracleDensity.estimatorWordEquiv line 45
Source documentation
This equivalence partitions, rather than reuses, the random bits of all the individual experiments in the estimator.
```
def estimatorWordEquiv (A : Instance I J) (C K j : ℕ) (delta failure : ℚ) :
    (Fin (estimatorWordBits A C K j delta failure) → Bool) ≃
      EstimatorInput A C K j delta failure :=
…
```
Mentions: OAI.ContingencyTables.CompanionOracleDensity.estimatorWordBits, OAI.ContingencyTables.CompanionOracleDensity.EstimatorInput
def OAI.ContingencyTables.CompanionOracleDensity.wordEstimate line 55
theorem OAI.ContingencyTables.CompanionOracleDensity.wordEstimate_failure line 63
Source documentation
The single fixed-length word has exactly the independent-product law.
```
theorem wordEstimate_failure (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 failure : ℚ) (he0 : 0 < epsilon) (he1 : epsilon < 1) (hf : 0 < failure)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…
```
Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger
theorem OAI.ContingencyTables.CompanionOracleDensity.wordEstimate_range line 89