DenseTrialCountProgram.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Computing one accepted-table numerator from the cached bin vector

abbrev OAI.ContingencyTables.DensePrograms.TrialCountData line 16
Source documentation
Cached walk vector, shared bit allowance, and the table/margin data with the requested precision.
```
abbrev TrialCountData := (List ℕ×List Bool)×OffsetWidthData
```
Mentions: OAI.ContingencyTables.DensePrograms.OffsetWidthData
def OAI.ContingencyTables.DensePrograms.trialCountIndexInput line 18
def OAI.ContingencyTables.DensePrograms.trialCountIndexInputRealizer line 21
lemma OAI.ContingencyTables.DensePrograms.polynomial_trialCountIndexInput line 27
def OAI.ContingencyTables.DensePrograms.trialCountOffsetInput line 37
def OAI.ContingencyTables.DensePrograms.trialCountOffsetInputRealizer line 40
lemma OAI.ContingencyTables.DensePrograms.polynomial_trialCountOffsetInput line 45
def OAI.ContingencyTables.DensePrograms.trialTableCount line 56
def OAI.ContingencyTables.DensePrograms.trialTableCountRealizer line 60
theorem OAI.ContingencyTables.DensePrograms.polynomial_trialTableCount line 69
Source documentation
Once the bin vector is cached, one accepted-table numerator uses polynomial binary arithmetic and one lookup.
```
theorem polynomial_trialTableCount : PolynomialTime trialTableCountRealizer := by
…
```
Mentions: OAI.ContingencyTables.DensePrograms.trialTableCountRealizer

theorem OAI.ContingencyTables.DensePrograms.trialTableCount_actual line 81

Source documentation

The program computes the count of the unique accepted trial for this table, using canonical walk tabulation.

theorem trialTableCount_actual {m n d : ℕ} (R : Option (Fin m) → ℕ)
    (P : Option (Fin n) → ℕ) (hd : 14≤d) (hq : m*n≤d)
    (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j) (h : ℕ)
    (cap : List Bool)
    (hcap : ∀ j : Fin (m*n),
      FairBits.offsetBitLength (integerWidth R P d (finProdFinEquiv.symm j)) h d≤cap.length)
    (X : Table R P) :
    trialTableCount ((tabulateDenseWalk ((marginCode R,marginCode P),(d,h)),cap),
      (tableCoordinatesCode R P d X,h))=
    (denseTrialCounts R P d hd hR hP finProdFinEquiv h
      (canonicalOrigin (m*n) d (by omega))).count
        (tableTrial R P d hd hR hP finProdFinEquiv X) := by
…

Mentions: OAI.ContingencyTables.FairBits.offsetBitLength, OAI.ContingencyTables.Table, OAI.ContingencyTables.DensePrograms.trialTableCount, OAI.ContingencyTables.DensePrograms.tabulateDenseWalk, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.DensePrograms.tableCoordinatesCode, OAI.ContingencyTables.DensePrograms.canonicalOrigin