OAI/Combinatorics/ContingencyTables/Sampling/ProfileScheduleSemantics.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The computed schedule and initializer equal the proved sampler data

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.marginDimension_ofFn line 19
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.marginPadding_ofFn line 22
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.marginStateBound_ofFn line 25
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.marginBinaryLength_ofFn line 29
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.parameterDimension_ofFn line 33
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.parameterBinaryLength_ofFn line 36
  7. lemma OAI.ContingencyTables.SmallGraphProfiles.parameterTrials_ofFn line 39
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.parameterSteps_ofFn line 44
  9. lemma OAI.ContingencyTables.SmallGraphProfiles.parameterAccuracy_ofFn line 49
  10. lemma OAI.ContingencyTables.SmallGraphProfiles.parameterProposalWidth_ofFn line 54
  11. lemma OAI.ContingencyTables.SmallGraphProfiles.parameterCompletionWidth_ofFn line 58
  12. lemma OAI.ContingencyTables.SmallGraphProfiles.parameterWordCount_ofFn line 63
  13. lemma OAI.ContingencyTables.SmallGraphProfiles.initialConfiguration_code line 68
  14. lemma OAI.ContingencyTables.SmallGraphProfiles.samplingSchedule_ofFn line 78
  15. theorem OAI.ContingencyTables.SmallGraphProfiles.samplingMatrix_code line 86

    Source documentation

    Equality of the actual list program with the listed finite-word draw. The current theorem is for the nonempty large-rectangle branch.

    theorem samplingMatrix_code
    (hr : 0<(largeIndices (d^20,List.ofFn r)).length)
    (hc : 0<(largeIndices (d^20,List.ofFn c)).length)
    (htotal : (∑ i,r i)=∑ j,c j) (k : ℕ)
    (bits : Fin (finiteSamplerBits r c k) → Bool) :
    samplingMatrix (((List.ofFn r,List.ofFn c),k),List.ofFn bits)=
      matrixCode (listedOuterDraw r c (computedCellEquiv r c) hr hc b (outerAccuracy d b k)
        (smallBinaryLength_parameters r c).1 (tableState r c (GreedyFeasibleTable.table r c htotal))
        (outerSteps d b k) (outerTrials d k) (GreedyFeasibleTable.table r c htotal) bits).val := by
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.finiteSamplerBits, OAI.ContingencyTables.SmallGraphProfiles.listedOuterDraw, OAI.ContingencyTables.SmallGraphProfiles.computedCellEquiv, OAI.ContingencyTables.outerAccuracy, OAI.ContingencyTables.SmallGraphProfiles.smallBinaryLength_parameters, OAI.ContingencyTables.SmallGraphProfiles.tableState, OAI.ContingencyTables.GreedyFeasibleTable.table, OAI.ContingencyTables.outerSteps, OAI.ContingencyTables.outerTrials