OAI/Combinatorics/ContingencyTables/Sampling/ExactExpectedTime.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.ExactExpectedTime.bound line 23

   Source documentation

   Expected runtime is bounded by the explicit costs of the ordinary prefix and the probability-weighted correction branch.

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

2. theorem OAI.ContingencyTables.ExactExpectedTime.summable line 69

   Source documentation

   The physical tail is summable for every equal-total margin pair.

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