OAI/Combinatorics/ContingencyTables/Sampling/ExactRareCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial dependence of the correction cost on its finite tabulation measure

  1. def OAI.ContingencyTables.ExactRareCost.measure line 15
  2. theorem OAI.ContingencyTables.ExactRareCost.core_polynomial line 17
  3. def OAI.ContingencyTables.ExactRareCost.publicMeasure line 40
  4. theorem OAI.ContingencyTables.ExactRareCost.public_polynomial line 45

    Source documentation

    All copying and physical simulation costs are polynomial in the already explicit finite-tabulation measure.

    theorem public_polynomial : ∃ p : Polynomial ℕ,∀ as B,
    LiteralProgram.packTime as.length+ExactPhysicalCost.budget as 1 B+
      LiteralProgram.postTime B+1 ≤ p.eval (publicMeasure as B) := by
…

    Mentions: OAI.ContingencyTables.LiteralProgram.packTime, OAI.ContingencyTables.ExactPhysicalCost.budget, OAI.ContingencyTables.LiteralProgram.postTime, OAI.ContingencyTables.ExactRareCost.publicMeasure