OAI/Combinatorics/ContingencyTables/Sampling/AllSamplingAccuracy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Accuracy of the single computed sampler for arbitrary margins

  1. def OAI.ContingencyTables.SmallGraphProfiles.scheduledTableDraw line 20

    Source documentation

    The mathematical draw whose code is the output of the single public program.

    def scheduledTableDraw (htotal : (∑ i,r i)=∑ j,c j) (k : ℕ)
    (bits : Fin (finiteSamplerBits r c k) → Bool) : Table r c :=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.finiteSamplerBits, OAI.ContingencyTables.Table

  2. theorem OAI.ContingencyTables.SmallGraphProfiles.samplingMatrixAll_code line 33
  3. theorem OAI.ContingencyTables.SmallGraphProfiles.publicSamplingAll_spec line 45
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.law_uniform_of_subsingleton line 52
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.variation_uniform_of_subsingleton line 61
  6. theorem OAI.ContingencyTables.SmallGraphProfiles.scheduledTableDraw_accuracy line 67

    Source documentation

    Only the two cited published inputs on the completion grid are used. The small and zero-dimensional branches need neither input.

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