OAI/Combinatorics/ContingencyTables/Sampling/ExactSamplingMachine.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact public sampler in uniform expected polynomial bit time

  1. theorem OAI.ContingencyTables.SmallGraphProfiles.exact_expected_polynomial line 16
  2. theorem OAI.ContingencyTables.SmallGraphProfiles.exactSampling_conditional line 60

    Source documentation

    Paper 200-01, main theorem (ii), conditional on the cited finite-box Prékopa--Leindler and finite-grid Cheeger inputs. The machine is fixed, including parsing, printing, and the unbiased-bit implementation.

    theorem exactSampling_conditional
    (hPL : ∀ q,PublishedInputs.FiniteBoxPrekopaLeindler q)
    (hCheeger : ∀ q k,PublishedInputs.FiniteCheeger (GridBoundary.Grid (I := Fin q) (4*k^8))) :
…

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