RowColumnPenalties.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Literal doubled row and column penalties

The false coordinate of a cell is its row value x. Its true coordinate is y, with physical column value q=B-y. Thus row and column factor groups are disjoint, while their small-cell subsets are nested inside them. Offsets below are the actual full margins and capacity sums of the paper.

def OAI.ContingencyTables.RowColumnPenalties.cellLine line 23
def OAI.ContingencyTables.RowColumnPenalties.smallCoordinate line 25
def OAI.ContingencyTables.RowColumnPenalties.rowView line 27
def OAI.ContingencyTables.RowColumnPenalties.columnView line 28
def OAI.ContingencyTables.RowColumnPenalties.columnCapacity line 31
def OAI.ContingencyTables.RowColumnPenalties.smallColumnCapacity line 32
def OAI.ContingencyTables.RowColumnPenalties.fullOffset line 35
def OAI.ContingencyTables.RowColumnPenalties.viewSlope line 38
def OAI.ContingencyTables.RowColumnPenalties.smallOffset line 40
lemma OAI.ContingencyTables.RowColumnPenalties.lineTotal_row line 44
lemma OAI.ContingencyTables.RowColumnPenalties.lineTotal_column line 50
lemma OAI.ContingencyTables.RowColumnPenalties.smallTotal_row line 54
lemma OAI.ContingencyTables.RowColumnPenalties.smallTotal_column line 60
lemma OAI.ContingencyTables.RowColumnPenalties.columnViews_add line 67
lemma OAI.ContingencyTables.RowColumnPenalties.smallColumnViews_add line 77
lemma OAI.ContingencyTables.RowColumnPenalties.full_affine_row line 90
lemma OAI.ContingencyTables.RowColumnPenalties.full_affine_column line 98
lemma OAI.ContingencyTables.RowColumnPenalties.small_affine_row line 109
lemma OAI.ContingencyTables.RowColumnPenalties.small_affine_column line 118

theorem OAI.ContingencyTables.RowColumnPenalties.penalty_eq line 134

Source documentation

This is exactly the manuscript's full row/column deviation plus its small residual violation penalty, on the actual doubled physical box.

theorem penalty_eq (small : I → J → Bool) (B : I → J → ℕ)
    (r cR : I → ℕ) (c cC : J → ℕ) (z : ((I × J) × Bool) → ℕ)
    (hz : InBox (fun u => B u.1.1 u.1.2) z) :
    penalty cellLine (smallCoordinate small) (fullOffset B cR cC) viewSlope
      (smallOffset small B r c) viewSlope z =
      (∑ i, |((∑ j, rowView z i j):ℝ)-cR i|)+
      (∑ j, |((∑ i, columnView B z i j):ℝ)-cC j|)+
      (∑ i, max (((∑ j, if small i j then rowView z i j else 0):ℝ)-r i) 0)+
      (∑ j, max (((∑ i, if small i j then columnView B z i j else 0):ℝ)-c j) 0) := by
…

Mentions: OAI.ContingencyTables.RowColumnPenalties.cellLine, OAI.ContingencyTables.RowColumnPenalties.smallCoordinate, OAI.ContingencyTables.RowColumnPenalties.fullOffset, OAI.ContingencyTables.RowColumnPenalties.viewSlope, OAI.ContingencyTables.RowColumnPenalties.smallOffset, OAI.ContingencyTables.RowColumnPenalties.rowView, OAI.ContingencyTables.RowColumnPenalties.columnView

def OAI.ContingencyTables.RowColumnPenalties.FullConditions line 149
theorem OAI.ContingencyTables.RowColumnPenalties.penalty_zero_iff line 158
Source documentation
Zero penalty means precisely the enlarged full margins and nonnegative original residuals, even for unbalanced defect profiles.
```
theorem penalty_zero_iff (small : I → J → Bool) (B : I → J → ℕ)
    (r rbar : I → ℕ) (c cbar : J → ℕ) (z : ((I × J) × Bool) → ℕ)
    (hz : InBox (fun u => B u.1.1 u.1.2) z) :
    penalty cellLine (smallCoordinate small) (fullOffset B rbar cbar) viewSlope
      (smallOffset small B r c) viewSlope z=0 ↔ FullConditions small B r rbar c cbar z := by
…
```
Mentions: OAI.ContingencyTables.RowColumnPenalties.cellLine, OAI.ContingencyTables.RowColumnPenalties.smallCoordinate, OAI.ContingencyTables.RowColumnPenalties.fullOffset, OAI.ContingencyTables.RowColumnPenalties.viewSlope, OAI.ContingencyTables.RowColumnPenalties.smallOffset, OAI.ContingencyTables.RowColumnPenalties.FullConditions