OAI/Combinatorics/ContingencyTables/Sampling/AllSamplingMachine.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The bounded public sampler on every margin pair

  1. def OAI.ContingencyTables.ProfilePrograms.allSamplingMachine line 12
  2. def OAI.ContingencyTables.ProfilePrograms.allSamplingMachineTime line 14
  3. lemma OAI.ContingencyTables.ProfilePrograms.publicSamplingAll_alphabet line 17
  4. lemma OAI.ContingencyTables.ProfilePrograms.allSamplingMachineTime_polynomial line 20
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.allSamplingMachineTime_public_bound line 35
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.allSamplingMachine_outputs line 53
  7. lemma OAI.ContingencyTables.SmallGraphProfiles.allSamplingMachine_mass line 75
  8. theorem OAI.ContingencyTables.SmallGraphProfiles.boundedSampling_conditional line 88

    Source documentation

    Paper 200-01, main theorem (i), conditional only on Prékopa (1973) Theorem 3/(2.3) on finite boxes and Levin--Peres (2017) Theorem 13.10, (13.6), Lemma 13.7 on the completion grids.

    theorem boundedSampling_conditional
    (hPL : ∀ q,PublishedInputs.FiniteBoxPrekopaLeindler q)
    (hCheeger : ∀ q d,PublishedInputs.FiniteCheeger
      (GridBoundary.Grid (I := Fin q) (4*d^8))) : BoundedSamplingStatement := by
…

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