AllSamplingSemantics.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

One executable program chooses the correct rectangle branch

lemma OAI.ContingencyTables.SmallGraphProfiles.hasLargeRectangle_spec line 21
lemma OAI.ContingencyTables.SmallGraphProfiles.allSmall_of_no_large line 28
lemma OAI.ContingencyTables.SmallGraphProfiles.parameterUnitWords_ofFn line 41
lemma OAI.ContingencyTables.SmallGraphProfiles.unitCodeBits_le line 45
lemma OAI.ContingencyTables.SmallGraphProfiles.scheduled_steps_pos line 50
lemma OAI.ContingencyTables.SmallGraphProfiles.unitSamplingMatrix_code line 57
Source documentation
The all-small branch uses a prefix of the same public fixed-length word.
```
lemma unitSamplingMatrix_code (hsmall : ∀ i j,paperSmall r c i j=true)
    (htotal : (∑ i,r i)=∑ j,c j) (k : ℕ) (bits : Fin (finiteSamplerBits r c k) → Bool) :
    unitSamplingMatrix (((List.ofFn r,List.ofFn c),k),List.ofFn bits)=
      matrixCode (unitCodeOuterDraw r c (computedCellEquiv r c) (allSmallFibre r c hsmall)
        (tableState r c (GreedyFeasibleTable.table r c htotal)) (outerSteps d b k) (outerTrials d k)
        (GreedyFeasibleTable.table r c htotal) (prefixWord (unitCodeBits_le r c k) bits)).val := by
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.finiteSamplerBits, OAI.ContingencyTables.SmallGraphProfiles.unitCodeOuterDraw, OAI.ContingencyTables.SmallGraphProfiles.computedCellEquiv, OAI.ContingencyTables.SmallGraphProfiles.allSmallFibre, OAI.ContingencyTables.SmallGraphProfiles.tableState, OAI.ContingencyTables.GreedyFeasibleTable.table, OAI.ContingencyTables.outerSteps, OAI.ContingencyTables.outerTrials, OAI.ContingencyTables.SmallGraphProfiles.unitCodeBits_le