ProfileBoxLaw.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual adaptive profile walk embedded in its enumerable box

def OAI.ContingencyTables.SmallGraphProfiles.profileBoxStep line 30
Source documentation
Invalid vectors get harmless stationary rows. Every actual profile row is exactly the computed sampler transition transported to the box.
```
def profileBoxStep (k : BoxIndex) : IntegerLaw BoxIndex (2^(s+f)) :=
…
```
Mentions: OAI.ContingencyTables.IntegerLaw
lemma OAI.ContingencyTables.SmallGraphProfiles.profileBoxStep_index line 34
lemma OAI.ContingencyTables.SmallGraphProfiles.profileBoxWalk_count line 41
lemma OAI.ContingencyTables.SmallGraphProfiles.profileBoxWalk_actual_count line 48
lemma OAI.ContingencyTables.SmallGraphProfiles.profileBox_iterate line 56
Source documentation
Matrix propagation computes all box masses, including the zero masses of invalid vectors, without enumerating random histories.
```
lemma profileBox_iterate (x : PaperStates r c) (N : ℕ) :
    IntegerMatrixPrograms.iterate (N,
      (List.ofFn (fun target : BoxIndex => List.ofFn (fun source : BoxIndex =>
        (profileBoxStep r c e hr hc b h hb source).count target)),
       List.ofFn (fun k : BoxIndex => if k=profileIndex r c e x then 1 else 0)))=
      List.ofFn (fun k : BoxIndex =>
        ((listedWalkCounts r c e hr hc b h hb x N).push (profileIndex r c e)).count k) := by
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.IntegerMatrixPrograms.iterate, OAI.ContingencyTables.SmallGraphProfiles.profileBoxStep, OAI.ContingencyTables.SmallGraphProfiles.profileIndex, OAI.ContingencyTables.SmallGraphProfiles.listedWalkCounts