PairedProfileSemantics.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The computed paired counts are the manuscript's literal profile

def OAI.ContingencyTables.PairedProfileSemantics.cellRows line 19
lemma OAI.ContingencyTables.PairedProfileSemantics.cellRows_lengths line 24
lemma OAI.ContingencyTables.PairedProfileSemantics.cellRows_flatten line 28
lemma OAI.ContingencyTables.PairedProfileSemantics.rows_encode line 41
lemma OAI.ContingencyTables.PairedProfileSemantics.counts_cellRow line 46
theorem OAI.ContingencyTables.PairedProfileSemantics.profileRows_encode line 56
lemma OAI.ContingencyTables.PairedProfileSemantics.copy_viewCount line 66
lemma OAI.ContingencyTables.PairedProfileSemantics.physical_profile_reindex line 84
theorem OAI.ContingencyTables.PairedProfileSemantics.profileRows_physical line 102
Source documentation
The executed rows use the catalog's actual order, with one pair of counts per retained physical cell.
```
theorem profileRows_physical (S : Set (Labels A × Bool)) :
    profileRows (List.ofFn (CompanionComputedInitial.capacities A),
      encodeSet (CompanionComputedInitial.coordinateOrder A) S)=
      List.ofFn (fun i =>
        (CompanionWeightOracle.profile A S ((CompanionComputedInitial.cellOrder A).symm i,false),
         CompanionWeightOracle.profile A S ((CompanionComputedInitial.cellOrder A).symm i,true))) := by
…
```
Mentions: OAI.ContingencyTables.CompanionComputedInitial.capacities, OAI.ContingencyTables.CompanionComputedInitial.coordinateOrder, OAI.ContingencyTables.CompanionWeightOracle.profile, OAI.ContingencyTables.CompanionComputedInitial.cellOrder