UnitBoxLaw.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.unitBoxStep line 26
Source documentation
Invalid vectors get harmless stationary rows. Every actual profile row is exactly the computed sampler transition transported to the box.
```
def unitBoxStep (k : BoxIndex) : IntegerLaw BoxIndex (2^(s)) :=
…
```
Mentions: OAI.ContingencyTables.IntegerLaw
lemma OAI.ContingencyTables.SmallGraphProfiles.unitBoxStep_index line 30
lemma OAI.ContingencyTables.SmallGraphProfiles.unitBoxWalk_count line 37
lemma OAI.ContingencyTables.SmallGraphProfiles.unitBoxWalk_actual_count line 44
lemma OAI.ContingencyTables.SmallGraphProfiles.unitBox_iterate line 52
Source documentation
Matrix propagation computes all box masses, including the zero masses of invalid vectors, without enumerating random histories.
```
lemma unitBox_iterate (x : PaperStates r c) (N : ℕ) :
    IntegerMatrixPrograms.iterate (N,
      (List.ofFn (fun target : BoxIndex => List.ofFn (fun source : BoxIndex =>
        (unitBoxStep r c e source).count target)),
       List.ofFn (fun k : BoxIndex => if k=profileIndex r c e x then 1 else 0)))=
      List.ofFn (fun k : BoxIndex =>
        ((unitWalkCounts r c e x N).push (profileIndex r c e)).count k) := by
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.IntegerMatrixPrograms.iterate, OAI.ContingencyTables.SmallGraphProfiles.unitBoxStep, OAI.ContingencyTables.SmallGraphProfiles.profileIndex, OAI.ContingencyTables.SmallGraphProfiles.unitWalkCounts