Repair.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Repair of a defect with its large completion

The two full matrices give the row and column views, agreeing at all large cells. Moving one unit from the positive cell to the crossing cell and resetting the column view preserves the enlarged margins. This is the joint-object injection underlying the repair in paper 200-01.

def OAI.ContingencyTables.transferInt line 21
Source documentation
A single unit transfer, allowing source and receiver to coincide.
```
def transferInt (X : I → J → ℕ) (source receiver : I × J) (i : I) (j : J) : ℤ :=
…
```
theorem OAI.ContingencyTables.transferInt_nonnegative line 26
theorem OAI.ContingencyTables.transferInt_row line 37
theorem OAI.ContingencyTables.transferInt_column line 44
def OAI.ContingencyTables.IsDefect line 52
Source documentation
The defect equation q=x-e_t+e_s identifies the sign convention.
```
def IsDefect (x q : I → J → ℕ) (negative positive : I × J) : Prop :=
…
```
theorem OAI.ContingencyTables.IsDefect.positive_entry line 57
def OAI.ContingencyTables.repairMatrix line 67
Source documentation
The crossing receiver (i',j) in the manuscript.
```
def repairMatrix (x : I → J → ℕ) (s t : I × J) : I → J → ℕ :=
…
```
theorem OAI.ContingencyTables.repairMatrix_cast line 71
theorem OAI.ContingencyTables.repairMatrix_margins line 79
Source documentation
The repaired matrix has the old row totals and old column-view totals. The crossing cell may be large, and either of its coordinates may coincide with those of the original defect cells.
```
theorem repairMatrix_margins {x q : I → J → ℕ} {s t : I × J}
    (h : IsDefect x q s t) (r : I → ℕ) (c : J → ℕ)
    (hr : ∀ i, ∑ j, x i j = r i) (hc : ∀ j, ∑ i, q i j = c j) :
    HasMargins (repairMatrix x s t) r c := by
…
```
Mentions: OAI.ContingencyTables.IsDefect, OAI.ContingencyTables.HasMargins, OAI.ContingencyTables.repairMatrix
theorem OAI.ContingencyTables.repairMatrix_injective line 105
Source documentation
Fixed defect labels make the repair injective on joint row/column views, hence also on the state together with its large completion.
```
theorem repairMatrix_injective {x q y p : I → J → ℕ} {s t : I × J}
    (hx : IsDefect x q s t) (hy : IsDefect y p s t)
    (heq : repairMatrix x s t = repairMatrix y s t) : x = y ∧ q = p := by
…
```
Mentions: OAI.ContingencyTables.IsDefect, OAI.ContingencyTables.repairMatrix