OAI/Combinatorics/ContingencyTables/Sampling/ProfilePublicSemantics.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.ProfilePrograms.samplingPrecision_spec line 11
2. lemma OAI.ContingencyTables.ProfilePrograms.samplingInput_spec line 23
3. lemma OAI.ContingencyTables.SmallGraphProfiles.parsedSampling_spec line 42
4. lemma OAI.ContingencyTables.SmallGraphProfiles.publicWordCount_spec line 53
5. theorem OAI.ContingencyTables.SmallGraphProfiles.publicSampling_spec line 58

   Source documentation

   Each concrete public word prints the matrix of the proved finite draw.

   theorem publicSampling_spec
       (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) :
       publicSampling (Algorithms.encodeSamplingInput r c k,List.ofFn bits)=
         Algorithms.encodeMatrix (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.Algorithms.encodeSamplingInput, OAI.ContingencyTables.Algorithms.encodeMatrix, 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