OAI/Combinatorics/ContingencyTables/Sampling/ProfileInverseRepairProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.ProfilePrograms.InverseRepairInput line 13

   Source documentation

   The three indices are the negative cell, positive cell and crossing cell. A crossing cell outside the small list has its length as index.

   abbrev InverseRepairInput := List ℕ×(List ℕ×(ℕ×(ℕ×ℕ)))

2. def OAI.ContingencyTables.ProfilePrograms.backwardRows line 15
3. def OAI.ContingencyTables.ProfilePrograms.backwardRowsRealizer line 18
4. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_backwardRows line 21
5. def OAI.ContingencyTables.ProfilePrograms.backwardColumns line 26
6. def OAI.ContingencyTables.ProfilePrograms.backwardColumnsRealizer line 29
7. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_backwardColumns line 34
8. def OAI.ContingencyTables.ProfilePrograms.backwardViews line 41
9. def OAI.ContingencyTables.ProfilePrograms.backwardViewsRealizer line 44
10. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_backwardViews line 48
11. lemma OAI.ContingencyTables.SmallGraphProfiles.transfer_at_index line 65
12. theorem OAI.ContingencyTables.SmallGraphProfiles.backwardViews_eq line 74

    Source documentation

    Exactness holds for all input profiles; neither boundedness nor a preexisting proof of a defect is needed to execute the inverse formula.

    theorem backwardViews_eq (B : I → J → ℕ) (v : SmallProfile small) (s t : I×J) :
        backwardViews (viewList small e v false,
          (List.ofFn (fun i => B (e i).val.1 (e i).val.2),
            (cellIndex small e s,(cellIndex small e t,cellIndex small e (t.1,s.2)))))=
          (viewList small e (inverseRepairProfile small B v s t) false,
            viewList small e (inverseRepairProfile small B v s t) true) := by
    …

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.viewList, OAI.ContingencyTables.SmallGraphProfiles.cellIndex, OAI.ContingencyTables.SmallGraphProfiles.inverseRepairProfile