OAI/Combinatorics/ContingencyTables/Sampling/RepairResiduals.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Original residual bounds are preserved by the literal repair

Only a small source entry is lowered. Every large entry is unchanged or increased. Since full row and column-view totals are preserved, the small row/column sums cannot increase.

  1. def OAI.ContingencyTables.largeRow line 20
  2. def OAI.ContingencyTables.smallColumnView line 23
  3. def OAI.ContingencyTables.largeColumnView line 26
  4. lemma OAI.ContingencyTables.row_small_large line 30
  5. lemma OAI.ContingencyTables.column_small_large line 39
  6. lemma OAI.ContingencyTables.repairMatrix_large line 48
  7. theorem OAI.ContingencyTables.repairMatrix_small_sums line 68

    Source documentation

    This covers small and large receivers and the two possible receiver coincidences without a special case in the residual calculation.

    theorem repairMatrix_small_sums {small : I → J → Bool} {x q : I → J → ℕ} {s t : I×J}
    (h : IsDefect x q s t) (hs : small s.1 s.2=true) (ht : small t.1 t.2=true) :
    (∀ i, smallRow small (repairMatrix x s t) i ≤ smallRow small x i) ∧
      (∀ j, smallColumnView small (repairMatrix x s t) j ≤ smallColumnView small q j) := by
…

    Mentions: OAI.ContingencyTables.IsDefect, OAI.ContingencyTables.repairMatrix, OAI.ContingencyTables.smallColumnView

  8. lemma OAI.ContingencyTables.entry_le_smallRow line 102
  9. lemma OAI.ContingencyTables.entry_le_smallColumn line 109
  10. theorem OAI.ContingencyTables.repairMatrix_small_capacity line 117

    Source documentation

    Every repaired small cell respects the manuscript's actual U box, because one of its original incident margins is strictly below U.

    theorem repairMatrix_small_capacity {x q : I → J → ℕ} {s t : I×J}
    (r : I → ℕ) (c : J → ℕ) (U : ℕ) (h : IsDefect x q s t)
    (hs : firstPaperSmall r c U s.1 s.2=true) (ht : firstPaperSmall r c U t.1 t.2=true)
    (hr : ∀ i, smallRow (firstPaperSmall r c U) x i ≤ r i)
    (hc : ∀ j, smallColumnView (firstPaperSmall r c U) q j ≤ c j)
    (i : I) (j : J) (hij : firstPaperSmall r c U i j=true) :
    repairMatrix x s t i j < U := by
…

    Mentions: OAI.ContingencyTables.IsDefect, OAI.ContingencyTables.smallColumnView, OAI.ContingencyTables.repairMatrix