OAI/Combinatorics/ContingencyTables/Sampling/RepairSmallMargins.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.SmallGraphProfiles.smallQ_column_sum line 17
2. lemma OAI.ContingencyTables.SmallGraphProfiles.repaired_small_row line 26
3. lemma OAI.ContingencyTables.SmallGraphProfiles.repaired_small_column line 36
4. theorem OAI.ContingencyTables.SmallGraphProfiles.repair_small_margin_abs line 52

   Source documentation

   The only loss from a retained margin is the possible single unit placed into the large receiver. This also covers coincident receiver slots.

   theorem repair_small_margin_abs (small : I → J → Bool) (B : I → J → ℕ)
       (z : SmallProfile small) (s t : I×J)
       (hd : IsDefect (smallView small z false) (smallQ small B z) s t)
       (ht : small t.1 t.2=true)
       (hcap : ∀ a : Cells small,repairMatrix (smallView small z false) s t a.val.1 a.val.2 ≤ B a.val.1 a.val.2) :
       (∀ i,|(smallRow small (smallView small (repairedProfile small B z s t) false) i:ℤ)-
         smallRow small (smallView small z false) i| ≤ 1) ∧
       (∀ j,|(smallColumn small B (smallView small (repairedProfile small B z s t) true) j:ℤ)-
         smallColumn small B (smallView small z true) j| ≤ 1) := by
   …

   Mentions: OAI.ContingencyTables.IsDefect, OAI.ContingencyTables.repairMatrix, OAI.ContingencyTables.SmallGraphProfiles.repairedProfile