OAI/Combinatorics/ContingencyTables/Machines/ScheduledResidualProgram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Executing residual weights from margins, precision, and branch denominator

  1. abbrev OAI.ContingencyTables.ProfilePrograms.ScheduledResidualCache line 14

    Source documentation

    Ordinary count vector, original margins, and reciprocal branch probability.

    abbrev ScheduledResidualCache := List ℕ×(CompletionMargins×ℕ)
  2. def OAI.ContingencyTables.ProfilePrograms.scheduledResidualCache line 16
  3. def OAI.ContingencyTables.ProfilePrograms.scheduledResidualCacheRealizer line 19
  4. def OAI.ContingencyTables.ProfilePrograms.scheduledResidualMeasure line 23
  5. lemma OAI.ContingencyTables.ProfilePrograms.work_scheduledResidualCache line 26
  6. def OAI.ContingencyTables.ProfilePrograms.cachedResidualInput line 40
  7. def OAI.ContingencyTables.ProfilePrograms.cachedResidualInputRealizer line 43
  8. def OAI.ContingencyTables.ProfilePrograms.cachedResidualMeasure line 50
  9. lemma OAI.ContingencyTables.ProfilePrograms.work_cachedResidualInput line 53
  10. def OAI.ContingencyTables.ProfilePrograms.cachedResidualCounts line 76
  11. def OAI.ContingencyTables.ProfilePrograms.cachedResidualCountsRealizer line 79
  12. lemma OAI.ContingencyTables.ProfilePrograms.work_cachedResidualCounts line 83
  13. def OAI.ContingencyTables.ProfilePrograms.scheduledResidualCounts line 89

    Source documentation

    This computes the complete correction vector; it asks for no probability oracle.

    def scheduledResidualCounts (z : SamplingParameters×ℕ) : List ℕ :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.SamplingParameters

  14. def OAI.ContingencyTables.ProfilePrograms.scheduledResidualCountsRealizer line 92
  15. lemma OAI.ContingencyTables.ProfilePrograms.work_scheduledResidualCounts line 96