IntegerBoxTruncation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite-box fixed-total weight

Truncating the positive product outside its box and required total leaves every valid two-removal matrix entry unchanged at a box-valid display two above that total. The balancing development therefore applies to the paper's literal zero-extended weight.

def OAI.ContingencyTables.IntegerBoxTruncation.truncate line 22
lemma OAI.ContingencyTables.IntegerBoxTruncation.removal_inBox line 26
lemma OAI.ContingencyTables.IntegerBoxTruncation.removal_total line 32
theorem OAI.ContingencyTables.IntegerBoxTruncation.removal_truncate_eq line 39
Source documentation
Exact equality of the actual truncated and product integer matrices.
```
theorem removal_truncate_eq (f : (I → ℕ) → ℝ) (m z : I → ℕ) (R : ℕ)
    (hz : InBox m z) (ht : (∑ i, z i)=R+2) :
    integerRemovalMatrix (truncate f m R) z = integerRemovalMatrix f z := by
…
```
Mentions: OAI.ContingencyTables.IntegerBoxTruncation.truncate
theorem OAI.ContingencyTables.IntegerBoxTruncation.truncate_positive_slice line 52
Source documentation
Positivity on the actual slice is unchanged by literal zero extension.
```
theorem truncate_positive_slice (f : (I → ℕ) → ℝ) (m : I → ℕ) (R : ℕ)
    (hpos : PositiveSlice f m R) : PositiveSlice (truncate f m R) m R := by
…
```
Mentions: OAI.ContingencyTables.IntegerBoxTruncation.truncate
theorem OAI.ContingencyTables.IntegerBoxTruncation.truncate_removal_slice line 59
Source documentation
The actual integer signature is unchanged by the box/total indicator.
```
theorem truncate_removal_slice (f : (I → ℕ) → ℝ) (m : I → ℕ) (R : ℕ)
    (hsig : RemovalSlice f m R) : RemovalSlice (truncate f m R) m R := by
…
```
Mentions: OAI.ContingencyTables.IntegerBoxTruncation.truncate