Model.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Contingency tables with arbitrary margins

The feasible sets in result 200 are represented by natural-valued matrices, without a positivity, balance, or sparsity restriction on the margins. The finite encoding bound is proved rather than assumed.

def OAI.ContingencyTables.HasMargins line 23
Source documentation
The row and column equations in both papers.
Also declared: ComparatorChallenges/ContingencyTables.lean:61 (same declaration text).
```
def HasMargins (X : I → J → ℕ) (r : I → ℕ) (c : J → ℕ) : Prop :=
…
```
def OAI.ContingencyTables.Table line 27
Source documentation
Unrestricted nonnegative integer tables with the specified margins.
Also declared: ComparatorChallenges/ContingencyTables.lean:64 (same declaration text).
```
def Table (r : I → ℕ) (c : J → ℕ) := {X : I → J → ℕ // HasMargins X r c}
```
Mentions: OAI.ContingencyTables.HasMargins
def OAI.ContingencyTables.BoundedTable line 30
Source documentation
The entry constraints for the companion paper, including structural zeros.
Also declared: ComparatorChallenges/ContingencyTables.lean:66 (same declaration text).
```
def BoundedTable (r : I → ℕ) (c : J → ℕ) (b : I → J → ℕ) :=
…
```
theorem OAI.ContingencyTables.totals_equal line 33
theorem OAI.ContingencyTables.entry_le_row line 38
Also declared: ComparatorChallenges/ContingencyTables.lean:69 (same declaration text).
theorem OAI.ContingencyTables.entry_le_total line 43
Also declared: ComparatorChallenges/ContingencyTables.lean:74 (same declaration text).
instance OAI.ContingencyTables.table_finite line 48
Source documentation
Binary margins may be large, but the feasible set is finite.
Also declared: ComparatorChallenges/ContingencyTables.lean:78 (same declaration text).
```
instance table_finite (r : I → ℕ) (c : J → ℕ) : Finite (Table r c) := by
…
```
Mentions: OAI.ContingencyTables.Table
instance OAI.ContingencyTables.table_fintype line 57
Also declared: ComparatorChallenges/ContingencyTables.lean:87 (same declaration text).
instance OAI.ContingencyTables.boundedTable_fintype line 60
Also declared: ComparatorChallenges/ContingencyTables.lean:90 (same declaration text).
theorem OAI.ContingencyTables.table_card_le line 67
Source documentation
The bound used in the exact correction's exhaustive branch.
```
theorem table_card_le (r : I → ℕ) (c : J → ℕ) :
    Fintype.card (Table r c) ≤ ((∑ i, r i) + 1) ^ (Fintype.card I * Fintype.card J) := by
…
```
Mentions: OAI.ContingencyTables.Table
theorem OAI.ContingencyTables.sum_decrease_one line 84
theorem OAI.ContingencyTables.exists_table line 94
Source documentation
Equal total nonnegative margins always admit an unrestricted table. The proof removes one unit at a positive row and a positive column. It is an existence argument; no polynomial runtime is asserted here.
```
theorem exists_table (r : I → ℕ) (c : J → ℕ) (htotal : ∑ i, r i = ∑ j, c j) :
    ∃ X, HasMargins X r c := by
…
```
Mentions: OAI.ContingencyTables.HasMargins
theorem OAI.ContingencyTables.table_nonempty line 145