OAI/Combinatorics/ContingencyTables/Sampling/ExactBoxBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The boxes actually enumerated by the exact correction have singly exponential size

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.originalEnumeration_count line 20
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.originalEnumeration_count_bound line 27
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.profileEnumeration_count line 39
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.profileEnumeration_count_bound line 45
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.exact_boxes_absorbed line 63

    Source documentation

    Any fixed polynomial of the product of these enumeration sizes is absorbed by the actual correction probability.

    lemma exact_boxes_absorbed (p : Polynomial ℕ) (A : ℕ) :
    p.eval (A*2^(3*(d*b)))≤2^(correctionPrecision r c)*
      (p.eval A*2^((3*p.natDegree)^2)) := by
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.correctionPrecision