OAI/Combinatorics/ContingencyTables/Sampling/ProfilePublicProgram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The sampler's public binary parser and matrix printer

  1. def OAI.ContingencyTables.ProfilePrograms.samplingPrecision line 12

    Source documentation

    Safely locate the precision field after the two margin vectors.

    def samplingPrecision (ns : List ℕ) : ℕ :=
…
  2. def OAI.ContingencyTables.ProfilePrograms.samplingPrecisionRealizer line 15
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_samplingPrecision line 22
  4. def OAI.ContingencyTables.ProfilePrograms.samplingInput line 31
  5. def OAI.ContingencyTables.ProfilePrograms.samplingInputRealizer line 34
  6. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_samplingInput line 37
  7. def OAI.ContingencyTables.ProfilePrograms.parsedSampling line 40
  8. def OAI.ContingencyTables.ProfilePrograms.parsedSamplingRealizer line 41
  9. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_parsedSampling line 43
  10. def OAI.ContingencyTables.ProfilePrograms.publicWordCount line 46
  11. def OAI.ContingencyTables.ProfilePrograms.publicWordCountRealizer line 47
  12. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_publicWordCount line 50
  13. def OAI.ContingencyTables.ProfilePrograms.publicSampling line 53
  14. def OAI.ContingencyTables.ProfilePrograms.publicSamplingRealizer line 56
  15. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_publicSampling line 65