OAI/Combinatorics/ContingencyTables/Sampling/CompiledResidualCorrection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact residual correction for the compiled public draw

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.correctionPrecision_pos line 18
  2. theorem OAI.ContingencyTables.SmallGraphProfiles.scheduled_residual_correction line 24

    Source documentation

    The residual uses the compiled sampler's finite output law.

    theorem scheduled_residual_correction
    (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

  3. theorem OAI.ContingencyTables.SmallGraphProfiles.public_residual_correction line 49

    Source documentation

    Consequently the same exact mixture identity holds for every sufficiently long execution of the physical finite-transition machine.

    theorem public_residual_correction
    (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