OAI/Combinatorics/ContingencyTables/Sampling/SmallProfileRepair.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.repairedProfile line 17
2. lemma OAI.ContingencyTables.SmallGraphProfiles.repairMatrix_pointwise line 22
3. lemma OAI.ContingencyTables.SmallGraphProfiles.repairedProfile_bounded line 26
4. lemma OAI.ContingencyTables.SmallGraphProfiles.repairedProfile_balanced line 35
5. theorem OAI.ContingencyTables.SmallGraphProfiles.repairedProfile_injective line 47

   Source documentation

   Fixed ordered defect labels recover both old views from the literal repaired profile; this does not forget the column-view complement.

   theorem repairedProfile_injective (small : I → J → Bool) (B : I → J → ℕ)
       (s t : I×J) (z w : SmallProfile small)
       (hz : ∀ a,z a ≤ B a.1.val.1 a.1.val.2) (hw : ∀ a,w a ≤ B a.1.val.1 a.1.val.2)
       (hdz : IsDefect (smallView small z false) (smallQ small B z) s t)
       (hdw : IsDefect (smallView small w false) (smallQ small B w) s t)
       (he : repairedProfile small B z s t=repairedProfile small B w s t) : z=w := by
   …

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