OAI/Combinatorics/ContingencyTables/Machines/ScheduledResidualLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Correctness and positivity of the executed correction vector

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.scheduledCounts_domination line 19
  2. theorem OAI.ContingencyTables.SmallGraphProfiles.scheduledResidualCounts_actual line 38

    Source documentation

    The explicit correction vector is the embedded integer residual law.

    theorem scheduledResidualCounts_actual
    (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.scheduledResidualCounts_sum line 56

    Source documentation

    Positive total weight makes the exact weighted rejection loop applicable.

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