OAI/Combinatorics/ContingencyTables/Sampling/ExactCorrectionPrefix.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The executed correction prefixes converge to the exact residual law

  1. def OAI.ContingencyTables.ProfilePrograms.correctionPrefix line 11
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.correctionPrefix_failure line 28
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.correctionPrefix_limit line 41
  4. theorem OAI.ContingencyTables.SmallGraphProfiles.corrected_prefix_limit line 63

    Source documentation

    The ordinary draw and correction prefixes have uniform limiting table mass.

    theorem corrected_prefix_limit
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler q)
    (hCheeger : PublishedInputs.FiniteCheeger (GridBoundary.Grid (I := Fin q) (4*d^8)))
…

    Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger, OAI.ContingencyTables.GridBoundary.Grid