SmallPatternArithmetic.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Integer tests for balanced and single-defect small profiles

lemma OAI.ContingencyTables.SmallGraphProfiles.cell_eq_coordinates line 17
lemma OAI.ContingencyTables.SmallGraphProfiles.view_at_cell line 22
lemma OAI.ContingencyTables.SmallGraphProfiles.q_at_cell line 28
def OAI.ContingencyTables.SmallGraphProfiles.CellSumBalanced line 33
def OAI.ContingencyTables.SmallGraphProfiles.CellSumDefect line 36
theorem OAI.ContingencyTables.SmallGraphProfiles.balanced_iff_cellSums line 42
theorem OAI.ContingencyTables.SmallGraphProfiles.defect_iff_cellSums line 63
Source documentation
On bounded coordinates the signed defect equation is precisely an equality of nonnegative integer sums. This avoids truncated subtraction in the executable profile-pattern test.
```
theorem defect_iff_cellSums
    (hb : ∀ a : Cells small,z (a,true)≤B a.val.1 a.val.2)
    (s t : Cells small) :
    IsDefect (smallView small z false) (smallQ small B z) s.val t.val ↔
      CellSumDefect small B z s t := by
…
```
Mentions: OAI.ContingencyTables.IsDefect, OAI.ContingencyTables.SmallGraphProfiles.CellSumDefect
theorem OAI.ContingencyTables.SmallGraphProfiles.pattern_iff_cellSums line 98
Source documentation
An allowed profile is detected by one balanced test or by one of the ordered cell-pair tests. This uses at most quadratically many labels.
```
theorem pattern_iff_cellSums
    (hb : ∀ a : Cells small,z (a,true)≤B a.val.1 a.val.2) :
    Pattern small B z ↔ CellSumBalanced small B z ∨
      ∃ s t : Cells small,CellSumDefect small B z s t := by
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.Pattern, OAI.ContingencyTables.SmallGraphProfiles.CellSumBalanced, OAI.ContingencyTables.SmallGraphProfiles.CellSumDefect