DenseSuccessCounts.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

One entry per accepted dense table, with no trial-fibre enumeration

theorem OAI.ContingencyTables.GridBoundary.denseTrial_success_count line 17
Source documentation
The unique bin-offset trial for a table supplies its entire success count. This removes a sum over all trials from each output lookup.
```
theorem denseTrial_success_count (R : Option I → ℕ) (P : Option J → ℕ) (d : ℕ)
    (hd : 14≤d) (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j)
    (e : I×J ≃ Fin q) (htotal : ∑ i,R i=∑ j,P j) (h : ℕ)
    (a : Grid (I := Fin q) (4*d^8)) (X : Table R P) :
…
```
Mentions: OAI.ContingencyTables.GridBoundary.Grid, OAI.ContingencyTables.Table
theorem OAI.ContingencyTables.GridBoundary.denseTrial_failure_count line 31
Source documentation
The rejected count is determined by the known common denominator and the accepted table counts, including all invalid completions.
```
theorem denseTrial_failure_count (R : Option I → ℕ) (P : Option J → ℕ) (d : ℕ)
    (hd : 14≤d) (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j)
    (e : I×J ≃ Fin q) (htotal : ∑ i,R i=∑ j,P j) (h : ℕ)
    (a : Grid (I := Fin q) (4*d^8)) :
…
```
Mentions: OAI.ContingencyTables.GridBoundary.Grid
theorem OAI.ContingencyTables.GridBoundary.denseTrial_table_count line 47
Source documentation
Evaluation uses one propagated bin numerator and one product of closed-form offset counts; it never enumerates the acceptance bits.
```
theorem denseTrial_table_count (R : Option I → ℕ) (P : Option J → ℕ) (d : ℕ)
    (hd : 14≤d) (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j)
    (e : I×J ≃ Fin q) (h : ℕ)
    (a : Grid (I := Fin q) (4*d^8)) (X : Table R P) :
…
```
Mentions: OAI.ContingencyTables.GridBoundary.Grid, OAI.ContingencyTables.Table