ProfileRepairProgram.lean`

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A polynomial binary program for the literal small-profile repair

def OAI.ContingencyTables.ProfilePrograms.differenceEntry line 11
def OAI.ContingencyTables.ProfilePrograms.differenceEntryRealizer line 14
lemma OAI.ContingencyTables.ProfilePrograms.polynomial_differenceEntry line 19
def OAI.ContingencyTables.ProfilePrograms.listDifference line 29
Source documentation
Preserve the second list's length, including malformed inputs.
```
def listDifference (z : List ℕ×List ℕ) : List ℕ :=
…
```
def OAI.ContingencyTables.ProfilePrograms.listDifferenceRealizer line 32
lemma OAI.ContingencyTables.ProfilePrograms.polynomial_listDifference line 36
lemma OAI.ContingencyTables.ProfilePrograms.listDifference_ofFn line 46
lemma OAI.ContingencyTables.ProfilePrograms.listExchange_ofFn_nat line 60
Source documentation
Natural indices permit the receiver to be absent from the list.
```
lemma listExchange_ofFn_nat {n : ℕ} (v : Fin n → ℕ) (i j : ℕ) :
    listExchange (List.ofFn v,(i,j))=
      List.ofFn (fun a => v a+(if a.val=i then 1 else 0)-(if a.val=j then 1 else 0)) := by
…
```
Mentions: OAI.ContingencyTables.ProfilePrograms.listExchange
abbrev OAI.ContingencyTables.ProfilePrograms.RepairInput line 73
def OAI.ContingencyTables.ProfilePrograms.repairedViews line 76
Source documentation
The final pair stores the source and receiver respectively.
```
def repairedViews (z : RepairInput) : List ℕ×List ℕ :=
…
```
Mentions: OAI.ContingencyTables.ProfilePrograms.RepairInput
def OAI.ContingencyTables.ProfilePrograms.repairRowsRealizer line 80
lemma OAI.ContingencyTables.ProfilePrograms.polynomial_repairRows line 86
def OAI.ContingencyTables.ProfilePrograms.repairedViewsRealizer line 92
theorem OAI.ContingencyTables.ProfilePrograms.polynomial_repairedViews line 96
def OAI.ContingencyTables.SmallGraphProfiles.cellIndex line 114
Source documentation
An absent large cell receives the out-of-range code n.
```
def cellIndex (t : I×J) : ℕ :=
…
```
lemma OAI.ContingencyTables.SmallGraphProfiles.cellIndex_eq line 118
def OAI.ContingencyTables.SmallGraphProfiles.viewList line 136
lemma OAI.ContingencyTables.SmallGraphProfiles.indexed_transfer line 139
theorem OAI.ContingencyTables.SmallGraphProfiles.repairedViews_eq line 151
Source documentation
The executable row transfer and complement produce exactly the graph repair, including a large crossing cell outside the stored list.
```
theorem repairedViews_eq (B : I → J → ℕ) (v : SmallProfile small) (s t : I×J) :
    repairedViews (viewList small e v false,
      (List.ofFn (fun i => B (e i).val.1 (e i).val.2),
        (cellIndex small e t,cellIndex small e (t.1,s.2))))=
      (viewList small e (repairedProfile small B v s t) false,
        viewList small e (repairedProfile small B v s t) true) := by
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.viewList, OAI.ContingencyTables.SmallGraphProfiles.cellIndex, OAI.ContingencyTables.SmallGraphProfiles.repairedProfile